chore(analysis/inner_product_space/basic): add inner_self_ne_zero (#18587)

This result is trivial, but it's presence is consistent with how we have both `norm_ne_zero` and `norm_ne_zero_iff`.

Author: eric-wieser

src/analysis/inner_product_space/basic.lean

@@ -209,6 +209,9 @@ by rw [←inner_conj_symm, inner_zero_left]; simp only [ring_hom.map_zero]
 lemma inner_self_eq_zero {x : F} : ⟪x, x⟫ = 0 ↔ x = 0 :=
 iff.intro (c.definite _) (by { rintro rfl, exact inner_zero_left _ })
 
+lemma inner_self_ne_zero {x : F} : ⟪x, x⟫ ≠ 0 ↔ x ≠ 0 :=
+inner_self_eq_zero.not
+
 lemma inner_self_re_to_K (x : F) : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
 by norm_num [ext_iff, inner_self_nonneg_im]
 
@@ -248,7 +251,7 @@ begin
   by_cases hy : y = 0,
   { rw [hy], simp only [is_R_or_C.abs_zero, inner_zero_left, mul_zero, add_monoid_hom.map_zero] },
   { change y ≠ 0 at hy,
-    have hy' : ⟪y, y⟫ ≠ 0 := λ h, by rw [inner_self_eq_zero] at h; exact hy h,
+    have hy' : ⟪y, y⟫ ≠ 0 := inner_self_ne_zero.mpr hy,
     set T := ⟪y, x⟫ / ⟪y, y⟫ with hT,
     have h₁ : re ⟪y, x⟫ = re ⟪x, y⟫ := inner_re_symm _ _,
     have h₂ : im ⟪y, x⟫ = -im ⟪x, y⟫ := inner_im_symm _ _,
@@ -510,6 +513,9 @@ begin
     exact inner_zero_left _ }
 end
 
+lemma inner_self_ne_zero {x : E} : ⟪x, x⟫ ≠ 0 ↔ x ≠ 0 :=
+inner_self_eq_zero.not
+
 @[simp] lemma inner_self_nonpos {x : E} : re ⟪x, x⟫ ≤ 0 ↔ x = 0 :=
 begin
   split,

src/analysis/inner_product_space/dual.lean

@@ -131,12 +131,7 @@ begin
                             ... = (ℓ x) * ⟪z, z⟫ / ⟪z, z⟫
             : by rw [h₂]
                             ... = ℓ x
-            : begin
-                have : ⟪z, z⟫ ≠ 0,
-                { change z = 0 → false at z_ne_0,
-                  rwa ←inner_self_eq_zero at z_ne_0 },
-                field_simp [this]
-              end,
+            : by field_simp [inner_self_ne_zero.2 z_ne_0],
     exact h₄ }
 end
 

src/analysis/inner_product_space/gram_schmidt_ortho.lean

@@ -96,7 +96,7 @@ begin
   { by_cases h : gram_schmidt 𝕜 f a = 0,
     { simp only [h, inner_zero_left, zero_div, zero_mul, sub_zero], },
     { rw [← inner_self_eq_norm_sq_to_K, div_mul_cancel, sub_self],
-      rwa [ne.def, inner_self_eq_zero], }, },
+      rwa [inner_self_ne_zero], }, },
   simp_intros i hi hia only [finset.mem_range],
   simp only [mul_eq_zero, div_eq_zero_iff, inner_self_eq_zero],
   right,

src/geometry/euclidean/angle/unoriented/basic.lean

@@ -112,8 +112,7 @@ end
 @[simp] lemma angle_self {x : V} (hx : x ≠ 0) : angle x x = 0 :=
 begin
   unfold angle,
-  rw [←real_inner_self_eq_norm_mul_norm, div_self (λ h, hx (inner_self_eq_zero.1 h)),
-      real.arccos_one]
+  rw [←real_inner_self_eq_norm_mul_norm, div_self (inner_self_ne_zero.2 hx), real.arccos_one]
 end
 
 /-- The angle between a nonzero vector and its negation. -/

src/geometry/euclidean/basic.lean

@@ -1046,7 +1046,7 @@ by rw [←neg_one_smul ℝ v, s.second_inter_smul p v (by norm_num : (-1 : ℝ)
   s.second_inter (s.second_inter p v) v = p :=
 begin
   by_cases hv : v = 0, { simp [hv] },
-  have hv' : ⟪v, v⟫ ≠ 0 := inner_self_eq_zero.not.2 hv,
+  have hv' : ⟪v, v⟫ ≠ 0 := inner_self_ne_zero.2 hv,
   simp only [sphere.second_inter, vadd_vsub_assoc, vadd_vadd, inner_add_right, inner_smul_right,
              div_mul_cancel _ hv'],
   rw [←@vsub_eq_zero_iff_eq V, vadd_vsub, ←add_smul, ←add_div],