∀ (α : Type u_2) (β : Type u_1) (γ : Type u_4) (δ : Type u_3) (x : (α ⊕ γ) ⊕ β ⊕ δ),
  (⇑(Equiv.sumAssoc (α ⊕ γ) β δ) ∘
        Sum.map (⇑(Equiv.sumAssoc α γ β).symm) id ∘
          Sum.map (Sum.map id ⇑(Equiv.sumComm β γ)) id ∘
            Sum.map (⇑(Equiv.sumAssoc α β γ)) id ∘ ⇑(Equiv.sumAssoc (α ⊕ β) γ δ).symm)
      ((⇑(Equiv.sumAssoc (α ⊕ β) γ δ) ∘
          Sum.map (⇑(Equiv.sumAssoc α β γ).symm) id ∘
            Sum.map (Sum.map id ⇑(Equiv.sumComm β γ).symm) id ∘
              Sum.map (⇑(Equiv.sumAssoc α γ β)) id ∘ ⇑(Equiv.sumAssoc (α ⊕ γ) β δ).symm)
        x) =
    x