feat(Analysis/Normed): add additional symm lemmas (leanprover-community#41149)

`Equiv` and `LinearEquiv` have the symm lemmas `symm_apply_eq` and `eq_symm_apply`. This adds those lemmas for `LinearIsometryEquiv`.

Author: TJHeeringa

Mathlib/Algebra/AddConstMap/Equiv.lean

@@ -76,6 +76,22 @@ initialize_simps_projections AddConstEquiv (toFun → apply, invFun → symm_app
 
 @[simp] lemma symm_symm (e : G ≃+c[a, b] H) : e.symm.symm = e := rfl
 
+theorem symm_apply_eq (e : G ≃+c[a, b] H) {a b} :
+    e.symm a = b ↔ a = e b :=
+  e.toEquiv.symm_apply_eq
+
+theorem eq_symm_apply (e : G ≃+c[a, b] H) {a b} :
+    b = e.symm a ↔ e b = a :=
+  e.toEquiv.eq_symm_apply
+
+@[simp] theorem apply_symm_apply (e : G ≃+c[a, b] H) (a) :
+    e (e.symm a) = a :=
+  e.toEquiv.apply_symm_apply _
+
+@[simp] theorem symm_apply_apply (e : G ≃+c[a, b] H) (a) :
+    e.symm (e a) = a :=
+  e.toEquiv.symm_apply_apply _
+
 /-- The identity map as an `AddConstEquiv`. -/
 @[simps! toEquiv apply]
 def refl (a : G) : G ≃+c[a, a] G where

Mathlib/Algebra/Group/Action/Equidecomp.lean

@@ -206,6 +206,14 @@ theorem right_inv {f : Equidecomp X G} {x : X} (h : x ∈ f.target) :
 @[simp]
 theorem symm_symm (f : Equidecomp X G) : f.symm.symm = f := rfl
 
+theorem symm_apply_eq (f : Equidecomp X G) {x y} (hx : x ∈ f.toPartialEquiv.target)
+    (hy : y ∈ f.toPartialEquiv.source) : f.symm x = y ↔ x = f y :=
+  f.toPartialEquiv.symm_apply_eq hy hx
+
+theorem eq_symm_apply (f : Equidecomp X G) {x y} (hx : x ∈ f.toPartialEquiv.target)
+    (hy : y ∈ f.toPartialEquiv.source) : y = f.symm x ↔ f y = x :=
+  f.toPartialEquiv.eq_symm_apply hy hx
+
 theorem symm_involutive : Function.Involutive (symm : Equidecomp X G → _) := symm_symm
 
 theorem symm_bijective : Function.Bijective (symm : Equidecomp X G → _) := symm_involutive.bijective

Mathlib/Algebra/Lie/Basic.lean

@@ -614,6 +614,12 @@ theorem apply_symm_apply (e : L₁ ≃ₗ⁅R⁆ L₂) : ∀ x, e (e.symm x) = x
 theorem symm_apply_apply (e : L₁ ≃ₗ⁅R⁆ L₂) : ∀ x, e.symm (e x) = x :=
   e.toLinearEquiv.symm_apply_apply
 
+theorem symm_apply_eq (e : L₁ ≃ₗ⁅R⁆ L₂) {x y} : e.symm x = y ↔ x = e y :=
+  e.toLinearEquiv.symm_apply_eq
+
+theorem eq_symm_apply (e : L₁ ≃ₗ⁅R⁆ L₂) {x y} : y = e.symm x ↔ e y = x :=
+  e.toLinearEquiv.eq_symm_apply
+
 @[simp]
 theorem refl_symm : (refl : L₁ ≃ₗ⁅R⁆ L₁).symm = refl :=
   rfl
@@ -982,7 +988,13 @@ theorem symm_apply_apply (e : M ≃ₗ⁅R,L⁆ N) : ∀ x, e.symm (e x) = x :=
 
 theorem apply_eq_iff_eq_symm_apply {m : M} {n : N} (e : M ≃ₗ⁅R,L⁆ N) :
     e m = n ↔ m = e.symm n :=
-  (e : M ≃ N).apply_eq_iff_eq_symm_apply
+  e.toEquiv.apply_eq_iff_eq_symm_apply
+
+theorem symm_apply_eq {m : M} {n : N} (e : M ≃ₗ⁅R,L⁆ N) : e.symm n = m ↔ n = e m :=
+  e.toEquiv.symm_apply_eq
+
+theorem eq_symm_apply {m : M} {n : N} (e : M ≃ₗ⁅R,L⁆ N) : m = e.symm n ↔ e m = n :=
+  e.toEquiv.eq_symm_apply
 
 @[simp]
 theorem symm_symm (e : M ≃ₗ⁅R,L⁆ N) : e.symm.symm = e := rfl

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -759,6 +759,14 @@ theorem invFun_eq_symm {e : A ≃⋆ₐ[R] B} : EquivLike.inv e = e.symm :=
 @[simp]
 theorem symm_symm (e : A ≃⋆ₐ[R] B) : e.symm.symm = e := rfl
 
+lemma symm_apply_eq (e : A ≃⋆ₐ[R] B) {x y} :
+    e.symm x = y ↔ x = e y :=
+  e.toEquiv.symm_apply_eq
+
+lemma eq_symm_apply (e : A ≃⋆ₐ[R] B) {x y} :
+    y = e.symm x ↔ e y = x :=
+  e.toEquiv.eq_symm_apply
+
 theorem symm_bijective : Function.Bijective (symm : (A ≃⋆ₐ[R] B) → B ≃⋆ₐ[R] A) :=
   Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
 

Mathlib/Analysis/Normed/Affine/Isometry.lean

@@ -505,6 +505,12 @@ theorem symm_apply_apply (x : P) : e.symm (e x) = x :=
 @[simp]
 theorem symm_symm : e.symm.symm = e := rfl
 
+theorem symm_apply_eq {x y} : e.symm x = y ↔ x = e y :=
+  e.toAffineEquiv.symm_apply_eq
+
+theorem eq_symm_apply {x y} : y = e.symm x ↔ e y = x :=
+  e.toAffineEquiv.eq_symm_apply
+
 theorem symm_bijective : Bijective (AffineIsometryEquiv.symm : (P₂ ≃ᵃⁱ[𝕜] P) → _) :=
   Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
 

Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

@@ -644,6 +644,12 @@ theorem apply_symm_apply (x : E₂) : e (e.symm x) = x :=
 theorem symm_apply_apply (x : E) : e.symm (e x) = x :=
   e.toLinearEquiv.symm_apply_apply x
 
+theorem symm_apply_eq {x y} : e.symm x = y ↔ x = e y :=
+  e.toEquiv.symm_apply_eq
+
+theorem eq_symm_apply {x y} : y = e.symm x ↔ e y = x :=
+  e.toEquiv.eq_symm_apply
+
 theorem map_eq_zero_iff {x : E} : e x = 0 ↔ x = 0 :=
   e.toLinearEquiv.map_eq_zero_iff
 

Mathlib/Data/PEquiv.lean

@@ -126,6 +126,12 @@ theorem symm_refl : (PEquiv.refl α).symm = PEquiv.refl α :=
 @[simp]
 theorem symm_symm (f : α ≃. β) : f.symm.symm = f := rfl
 
+theorem symm_apply_eq (f : α ≃. β) {x : β} {y : α} : f.symm x = y ↔ x = f y := by
+  rw [eq_some_iff, eq_comm]
+
+theorem eq_symm_apply (f : α ≃. β) {x : β} {y : α} : y = f.symm x ↔ f y = x := by
+  rw [← eq_some_iff, eq_comm]
+
 theorem symm_bijective : Function.Bijective (PEquiv.symm : (α ≃. β) → β ≃. α) :=
   Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
 

Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

@@ -102,6 +102,14 @@ def toIsometry (g : Q₁.IsometryEquiv Q₂) : Q₁ →qᵢ Q₂ where
 @[simp] lemma symm_apply_apply (f : Q₁.IsometryEquiv Q₂) (x : M₁) : f.symm (f x) = x :=
   f.toEquiv.symm_apply_apply x
 
+theorem symm_apply_eq (f : Q₁.IsometryEquiv Q₂) {x y} :
+    f.symm x = y ↔ x = f y :=
+  f.toEquiv.symm_apply_eq
+
+theorem eq_symm_apply (f : Q₁.IsometryEquiv Q₂) {x y} :
+    y = f.symm x ↔ f y = x :=
+  f.toEquiv.eq_symm_apply
+
 @[simp] lemma coe_symm_toLinearEquiv (f : Q₁.IsometryEquiv Q₂) : f.toLinearEquiv.symm = f.symm :=
   rfl
 

Mathlib/Logic/Equiv/PartialEquiv.lean

@@ -200,10 +200,14 @@ theorem right_inv {x : β} (h : x ∈ e.target) : e (e.symm x) = x :=
 theorem target_subset_range : e.target ⊆ range e :=
   fun x hx ↦ ⟨e.symm x, right_inv e hx⟩
 
-theorem eq_symm_apply {x : α} {y : β} (hx : x ∈ e.source) (hy : y ∈ e.target) :
-    x = e.symm y ↔ e x = y :=
+theorem symm_apply_eq {x : α} {y : β} (hx : x ∈ e.source) (hy : y ∈ e.target) :
+    e.symm y = x ↔ y = e x :=
   ⟨fun h => by rw [← e.right_inv hy, h], fun h => by rw [← e.left_inv hx, h]⟩
 
+theorem eq_symm_apply {x : α} {y : β} (hx : x ∈ e.source) (hy : y ∈ e.target) :
+    x = e.symm y ↔ e x = y := by
+  simp [eq_comm, ← symm_apply_eq e hx hy]
+
 protected theorem mapsTo : MapsTo e e.source e.target := fun _ => e.map_source
 
 theorem mapsTo_symm : MapsTo e.symm e.target e.source :=

Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

@@ -293,6 +293,12 @@ theorem self_trans_symm (e : α ≃ᵐ β) : e.trans e.symm = refl α :=
 theorem trans_symm (e₁ : α ≃ᵐ β) (e₂ : β ≃ᵐ γ) : (e₁.trans e₂).symm = e₂.symm.trans (e₁.symm) :=
   rfl
 
+theorem symm_apply_eq (e : α ≃ᵐ β) {x y} : e.symm x = y ↔ x = e y :=
+  e.toEquiv.symm_apply_eq
+
+theorem eq_symm_apply (e : α ≃ᵐ β) {x y} : y = e.symm x ↔ e y = x :=
+  e.toEquiv.eq_symm_apply
+
 protected theorem surjective (e : α ≃ᵐ β) : Surjective e :=
   e.toEquiv.surjective