feat(analysis/inner_product_space): promote implications to iffs (#17727

)

src/analysis/inner_product_space/basic.lean

@@ -2226,26 +2226,19 @@ lemma submodule.inner_right_of_mem_orthogonal {u v : E} (hu : u ∈ K) (hv : v 
 lemma submodule.inner_left_of_mem_orthogonal {u v : E} (hu : u ∈ K) (hv : v ∈ Kᗮ) : ⟪v, u⟫ = 0 :=
 by rw [inner_eq_zero_sym]; exact submodule.inner_right_of_mem_orthogonal hu hv
 
-/-- A vector in `(𝕜 ∙ u)ᗮ` is orthogonal to `u`. -/
-lemma inner_right_of_mem_orthogonal_singleton (u : E) {v : E} (hv : v ∈ (𝕜 ∙ u)ᗮ) : ⟪u, v⟫ = 0 :=
-submodule.inner_right_of_mem_orthogonal (submodule.mem_span_singleton_self u) hv
-
-/-- A vector in `(𝕜 ∙ u)ᗮ` is orthogonal to `u`. -/
-lemma inner_left_of_mem_orthogonal_singleton (u : E) {v : E} (hv : v ∈ (𝕜 ∙ u)ᗮ) : ⟪v, u⟫ = 0 :=
-submodule.inner_left_of_mem_orthogonal (submodule.mem_span_singleton_self u) hv
-
-/-- A vector orthogonal to `u` lies in `(𝕜 ∙ u)ᗮ`. -/
-lemma mem_orthogonal_singleton_of_inner_right (u : E) {v : E} (hv : ⟪u, v⟫ = 0) : v ∈ (𝕜 ∙ u)ᗮ :=
+/-- A vector is in `(𝕜 ∙ u)ᗮ` iff it is orthogonal to `u`. -/
+lemma submodule.mem_orthogonal_singleton_iff_inner_right {u v : E} : v ∈ (𝕜 ∙ u)ᗮ ↔ ⟪u, v⟫ = 0 :=
 begin
-  intros w hw,
+  refine ⟨submodule.inner_right_of_mem_orthogonal (submodule.mem_span_singleton_self u), _⟩,
+  intros hv w hw,
   rw submodule.mem_span_singleton at hw,
   obtain ⟨c, rfl⟩ := hw,
   simp [inner_smul_left, hv],
 end
 
-/-- A vector orthogonal to `u` lies in `(𝕜 ∙ u)ᗮ`. -/
-lemma mem_orthogonal_singleton_of_inner_left (u : E) {v : E} (hv : ⟪v, u⟫ = 0) : v ∈ (𝕜 ∙ u)ᗮ :=
-mem_orthogonal_singleton_of_inner_right u $ inner_eq_zero_sym.2 hv
+/-- A vector in `(𝕜 ∙ u)ᗮ` is orthogonal to `u`. -/
+lemma submodule.mem_orthogonal_singleton_iff_inner_left {u v : E} : v ∈ (𝕜 ∙ u)ᗮ ↔ ⟪v, u⟫ = 0 :=
+by rw [submodule.mem_orthogonal_singleton_iff_inner_right, inner_eq_zero_sym]
 
 lemma submodule.sub_mem_orthogonal_of_inner_left {x y : E}
   (h : ∀ (v : K), ⟪x, v⟫ = ⟪y, v⟫) : x - y ∈ Kᗮ :=

src/analysis/inner_product_space/gram_schmidt_ortho.lean

@@ -183,12 +183,12 @@ begin
     rw coe_eq_zero,
     suffices : span 𝕜 (f '' set.Iic j) ≤ (𝕜 ∙ f i)ᗮ,
     { apply orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero,
-      apply mem_orthogonal_singleton_of_inner_left,
-      apply inner_right_of_mem_orthogonal_singleton,
+      rw mem_orthogonal_singleton_iff_inner_left,
+      rw ←mem_orthogonal_singleton_iff_inner_right,
       exact this (gram_schmidt_mem_span 𝕜 f (le_refl j)) },
     rw span_le,
     rintros - ⟨k, hk, rfl⟩,
-    apply mem_orthogonal_singleton_of_inner_left,
+    rw [set_like.mem_coe, mem_orthogonal_singleton_iff_inner_left],
     apply hf,
     refine (lt_of_le_of_lt hk _).ne,
     simpa using hj },
@@ -357,15 +357,15 @@ lemma inner_gram_schmidt_orthonormal_basis_eq_zero {f : ι → E} {i : ι}
   (hi : gram_schmidt_normed 𝕜 f i = 0) (j : ι) :
   ⟪gram_schmidt_orthonormal_basis h f i, f j⟫ = 0 :=
 begin
-  apply inner_right_of_mem_orthogonal_singleton,
+  rw ←mem_orthogonal_singleton_iff_inner_right,
   suffices : span 𝕜 (gram_schmidt_normed 𝕜 f '' Iic j)
     ≤ (𝕜 ∙ gram_schmidt_orthonormal_basis h f i)ᗮ,
   { apply this,
     rw span_gram_schmidt_normed,
     simpa using mem_span_gram_schmidt 𝕜 f (le_refl j) },
   rw span_le,
   rintros - ⟨k, -, rfl⟩,
-  apply mem_orthogonal_singleton_of_inner_left,
+  rw [set_like.mem_coe, mem_orthogonal_singleton_iff_inner_left],
   by_cases hk : gram_schmidt_normed 𝕜 f k = 0,
   { simp [hk] },
   rw ← gram_schmidt_orthonormal_basis_apply h hk,

src/analysis/inner_product_space/projection.lean

@@ -915,7 +915,7 @@ begin
   have h₁ : R (v - w) = -(v - w) := reflection_orthogonal_complement_singleton_eq_neg (v - w),
   have h₂ : R (v + w) = v + w,
   { apply reflection_mem_subspace_eq_self,
-    apply mem_orthogonal_singleton_of_inner_left,
+    rw submodule.mem_orthogonal_singleton_iff_inner_left,
     rw real_inner_add_sub_eq_zero_iff,
     exact h },
   convert congr_arg2 (+) h₂ h₁ using 1,
@@ -1096,7 +1096,7 @@ begin
       apply hV,
       rw hW w hw,
       refine reflection_mem_subspace_eq_self _,
-      apply mem_orthogonal_singleton_of_inner_left,
+      rw submodule.mem_orthogonal_singleton_iff_inner_left,
       exact submodule.sub_mem _ v.prop hφv _ hw },
     -- `v` is also fixed by `φ.trans ρ`
     have H₁V : (v : F) ∈ V,

src/analysis/inner_product_space/two_dim.lean

@@ -215,7 +215,7 @@ def right_angle_rotation_aux₂ : E →ₗᵢ[ℝ] E :=
         have : finrank ℝ E = 2 := fact.out _,
         linarith },
       obtain ⟨w, hw₀⟩ : ∃ w : Kᗮ, w ≠ 0 := exists_ne 0,
-      have hw' : ⟪x, (w:E)⟫ = 0 := inner_right_of_mem_orthogonal_singleton x w.2, -- hw'₀,
+      have hw' : ⟪x, (w:E)⟫ = 0 := submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2,
       have hw : (w:E) ≠ 0 := λ h, hw₀ (submodule.coe_eq_zero.mp h),
       refine le_of_mul_le_mul_right _ (by rwa norm_pos_iff : 0 < ‖(w:E)‖),
       rw ← o.abs_area_form_of_orthogonal hw',

src/geometry/manifold/instances/sphere.lean

@@ -124,8 +124,9 @@ begin
   suffices : ‖(4:ℝ) • w + (‖w‖ ^ 2 - 4) • v‖ ^ 2 = (‖w‖ ^ 2 + 4) ^ 2,
   { have h₃ : 0 ≤ ‖stereo_inv_fun_aux v w‖ := norm_nonneg _,
     simpa [h₁, h₃, -one_pow] using this },
+  rw submodule.mem_orthogonal_singleton_iff_inner_left at hw,
   simp [norm_add_sq_real, norm_smul, inner_smul_left, inner_smul_right,
-    inner_left_of_mem_orthogonal_singleton _ hw, mul_pow, real.norm_eq_abs, hv],
+    hw, mul_pow, real.norm_eq_abs, hv],
   ring
 end
 
@@ -186,7 +187,7 @@ lemma stereo_inv_fun_ne_north_pole (hv : ‖v‖ = 1) (w : (ℝ ∙ v)ᗮ) :
 begin
   refine subtype.ne_of_val_ne _,
   rw ← inner_lt_one_iff_real_of_norm_one _ hv,
-  { have hw : ⟪v, w⟫_ℝ = 0 := inner_right_of_mem_orthogonal_singleton v w.2,
+  { have hw : ⟪v, w⟫_ℝ = 0 := submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2,
     have hw' : (‖(w:E)‖ ^ 2 + 4)⁻¹ * (‖(w:E)‖ ^ 2 - 4) < 1,
     { refine (inv_mul_lt_iff' _).mpr _,
       { nlinarith },
@@ -212,7 +213,7 @@ begin
   have split : ↑x = a • v + ↑y,
   { convert eq_sum_orthogonal_projection_self_orthogonal_complement (ℝ ∙ v) x,
     exact (orthogonal_projection_unit_singleton ℝ hv x).symm },
-  have hvy : ⟪v, y⟫_ℝ = 0 := inner_right_of_mem_orthogonal_singleton v y.2,
+  have hvy : ⟪v, y⟫_ℝ = 0 := submodule.mem_orthogonal_singleton_iff_inner_right.mp y.2,
   have pythag : 1 = a ^ 2 + ‖y‖ ^ 2,
   { have hvy' : ⟪a • v, y⟫_ℝ = 0 := by simp [inner_smul_left, hvy],
     convert norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy' using 2,
@@ -261,7 +262,7 @@ begin
       orthogonal_projection_orthogonal_complement_singleton_eq_zero v,
     have h₂ : orthogonal_projection (ℝ ∙ v)ᗮ w = w :=
       orthogonal_projection_mem_subspace_eq_self w,
-    have h₃ : innerSL v w = (0:ℝ) := inner_right_of_mem_orthogonal_singleton v w.2,
+    have h₃ : innerSL v w = (0:ℝ) := submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2,
     have h₄ : innerSL v v = (1:ℝ) := by simp [real_inner_self_eq_norm_mul_norm, hv],
     simp [h₁, h₂, h₃, h₄, continuous_linear_map.map_add, continuous_linear_map.map_smul,
       mul_smul] },