α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort u_1
x : α
⊢ ↑((Equiv.cast (_ : α = α)).trans (Equiv.cast (_ : α = α))) x = ↑(Equiv.cast (_ : α = α)) x
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α β γ : Sort u_1
h : α = β
h2 : β = γ
x : α
⊢ ↑((Equiv.cast h).trans (Equiv.cast h2)) x = ↑(Equiv.cast (_ : α = γ)) x
substs h h2
no goals
α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort u_1
x : α
⊢ ↑((Equiv.cast (_ : α = α)).trans (Equiv.cast (_ : α = α))) x = ↑(Equiv.cast (_ : α = α)) x
rfl