no goals
α✝ : Type u
α' : Type w
β✝ : Type v
β' : Type x
γ✝ : Type ?u.12562
δ✝ : Type ?u.12565
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Sort u_5
f₁ : α → β
f₂ : β → ε
g₁ : γ → δ
g₂ : δ → ε
x : α ⊕ γ
⊢ Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
cases x <;> rfl