-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ_1 : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
δ : Type u_12
x : (α ⊕ β) ⊕ γ ⊕ δ
inl :
  ∀ (a : α),
    Eq (α := (α ⊕ β) ⊕ γ ⊕ δ)
      (comp (α := (α ⊕ γ) ⊕ β ⊕ δ) (β := ((α ⊕ β) ⊕ γ) ⊕ δ)
        (⇑(sumAssoc (α ⊕ β) γ δ) : (a : ((α ⊕ β) ⊕ γ) ⊕ δ) → (α ⊕ β) ⊕ γ ⊕ δ)
        (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ).symm : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) id)
          (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ).symm : (a : γ ⊕ β) → β ⊕ γ)) id)
            (comp (β := ((α ⊕ γ) ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β) : (a : (α ⊕ γ) ⊕ β) → α ⊕ γ ⊕ β) id)
              (⇑(Equiv.symm (sumAssoc (α ⊕ γ) β δ)) : (a : (α ⊕ γ) ⊕ β ⊕ δ) → ((α ⊕ γ) ⊕ β) ⊕ δ))))
        (comp (α := (α ⊕ β) ⊕ γ ⊕ δ) (β := ((α ⊕ γ) ⊕ β) ⊕ δ)
          (⇑(sumAssoc (α ⊕ γ) β δ) : (a : ((α ⊕ γ) ⊕ β) ⊕ δ) → (α ⊕ γ) ⊕ β ⊕ δ)
          (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β).symm : (a : α ⊕ γ ⊕ β) → (α ⊕ γ) ⊕ β) id)
            (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ) : (a : β ⊕ γ) → γ ⊕ β)) id)
              (comp (β := ((α ⊕ β) ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ) : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) id)
                (⇑(Equiv.symm (sumAssoc (α ⊕ β) γ δ)) : (a : (α ⊕ β) ⊕ γ ⊕ δ) → ((α ⊕ β) ⊕ γ) ⊕ δ))))
          (Sum.inl (Sum.inl a))))
      (Sum.inl (Sum.inl a))
⊢ comp (α := (α ⊕ γ) ⊕ β ⊕ δ) (β := ((α ⊕ β) ⊕ γ) ⊕ δ)
      (⇑(sumAssoc (α ⊕ β) γ δ) : (a : ((α ⊕ β) ⊕ γ) ⊕ δ) → (α ⊕ β) ⊕ γ ⊕ δ)
      (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ).symm : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) id)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ).symm : (a : γ ⊕ β) → β ⊕ γ)) id)
          (comp (β := ((α ⊕ γ) ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β) : (a : (α ⊕ γ) ⊕ β) → α ⊕ γ ⊕ β) id)
            (⇑(Equiv.symm (sumAssoc (α ⊕ γ) β δ)) : (a : (α ⊕ γ) ⊕ β ⊕ δ) → ((α ⊕ γ) ⊕ β) ⊕ δ))))
      (comp (β := ((α ⊕ γ) ⊕ β) ⊕ δ) (⇑(sumAssoc (α ⊕ γ) β δ) : (a : ((α ⊕ γ) ⊕ β) ⊕ δ) → (α ⊕ γ) ⊕ β ⊕ δ)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β).symm : (a : α ⊕ γ ⊕ β) → (α ⊕ γ) ⊕ β) id)
          (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ) : (a : β ⊕ γ) → γ ⊕ β)) id)
            (comp (β := ((α ⊕ β) ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ) : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) id)
              (⇑(Equiv.symm (sumAssoc (α ⊕ β) γ δ)) : (a : (α ⊕ β) ⊕ γ ⊕ δ) → ((α ⊕ β) ⊕ γ) ⊕ δ))))
        x) =
    x
have inl₁ : ∀ (b : β),
  Eq (α := (α ⊕ β) ⊕ γ ⊕ δ)
    (comp (α := (α ⊕ γ) ⊕ β ⊕ δ) (β := ((α ⊕ β) ⊕ γ) ⊕ δ)
      (⇑(sumAssoc (α ⊕ β) γ δ) : (a : ((α ⊕ β) ⊕ γ) ⊕ δ) → (α ⊕ β) ⊕ γ ⊕ δ)
      (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ).symm : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) id)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ).symm : (a : γ ⊕ β) → β ⊕ γ)) id)
          (comp (β := ((α ⊕ γ) ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β) : (a : (α ⊕ γ) ⊕ β) → α ⊕ γ ⊕ β) id)
            (⇑(Equiv.symm (sumAssoc (α ⊕ γ) β δ)) : (a : (α ⊕ γ) ⊕ β ⊕ δ) → ((α ⊕ γ) ⊕ β) ⊕ δ))))
      (comp (α := (α ⊕ β) ⊕ γ ⊕ δ) (β := ((α ⊕ γ) ⊕ β) ⊕ δ)
        (⇑(sumAssoc (α ⊕ γ) β δ) : (a : ((α ⊕ γ) ⊕ β) ⊕ δ) → (α ⊕ γ) ⊕ β ⊕ δ)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β).symm : (a : α ⊕ γ ⊕ β) → (α ⊕ γ) ⊕ β) id)
          (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ) : (a : β ⊕ γ) → γ ⊕ β)) id)
            (comp (β := ((α ⊕ β) ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ) : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) id)
              (⇑(Equiv.symm (sumAssoc (α ⊕ β) γ δ)) : (a : (α ⊕ β) ⊕ γ ⊕ δ) → ((α ⊕ β) ⊕ γ) ⊕ δ))))
        (Sum.inl (inr b))))
    (Sum.inl (inr b))
Tactic: rcases x with ((a | b) | (c | d))
Cleared hypotheses: x