case H
α : Type u_1
β : Type u_2
γ : Type ?u.36194
δ : Type ?u.36197
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
x✝ : β
⊢ ↑(Homeomorph.trans (Homeomorph.symm h) h) x✝ = ↑(Homeomorph.refl β) x✝
α : Type u_1
β : Type u_2
γ : Type ?u.36194
δ : Type ?u.36197
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
⊢ Homeomorph.trans (Homeomorph.symm h) h = Homeomorph.refl β
ext
no goals
case H
α : Type u_1
β : Type u_2
γ : Type ?u.36194
δ : Type ?u.36197
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
x✝ : β
⊢ ↑(Homeomorph.trans (Homeomorph.symm h) h) x✝ = ↑(Homeomorph.refl β) x✝
apply apply_symm_apply