Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl.inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ✝ : Sort u_8
α : Type ?u.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
a : α
⊢ (⇑(sumAssoc (α ⊕ β) γ δ) ∘
        Sum.map (⇑(sumAssoc α β γ).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
      ((⇑(sumAssoc (α ⊕ γ) β δ) ∘
          Sum.map (⇑(sumAssoc α γ β).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
        (inl (inl a))) =
    inl (inl a)

pp: case inl.inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ✝ : Sort u_8
α : Type ?u.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
b : β
⊢ (⇑(sumAssoc (α ⊕ β) γ δ) ∘
        Sum.map (⇑(sumAssoc α β γ).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
      ((⇑(sumAssoc (α ⊕ γ) β δ) ∘
          Sum.map (⇑(sumAssoc α γ β).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
        (inl (inr b))) =
    inl (inr b)

pp: case inr.inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ✝ : Sort u_8
α : Type ?u.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
c : γ
⊢ (⇑(sumAssoc (α ⊕ β) γ δ) ∘
        Sum.map (⇑(sumAssoc α β γ).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
      ((⇑(sumAssoc (α ⊕ γ) β δ) ∘
          Sum.map (⇑(sumAssoc α γ β).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
        (inr (inl c))) =
    inr (inl c)

pp: case inr.inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ✝ : Sort u_8
α : Type ?u.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
d : δ
⊢ (⇑(sumAssoc (α ⊕ β) γ δ) ∘
        Sum.map (⇑(sumAssoc α β γ).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
      ((⇑(sumAssoc (α ⊕ γ) β δ) ∘
          Sum.map (⇑(sumAssoc α γ β).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
        (inr (inr d))) =
    inr (inr d)

Tactic:
<;>

Goal state after:
case inl.inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ✝ : Sort u_8
α : Type ?u.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
a : α
⊢ (⇑(sumAssoc (α ⊕ β) γ δ) ∘
        Sum.map (⇑(sumAssoc α β γ).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
      ((⇑(sumAssoc (α ⊕ γ) β δ) ∘
          Sum.map (⇑(sumAssoc α γ β).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
        (inl (inl a))) =
    inl (inl a)

case inl.inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ✝ : Sort u_8
α : Type ?u.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
b : β
⊢ (⇑(sumAssoc (α ⊕ β) γ δ) ∘
        Sum.map (⇑(sumAssoc α β γ).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
      ((⇑(sumAssoc (α ⊕ γ) β δ) ∘
          Sum.map (⇑(sumAssoc α γ β).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
        (inl (inr b))) =
    inl (inr b)

case inr.inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ✝ : Sort u_8
α : Type ?u.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
c : γ
⊢ (⇑(sumAssoc (α ⊕ β) γ δ) ∘
        Sum.map (⇑(sumAssoc α β γ).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
      ((⇑(sumAssoc (α ⊕ γ) β δ) ∘
          Sum.map (⇑(sumAssoc α γ β).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
        (inr (inl c))) =
    inr (inl c)

case inr.inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ✝ : Sort u_8
α : Type ?u.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
d : δ
⊢ (⇑(sumAssoc (α ⊕ β) γ δ) ∘
        Sum.map (⇑(sumAssoc α β γ).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
      ((⇑(sumAssoc (α ⊕ γ) β δ) ∘
          Sum.map (⇑(sumAssoc α γ β).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
        (inr (inr d))) =
    inr (inr d)