case H
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
i : α₁ ⊕ α₂
⊢ ↑((sumCongr e f).trans (sumCongr g h)) i = ↑(sumCongr (e.trans g) (f.trans h)) i
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
⊢ (sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h)
ext i
no goals
case H
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
i : α₁ ⊕ α₂
⊢ ↑((sumCongr e f).trans (sumCongr g h)) i = ↑(sumCongr (e.trans g) (f.trans h)) i
cases i <;> rfl