feat: forward-port mathlib#18551 (#2669)

forward-port of leanprover-community/mathlib#18551.
leanprover-community · Mar 6, 2023 · 7f714c6 · 7f714c6
1 parent e8dd45a
commit 7f714c6
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
@@ -108,6 +108,11 @@ theorem ext {h h' : α ≃ₜ β} (H : ∀ x, h x = h' x) : h = h' :=
   FunLike.ext _ _ H
 #align homeomorph.ext Homeomorph.ext
 
+@[simp]
+lemma symm_symm (h : α ≃ₜ β) : h.symm.symm = h := by
+  ext
+  rfl
+
 /-- Identity map as a homeomorphism. -/
 @[simps! (config := { fullyApplied := false }) apply]
 protected def refl (α : Type _) [TopologicalSpace α] : α ≃ₜ α where