no goals
α : Type u_1
β : Type u_2
γ : Type ?u.58426
δ : Type ?u.58429
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
⊢ QuotientMap (↑h ∘ ↑(Homeomorph.symm h))
simp only [self_comp_symm, QuotientMap.id]