feat(*/Equiv/*): Add symm_bijective lemmas next to symm_symms (#8444)

linesthatinterlace · eric-wieser · linesthatinterlace · commit e368f2a55ed7 · 2023-12-01T11:18:55.000Z
Co-authored-by: Eric Wieser &lt;wieser.eric@gmail.com&gt;
Co-authored-by: lines &lt;34025592+linesthatinterlace@users.noreply.github.com&gt;
diff --git a/Mathlib/Algebra/Algebra/Equiv.lean b/Mathlib/Algebra/Algebra/Equiv.lean
@@ -362,7 +362,7 @@ theorem symm_symm (e : A₁ ≃ₐ[R] A₂) : e.symm.symm = e := by
 #align alg_equiv.symm_symm AlgEquiv.symm_symm
 
 theorem symm_bijective : Function.Bijective (symm : (A₁ ≃ₐ[R] A₂) → A₂ ≃ₐ[R] A₁) :=
-  Equiv.bijective ⟨symm, symm, symm_symm, symm_symm⟩
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
 #align alg_equiv.symm_bijective AlgEquiv.symm_bijective
 
 @[simp]
diff --git a/Mathlib/Algebra/Group/Equiv/Basic.lean b/Mathlib/Algebra/Group/Equiv/Basic.lean
@@ -343,8 +343,8 @@ theorem symm_symm (f : M ≃* N) : f.symm.symm = f := rfl
 #align add_equiv.symm_symm AddEquiv.symm_symm
 
 @[to_additive]
-theorem symm_bijective : Function.Bijective (symm : M ≃* N → N ≃* M) :=
-  Equiv.bijective ⟨symm, symm, symm_symm, symm_symm⟩
+theorem symm_bijective : Function.Bijective (symm : (M ≃* N) → N ≃* M) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
 #align mul_equiv.symm_bijective MulEquiv.symm_bijective
 #align add_equiv.symm_bijective AddEquiv.symm_bijective
 
diff --git a/Mathlib/Algebra/Homology/ComplexShape.lean b/Mathlib/Algebra/Homology/ComplexShape.lean
@@ -102,6 +102,10 @@ theorem symm_symm (c : ComplexShape ι) : c.symm.symm = c := by
   simp
 #align complex_shape.symm_symm ComplexShape.symm_symm
 
+theorem symm_bijective :
+    Function.Bijective (ComplexShape.symm : ComplexShape ι → ComplexShape ι) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 /-- The "composition" of two `ComplexShape`s.
 
 We need this to define "related in k steps" later.
diff --git a/Mathlib/Algebra/Lie/Basic.lean b/Mathlib/Algebra/Lie/Basic.lean
@@ -633,6 +633,9 @@ theorem symm_symm (e : L₁ ≃ₗ⁅R⁆ L₂) : e.symm.symm = e := by
   rfl
 #align lie_equiv.symm_symm LieEquiv.symm_symm
 
+theorem symm_bijective : Function.Bijective (LieEquiv.symm : (L₁ ≃ₗ⁅R⁆ L₂) → L₂ ≃ₗ⁅R⁆ L₁) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 @[simp]
 theorem apply_symm_apply (e : L₁ ≃ₗ⁅R⁆ L₂) : ∀ x, e (e.symm x) = x :=
   e.toLinearEquiv.apply_symm_apply
@@ -1108,6 +1111,10 @@ theorem symm_symm (e : M ≃ₗ⁅R,L⁆ N) : e.symm.symm = e := by
   rfl
 #align lie_module_equiv.symm_symm LieModuleEquiv.symm_symm
 
+theorem symm_bijective :
+    Function.Bijective (LieModuleEquiv.symm : (M ≃ₗ⁅R,L⁆ N) → N ≃ₗ⁅R,L⁆ M) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 /-- Lie module equivalences are transitive. -/
 @[trans]
 def trans (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) : M ≃ₗ⁅R,L⁆ P :=
diff --git a/Mathlib/Algebra/Module/Equiv.lean b/Mathlib/Algebra/Module/Equiv.lean
@@ -519,9 +519,7 @@ theorem symm_symm (e : M ≃ₛₗ[σ] M₂) : e.symm.symm = e := by
 
 theorem symm_bijective [Module R M] [Module S M₂] [RingHomInvPair σ' σ] [RingHomInvPair σ σ'] :
     Function.Bijective (symm : (M ≃ₛₗ[σ] M₂) → M₂ ≃ₛₗ[σ'] M) :=
-  Equiv.bijective
-    ⟨(symm : (M ≃ₛₗ[σ] M₂) → M₂ ≃ₛₗ[σ'] M), (symm : (M₂ ≃ₛₗ[σ'] M) → M ≃ₛₗ[σ] M₂), symm_symm,
-      symm_symm⟩
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
 #align linear_equiv.symm_bijective LinearEquiv.symm_bijective
 
 @[simp]
diff --git a/Mathlib/Algebra/Order/Hom/Ring.lean b/Mathlib/Algebra/Order/Hom/Ring.lean
@@ -505,9 +505,8 @@ theorem symm_trans_self (e : α ≃+*o β) : e.symm.trans e = OrderRingIso.refl
   ext e.right_inv
 #align order_ring_iso.symm_trans_self OrderRingIso.symm_trans_self
 
-theorem symm_bijective : Bijective (OrderRingIso.symm : α ≃+*o β → β ≃+*o α) :=
-  ⟨fun f g h => f.symm_symm.symm.trans <| (congr_arg OrderRingIso.symm h).trans g.symm_symm,
-    fun f => ⟨f.symm, f.symm_symm⟩⟩
+theorem symm_bijective : Bijective (OrderRingIso.symm : (α ≃+*o β) → β ≃+*o α) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
 #align order_ring_iso.symm_bijective OrderRingIso.symm_bijective
 
 end LE
diff --git a/Mathlib/Algebra/Ring/Equiv.lean b/Mathlib/Algebra/Ring/Equiv.lean
@@ -295,8 +295,8 @@ theorem coe_toEquiv_symm (e : R ≃+* S) : (e.symm : S ≃ R) = (e : R ≃ S).sy
   rfl
 #align ring_equiv.coe_to_equiv_symm RingEquiv.coe_toEquiv_symm
 
-theorem symm_bijective : Function.Bijective (RingEquiv.symm : R ≃+* S → S ≃+* R) :=
-  Equiv.bijective ⟨RingEquiv.symm, RingEquiv.symm, symm_symm, symm_symm⟩
+theorem symm_bijective : Function.Bijective (RingEquiv.symm : (R ≃+* S) → S ≃+* R) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
 #align ring_equiv.symm_bijective RingEquiv.symm_bijective
 
 @[simp]
diff --git a/Mathlib/Algebra/Star/StarAlgHom.lean b/Mathlib/Algebra/Star/StarAlgHom.lean
@@ -867,7 +867,7 @@ theorem symm_symm (e : A ≃⋆ₐ[R] B) : e.symm.symm = e := by
 #align star_alg_equiv.symm_symm StarAlgEquiv.symm_symm
 
 theorem symm_bijective : Function.Bijective (symm : (A ≃⋆ₐ[R] B) → B ≃⋆ₐ[R] A) :=
-  Equiv.bijective ⟨symm, symm, symm_symm, symm_symm⟩
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
 #align star_alg_equiv.symm_bijective StarAlgEquiv.symm_bijective
 
 -- porting note: doesn't align with Mathlib 3 because `StarAlgEquiv.mk` has a new signature
diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
@@ -114,7 +114,7 @@ def reflTransSymm (p : Path x₀ x₁) : Homotopy (Path.refl x₀) (p.trans p.sy
 /-- For any path `p` from `x₀` to `x₁`, we have a homotopy from the constant path based at `x₁` to
   `p.symm.trans p`. -/
 def reflSymmTrans (p : Path x₀ x₁) : Homotopy (Path.refl x₁) (p.symm.trans p) :=
-  (reflTransSymm p.symm).cast rfl <| congr_arg _ Path.symm_symm
+  (reflTransSymm p.symm).cast rfl <| congr_arg _ (Path.symm_symm _)
 #align path.homotopy.refl_symm_trans Path.Homotopy.reflSymmTrans
 
 end
diff --git a/Mathlib/Data/PEquiv.lean b/Mathlib/Data/PEquiv.lean
@@ -135,8 +135,11 @@ theorem symm_refl : (PEquiv.refl α).symm = PEquiv.refl α :=
 theorem symm_symm (f : α ≃. β) : f.symm.symm = f := by cases f; rfl
 #align pequiv.symm_symm PEquiv.symm_symm
 
+theorem symm_bijective : Function.Bijective (PEquiv.symm : (α ≃. β) → β ≃. α) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 theorem symm_injective : Function.Injective (@PEquiv.symm α β) :=
-  LeftInverse.injective symm_symm
+  symm_bijective.injective
 #align pequiv.symm_injective PEquiv.symm_injective
 
 theorem trans_assoc (f : α ≃. β) (g : β ≃. γ) (h : γ ≃. δ) :
diff --git a/Mathlib/Logic/Equiv/Defs.lean b/Mathlib/Logic/Equiv/Defs.lean
@@ -330,6 +330,9 @@ theorem eq_symm_apply {α β} (e : α ≃ β) {x y} : y = e.symm x ↔ e y = x :
 @[simp] theorem symm_symm (e : α ≃ β) : e.symm.symm = e := by cases e; rfl
 #align equiv.symm_symm Equiv.symm_symm
 
+theorem symm_bijective : Function.Bijective (Equiv.symm : (α ≃ β) → β ≃ α) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 @[simp] theorem trans_refl (e : α ≃ β) : e.trans (Equiv.refl β) = e := by cases e; rfl
 #align equiv.trans_refl Equiv.trans_refl
 
diff --git a/Mathlib/Logic/Equiv/LocalEquiv.lean b/Mathlib/Logic/Equiv/LocalEquiv.lean
@@ -333,6 +333,9 @@ theorem symm_symm : e.symm.symm = e := by
   rfl
 #align local_equiv.symm_symm LocalEquiv.symm_symm
 
+theorem symm_bijective : Function.Bijective (LocalEquiv.symm : LocalEquiv α β → LocalEquiv β α) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 theorem image_source_eq_target : e '' e.source = e.target :=
   e.bijOn.image_eq
 #align local_equiv.image_source_eq_target LocalEquiv.image_source_eq_target
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
@@ -1373,6 +1373,10 @@ attribute [simps! apply toEquiv] trans refl
 @[simp]
 theorem symm_symm (e : α ≃ᵐ β) : e.symm.symm = e := rfl
 
+theorem symm_bijective :
+    Function.Bijective (MeasurableEquiv.symm : (α ≃ᵐ β) → β ≃ᵐ α) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 @[simp]
 theorem symm_refl (α : Type*) [MeasurableSpace α] : (refl α).symm = refl α :=
   rfl
diff --git a/Mathlib/Order/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean
@@ -886,8 +886,11 @@ theorem symm_symm (e : α ≃o β) : e.symm.symm = e := by
   rfl
 #align order_iso.symm_symm OrderIso.symm_symm
 
-theorem symm_injective : Function.Injective (symm : α ≃o β → β ≃o α) := fun e e' h => by
-  rw [← e.symm_symm, h, e'.symm_symm]
+theorem symm_bijective : Function.Bijective (OrderIso.symm : (α ≃o β) → β ≃o α) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
+theorem symm_injective : Function.Injective (symm : α ≃o β → β ≃o α) :=
+  symm_bijective.injective
 #align order_iso.symm_injective OrderIso.symm_injective
 
 @[simp]
diff --git a/Mathlib/Topology/Connected/PathConnected.lean b/Mathlib/Topology/Connected/PathConnected.lean
@@ -172,12 +172,15 @@ def symm (γ : Path x y) : Path y x where
 #align path.symm Path.symm
 
 @[simp]
-theorem symm_symm {γ : Path x y} : γ.symm.symm = γ := by
+theorem symm_symm (γ : Path x y) : γ.symm.symm = γ := by
   ext t
   show γ (σ (σ t)) = γ t
   rw [unitInterval.symm_symm]
 #align path.symm_symm Path.symm_symm
 
+theorem symm_bijective : Function.Bijective (Path.symm : Path x y → Path y x) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 @[simp]
 theorem refl_symm {a : X} : (Path.refl a).symm = Path.refl a := by
   ext
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
@@ -79,6 +79,9 @@ protected def symm (h : X ≃ₜ Y) : Y ≃ₜ X where
 @[simp] theorem symm_symm (h : X ≃ₜ Y) : h.symm.symm = h := rfl
 #align homeomorph.symm_symm Homeomorph.symm_symm
 
+theorem symm_bijective : Function.Bijective (Homeomorph.symm : (X ≃ₜ Y) → Y ≃ₜ X) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 /-- See Note [custom simps projection] -/
 def Simps.symm_apply (h : X ≃ₜ Y) : Y → X :=
   h.symm
diff --git a/Mathlib/Topology/Homotopy/Basic.lean b/Mathlib/Topology/Homotopy/Basic.lean
@@ -231,6 +231,10 @@ theorem symm_symm {f₀ f₁ : C(X, Y)} (F : Homotopy f₀ f₁) : F.symm.symm =
   simp
 #align continuous_map.homotopy.symm_symm ContinuousMap.Homotopy.symm_symm
 
+theorem symm_bijective {f₀ f₁ : C(X, Y)} :
+    Function.Bijective (Homotopy.symm : Homotopy f₀ f₁ → Homotopy f₁ f₀) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 /--
 Given `Homotopy f₀ f₁` and `Homotopy f₁ f₂`, we can define a `Homotopy f₀ f₂` by putting the first
 homotopy on `[0, 1/2]` and the second on `[1/2, 1]`.
@@ -503,6 +507,10 @@ theorem symm_symm {f₀ f₁ : C(X, Y)} (F : HomotopyWith f₀ f₁ P) : F.symm.
   ext <| Homotopy.congr_fun <| Homotopy.symm_symm _
 #align continuous_map.homotopy_with.symm_symm ContinuousMap.HomotopyWith.symm_symm
 
+theorem symm_bijective {f₀ f₁ : C(X, Y)} :
+    Function.Bijective (HomotopyWith.symm : HomotopyWith f₀ f₁ P → HomotopyWith f₁ f₀ P) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 /--
 Given `HomotopyWith f₀ f₁ P` and `HomotopyWith f₁ f₂ P`, we can define a `HomotopyWith f₀ f₂ P`
 by putting the first homotopy on `[0, 1/2]` and the second on `[1/2, 1]`.
@@ -629,6 +637,10 @@ theorem symm_symm (F : HomotopyRel f₀ f₁ S) : F.symm.symm = F :=
   HomotopyWith.symm_symm F
 #align continuous_map.homotopy_rel.symm_symm ContinuousMap.HomotopyRel.symm_symm
 
+theorem symm_bijective :
+    Function.Bijective (HomotopyRel.symm : HomotopyRel f₀ f₁ S → HomotopyRel f₁ f₀ S) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 /-- Given `HomotopyRel f₀ f₁ S` and `HomotopyRel f₁ f₂ S`, we can define a `HomotopyRel f₀ f₂ S`
 by putting the first homotopy on `[0, 1/2]` and the second on `[1/2, 1]`.
 -/
diff --git a/Mathlib/Topology/Homotopy/Path.lean b/Mathlib/Topology/Homotopy/Path.lean
@@ -117,6 +117,9 @@ theorem symm_symm (F : Homotopy p₀ p₁) : F.symm.symm = F :=
   ContinuousMap.HomotopyRel.symm_symm F
 #align path.homotopy.symm_symm Path.Homotopy.symm_symm
 
+theorem symm_bijective : Function.Bijective (Homotopy.symm : Homotopy p₀ p₁ → Homotopy p₁ p₀) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 /--
 Given `Homotopy p₀ p₁` and `Homotopy p₁ p₂`, we can define a `Homotopy p₀ p₂` by putting the first
 homotopy on `[0, 1/2]` and the second on `[1/2, 1]`.
diff --git a/Mathlib/Topology/LocalHomeomorph.lean b/Mathlib/Topology/LocalHomeomorph.lean
@@ -356,6 +356,10 @@ theorem symm_target : e.symm.target = e.source :=
 @[simp, mfld_simps] theorem symm_symm : e.symm.symm = e := rfl
 #align local_homeomorph.symm_symm LocalHomeomorph.symm_symm
 
+theorem symm_bijective : Function.Bijective
+    (LocalHomeomorph.symm : LocalHomeomorph α β → LocalHomeomorph β α) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 /-- A local homeomorphism is continuous at any point of its source -/
 protected theorem continuousAt {x : α} (h : x ∈ e.source) : ContinuousAt e x :=
   (e.continuousOn x h).continuousAt (e.open_source.mem_nhds h)
diff --git a/Mathlib/Topology/MetricSpace/DilationEquiv.lean b/Mathlib/Topology/MetricSpace/DilationEquiv.lean
@@ -77,6 +77,10 @@ def symm (e : X ≃ᵈ Y) : Y ≃ᵈ X where
       ENNReal.coe_one, one_mul]
 
 @[simp] theorem symm_symm (e : X ≃ᵈ Y) : e.symm.symm = e := rfl
+
+theorem symm_bijective : Function.Bijective (DilationEquiv.symm : (X ≃ᵈ Y) → Y ≃ᵈ X) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 @[simp] theorem apply_symm_apply (e : X ≃ᵈ Y) (x : Y) : e (e.symm x) = x := e.right_inv x
 @[simp] theorem symm_apply_apply (e : X ≃ᵈ Y) (x : X) : e.symm (e x) = x := e.left_inv x
 
diff --git a/Mathlib/Topology/MetricSpace/Isometry.lean b/Mathlib/Topology/MetricSpace/Isometry.lean
@@ -420,6 +420,9 @@ initialize_simps_projections IsometryEquiv (toEquiv_toFun → apply, toEquiv_inv
 theorem symm_symm (h : α ≃ᵢ β) : h.symm.symm = h := rfl
 #align isometry_equiv.symm_symm IsometryEquiv.symm_symm
 
+theorem symm_bijective : Bijective (IsometryEquiv.symm : (α ≃ᵢ β) → β ≃ᵢ α) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 @[simp]
 theorem apply_symm_apply (h : α ≃ᵢ β) (y : β) : h (h.symm y) = y :=
   h.toEquiv.apply_symm_apply y
diff --git a/Mathlib/Topology/UnitInterval.lean b/Mathlib/Topology/UnitInterval.lean
@@ -123,6 +123,9 @@ theorem symm_symm (x : I) : σ (σ x) = x :=
   Subtype.ext <| by simp [symm]
 #align unit_interval.symm_symm unitInterval.symm_symm
 
+theorem symm_bijective : Function.Bijective (symm : I → I) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
 @[simp]
 theorem coe_symm_eq (x : I) : (σ x : ℝ) = 1 - x :=
   rfl
