case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
x✝¹ : α ≃ δ
x✝ : γ
⊢ ↑(↑((equivCongr ab de).trans (equivCongr bc ef)) x✝¹) x✝ = ↑(↑(equivCongr (ab.trans bc) (de.trans ef)) x✝¹) x✝
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
⊢ (equivCongr ab de).trans (equivCongr bc ef) = equivCongr (ab.trans bc) (de.trans ef)
ext
no goals
case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
x✝¹ : α ≃ δ
x✝ : γ
⊢ ↑(↑((equivCongr ab de).trans (equivCongr bc ef)) x✝¹) x✝ = ↑(↑(equivCongr (ab.trans bc) (de.trans ef)) x✝¹) x✝
rfl