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