feat(Analysis/InnerProductSpace/Basic): add a simp lemma (#30793)

LessnessRandomness · JovanGerb · LessnessRandomness · commit fef46774e78e · 2025-11-14T19:40:08.000Z
Add a simp lemma (for benchmarking purposes - to see if it doesn't have a bad performance impact).

Co-authored-by: Jovan Gerbscheid &lt;jovan.gerbscheid@gmail.com&gt;
diff --git a/Mathlib/Analysis/Convex/Cone/InnerDual.lean b/Mathlib/Analysis/Convex/Cone/InnerDual.lean
@@ -60,7 +60,7 @@ def innerDual (s : Set E) : ProperCone ℝ E := .dual (innerₗ E) s
 /-- Dual cone of the total space is the convex cone `{0}`. -/
 @[simp]
 lemma innerDual_univ : innerDual (univ : Set E) = ⊥ :=
-  le_antisymm (fun x hx ↦ by simpa [← real_inner_self_nonpos] using hx (mem_univ (-x))) (by simp)
+  le_antisymm (fun x hx ↦ by simpa using hx (mem_univ (-x))) (by simp)
 
 @[gcongr] lemma innerDual_le_innerDual (h : t ⊆ s) : innerDual s ≤ innerDual t :=
   fun _y hy _x hx ↦ hy (h hx)
@@ -179,7 +179,7 @@ theorem innerDualCone_univ : (univ : Set H).innerDualCone = 0 := by
   suffices ∀ x : H, x ∈ (univ : Set H).innerDualCone → x = 0 by
     apply SetLike.coe_injective
     exact eq_singleton_iff_unique_mem.mpr ⟨fun x _ => (inner_zero_right _).ge, this⟩
-  exact fun x hx => by simpa [← real_inner_self_nonpos] using hx (-x) (mem_univ _)
+  exact fun x hx => by simpa using hx (-x) (mem_univ _)
 
 variable {s t} in
 set_option linter.deprecated false in
diff --git a/Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean b/Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
@@ -42,7 +42,7 @@ section RCLike
 variable [RCLike R] [Fintype G]
 
 lemma wInner_cWeight_self (ψ : AddChar G R) : ⟪(ψ : G → R), ψ⟫ₙ_[R] = 1 := by
-  simp [wInner_cWeight_eq_expect, ψ.norm_apply, RCLike.mul_conj]
+  simp [wInner_cWeight_eq_expect, ψ.norm_apply]
 
 end RCLike
 end AddGroup
diff --git a/Mathlib/Analysis/InnerProductSpace/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Basic.lean
@@ -61,8 +61,8 @@ theorem inner_eq_zero_symm {x y : E} : ⟪x, y⟫ = 0 ↔ ⟪y, x⟫ = 0 := by
 instance {ι : Sort*} (v : ι → E) : IsSymm ι fun i j => ⟪v i, v j⟫ = 0 where
   symm _ _ := inner_eq_zero_symm.1
 
-@[simp]
-theorem inner_self_im (x : E) : im ⟪x, x⟫ = 0 := by rw [← @ofReal_inj 𝕜, im_eq_conj_sub]; simp
+theorem inner_self_im (x : E) : im ⟪x, x⟫ = 0 := by
+  rw [← @ofReal_inj 𝕜, im_eq_conj_sub]; simp
 
 theorem inner_add_left (x y z : E) : ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫ :=
   InnerProductSpace.add_left _ _ _
@@ -183,10 +183,10 @@ theorem inner_self_nonneg {x : E} : 0 ≤ re ⟪x, x⟫ :=
 theorem real_inner_self_nonneg {x : F} : 0 ≤ ⟪x, x⟫_ℝ :=
   @inner_self_nonneg ℝ F _ _ _ x
 
-@[simp]
 theorem inner_self_ofReal_re (x : E) : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
   ((RCLike.is_real_TFAE (⟪x, x⟫ : 𝕜)).out 2 3).2 (inner_self_im (𝕜 := 𝕜) x)
 
+@[simp]
 theorem inner_self_eq_norm_sq_to_K (x : E) : ⟪x, x⟫ = (‖x‖ : 𝕜) ^ 2 := by
   rw [← inner_self_ofReal_re, ← norm_sq_eq_re_inner, ofReal_pow]
 
@@ -290,7 +290,6 @@ local notation "⟪" x ", " y "⟫" => inner 𝕜 x y
 
 export InnerProductSpace (norm_sq_eq_re_inner)
 
-@[simp]
 theorem inner_self_eq_zero {x : E} : ⟪x, x⟫ = 0 ↔ x = 0 := by
   rw [inner_self_eq_norm_sq_to_K, sq_eq_zero_iff, ofReal_eq_zero, norm_eq_zero]
 
@@ -313,13 +312,11 @@ theorem ext_iff_inner_right {x y : E} : x = y ↔ ∀ v, ⟪x, v⟫ = ⟪y, v⟫
 
 variable {𝕜}
 
-@[simp]
 theorem re_inner_self_nonpos {x : E} : re ⟪x, x⟫ ≤ 0 ↔ x = 0 := by
-  rw [← norm_sq_eq_re_inner, (sq_nonneg _).ge_iff_eq', sq_eq_zero_iff, norm_eq_zero]
+  simp
 
-@[simp]
 lemma re_inner_self_pos {x : E} : 0 < re ⟪x, x⟫ ↔ x ≠ 0 := by
-  simpa [-re_inner_self_nonpos] using re_inner_self_nonpos (𝕜 := 𝕜) (x := x).not
+  simp [sq_pos_iff]
 
 @[deprecated (since := "2025-04-22")] alias inner_self_nonpos := re_inner_self_nonpos
 @[deprecated (since := "2025-04-22")] alias inner_self_pos := re_inner_self_pos
@@ -744,7 +741,7 @@ theorem inner_eq_norm_mul_iff_div {x y : E} (h₀ : x ≠ 0) :
   · have : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫ : 𝕜) • x :=
       ((norm_inner_eq_norm_tfae 𝕜 x y).out 0 1).1 (by simp [h])
     rw [this.resolve_left h₀, h]
-    simp [norm_smul, inner_self_ofReal_norm, mul_div_cancel_right₀ _ h₀']
+    simp [norm_smul, mul_div_cancel_right₀ _ h₀']
   · conv_lhs => rw [← h, inner_smul_right, inner_self_eq_norm_sq_to_K]
     field
 
@@ -796,6 +793,9 @@ theorem inner_eq_one_iff_of_norm_one {x y : E} (hx : ‖x‖ = 1) (hy : ‖y‖
     ⟪x, y⟫ = 1 ↔ x = y := by
   convert inner_eq_norm_mul_iff (𝕜 := 𝕜) (E := E) using 2 <;> simp [hx, hy]
 
+theorem inner_self_eq_one_of_norm_one {x : E} (hx : ‖x‖ = 1) : ⟪x, x⟫_𝕜 = 1 :=
+  (inner_eq_one_iff_of_norm_one hx hx).mpr rfl
+
 theorem inner_lt_norm_mul_iff_real {x y : F} : ⟪x, y⟫_ℝ < ‖x‖ * ‖y‖ ↔ ‖y‖ • x ≠ ‖x‖ • y :=
   calc
     ⟪x, y⟫_ℝ < ‖x‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ ≠ ‖x‖ * ‖y‖ :=
@@ -813,7 +813,8 @@ theorem eq_of_norm_le_re_inner_eq_norm_sq {x y : E} (hle : ‖x‖ ≤ ‖y‖)
   suffices H : re ⟪x - y, x - y⟫ ≤ 0 by rwa [re_inner_self_nonpos, sub_eq_zero] at H
   have H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2 := by gcongr
   have H₂ : re ⟪y, x⟫ = ‖y‖ ^ 2 := by rwa [← inner_conj_symm, conj_re]
-  simpa [inner_sub_left, inner_sub_right, ← norm_sq_eq_re_inner, h, H₂] using H₁
+  simp only [inner_sub_left, inner_sub_right]
+  simpa [h, H₂] using H₁
 
 /-- Equality is achieved in the triangle inequality iff the two vectors are collinear. -/
 theorem norm_add_eq_iff_real {x y : F} : ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y := by
diff --git a/Mathlib/Analysis/InnerProductSpace/Dual.lean b/Mathlib/Analysis/InnerProductSpace/Dual.lean
@@ -163,7 +163,7 @@ def toDual : E ≃ₗᵢ⋆[𝕜] StrongDual 𝕜 E :=
           ⟪(ℓ z† / ⟪z, z⟫) • z, x⟫ = ℓ z / ⟪z, z⟫ * ⟪z, x⟫ := by simp [inner_smul_left]
           _ = ℓ z * ⟪z, x⟫ / ⟪z, z⟫ := by rw [← div_mul_eq_mul_div]
           _ = ℓ x * ⟪z, z⟫ / ⟪z, z⟫ := by rw [h₂]
-          _ = ℓ x := by field [inner_self_ne_zero.2])
+          _ = ℓ x := by have : ⟪z, z⟫ ≠ 0 := inner_self_ne_zero.mpr z_ne_0; field)
 
 variable {𝕜} {E}
 
diff --git a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean
@@ -78,7 +78,7 @@ theorem posSemidef_gram (v : n → E) :
     PosSemidef (gram 𝕜 v) := by
   refine ⟨isHermitian_gram _ _, fun x ↦ ?_⟩
   rw [star_dotProduct_gram_mulVec, le_iff_re_im]
-  simp [inner_self_nonneg]
+  simp
 
 /-- In a normed space, positive definiteness of `gram 𝕜 v` implies linear independence of `v`. -/
 theorem linearIndependent_of_posDef_gram {v : n → E} (h_gram : PosDef (gram 𝕜 v)) :
diff --git a/Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean b/Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean
@@ -100,4 +100,4 @@ theorem ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection (f : E
     · simpa using f.le_of_opNorm_le hf x
     · have : ∀ y, ⟪f y, x⟫ = ⟪y, x⟫ := by
         simpa [Submodule.mem_orthogonal, inner_sub_left, sub_eq_zero] using hx
-      simp [this, ← norm_sq_eq_re_inner]
+      simp [this]
diff --git a/Mathlib/Analysis/InnerProductSpace/Orthonormal.lean b/Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
@@ -84,7 +84,8 @@ theorem orthonormal_iff_ite [DecidableEq ι] {v : ι → E} :
   · intro h
     constructor
     · intro i
-      have h' : ‖v i‖ ^ 2 = 1 ^ 2 := by simp [@norm_sq_eq_re_inner 𝕜, h i i]
+      have h' : ‖v i‖ ^ 2 = 1 ^ 2 := by
+        rw [@norm_sq_eq_re_inner 𝕜, h i i]; simp
       have h₁ : 0 ≤ ‖v i‖ := norm_nonneg _
       have h₂ : (0 : ℝ) ≤ 1 := zero_le_one
       rwa [sq_eq_sq₀ h₁ h₂] at h'
diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -422,9 +422,8 @@ lemma enorm_eq_one (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
 lemma inner_eq_zero (b : OrthonormalBasis ι 𝕜 E) {i j : ι} (hij : i ≠ j) :
     ⟪b i, b j⟫ = 0 := b.orthonormal.inner_eq_zero hij
 
-@[simp]
 lemma inner_eq_one (b : OrthonormalBasis ι 𝕜 E) (i : ι) : ⟪b i, b i⟫ = 1 := by
-  simp [inner_self_eq_norm_sq_to_K]
+  simp
 
 lemma inner_eq_ite [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i j : ι) :
     ⟪b i, b j⟫ = if i = j then 1 else 0 := by
diff --git a/Mathlib/Analysis/InnerProductSpace/ProdL2.lean b/Mathlib/Analysis/InnerProductSpace/ProdL2.lean
@@ -29,7 +29,7 @@ noncomputable instance instProdInnerProductSpace :
     InnerProductSpace 𝕜 (WithLp 2 (E × F)) where
   inner x y := ⟪x.fst, y.fst⟫_𝕜 + ⟪x.snd, y.snd⟫_𝕜
   norm_sq_eq_re_inner x := by
-    simp [prod_norm_sq_eq_of_L2, ← norm_sq_eq_re_inner]
+    simp [prod_norm_sq_eq_of_L2]
   conj_inner_symm x y := by
     simp
   add_left x y z := by
diff --git a/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean b/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
@@ -144,7 +144,7 @@ theorem eq_smul_self_of_isLocalExtrOn_real (hT : IsSelfAdjoint T) {x₀ : F}
   set c : ℝ := -b⁻¹ * a
   convert hc
   have := congr_arg (fun x => ⟪x, x₀⟫_ℝ) hc
-  simp [field, inner_smul_left, real_inner_self_eq_norm_mul_norm, mul_comm a] at this ⊢
+  simp [field, inner_smul_left, mul_comm a] at this ⊢
   exact this
 
 end Real
diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean
@@ -64,6 +64,7 @@ instance instInner : Inner 𝕜 (E ⊗[𝕜] F) := ⟨fun x y => inner_ x y⟩
 
 private lemma inner_def (x y : E ⊗[𝕜] F) : inner 𝕜 x y = inner_ x y := rfl
 
+variable (𝕜) in
 @[simp] theorem inner_tmul (x x' : E) (y y' : F) :
     inner 𝕜 (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') = inner 𝕜 x x' * inner 𝕜 y y' := rfl
 
@@ -139,7 +140,7 @@ instance instInnerProductSpace : InnerProductSpace 𝕜 (E ⊗[𝕜] F) := .ofCo
 
 @[simp] theorem norm_tmul (x : E) (y : F) :
     ‖x ⊗ₜ[𝕜] y‖ = ‖x‖ * ‖y‖ := by
-  simp [norm_eq_sqrt_re_inner (𝕜 := 𝕜), Real.sqrt_mul inner_self_nonneg]
+  simpa using congr(√(RCLike.re $(inner_tmul 𝕜 x x y y)))
 
 @[simp] theorem nnnorm_tmul (x : E) (y : F) :
     ‖x ⊗ₜ[𝕜] y‖₊ = ‖x‖₊ * ‖y‖₊ := by simp [← NNReal.coe_inj]
diff --git a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean
@@ -349,8 +349,8 @@ theorem inner_mul_inner_add_areaForm_mul_areaForm' (a x : E) :
   apply (o.basisRightAngleRotation a ha).ext
   intro i
   fin_cases i
-  · simp [real_inner_self_eq_norm_sq, mul_comm, real_inner_comm]
-  · simp [real_inner_self_eq_norm_sq, mul_comm, o.areaForm_swap a x]
+  · simp [mul_comm, real_inner_comm]
+  · simp [mul_comm, o.areaForm_swap a x]
 
 /-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫`. -/
 theorem inner_mul_inner_add_areaForm_mul_areaForm (a x y : E) :
@@ -368,8 +368,8 @@ theorem inner_mul_areaForm_sub' (a x : E) : ⟪a, x⟫ • ω a - ω a x • inn
   apply (o.basisRightAngleRotation a ha).ext
   intro i
   fin_cases i
-  · simp [real_inner_self_eq_norm_sq, mul_comm, o.areaForm_swap a x]
-  · simp [real_inner_self_eq_norm_sq, mul_comm, real_inner_comm]
+  · simp [mul_comm, o.areaForm_swap a x]
+  · simp [mul_comm, real_inner_comm]
 
 /-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y`. -/
 theorem inner_mul_areaForm_sub (a x y : E) : ⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y :=
@@ -420,7 +420,7 @@ theorem kahler_swap (x y : E) : o.kahler x y = conj (o.kahler y x) := by
 
 @[simp]
 theorem kahler_apply_self (x : E) : o.kahler x x = ‖x‖ ^ 2 := by
-  simp [kahler_apply_apply, real_inner_self_eq_norm_sq]
+  simp [kahler_apply_apply]
 
 @[simp]
 theorem kahler_rightAngleRotation_left (x y : E) :
diff --git a/Mathlib/Analysis/InnerProductSpace/l2Space.lean b/Mathlib/Analysis/InnerProductSpace/l2Space.lean
@@ -115,7 +115,7 @@ instance instInnerProductSpace : InnerProductSpace 𝕜 (lp G 2) :=
         ‖f‖ ^ 2 = ‖f‖ ^ (2 : ℝ≥0∞).toReal := by norm_cast
         _ = ∑' i, ‖f i‖ ^ (2 : ℝ≥0∞).toReal := lp.norm_rpow_eq_tsum ?_ f
         _ = ∑' i, ‖f i‖ ^ (2 : ℕ) := by norm_cast
-        _ = ∑' i, re ⟪f i, f i⟫ := by simp [norm_sq_eq_re_inner (𝕜 := 𝕜)]
+        _ = ∑' i, re ⟪f i, f i⟫ := by simp
         _ = re (∑' i, ⟪f i, f i⟫) := (RCLike.reCLM.map_tsum ?_).symm
       · norm_num
       · exact summable_inner f f
diff --git a/Mathlib/Analysis/Quaternion.lean b/Mathlib/Analysis/Quaternion.lean
@@ -82,7 +82,7 @@ theorem nnnorm_star (a : ℍ) : ‖star a‖₊ = ‖a‖₊ :=
 
 noncomputable instance : NormedDivisionRing ℍ where
   dist_eq _ _ := rfl
-  norm_mul _ _ := by simp [norm_eq_sqrt_real_inner, inner_self]
+  norm_mul _ _ := by simp_rw [norm_eq_sqrt_real_inner, inner_self]; simp
 
 noncomputable instance : NormedAlgebra ℝ ℍ where
   norm_smul_le := norm_smul_le
diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean
@@ -235,6 +235,14 @@ theorem smul_im (r : ℝ) (z : K) : im (r • z) = r * im z := by
 theorem norm_ofReal (r : ℝ) : ‖(r : K)‖ = |r| :=
   norm_algebraMap' K r
 
+@[simp]
+theorem re_ofReal_pow (a : ℝ) (n : ℕ) : re ((a : K) ^ n) = a ^ n := by
+  rw [← ofReal_pow, @ofReal_re]
+
+@[simp]
+theorem im_ofReal_pow (a : ℝ) (n : ℕ) : im ((a : K) ^ n) = 0 := by
+  rw [← @ofReal_pow, @ofReal_im_ax]
+
 /-! ### Characteristic zero -/
 
 -- see Note [lower instance priority]
diff --git a/Mathlib/Geometry/Euclidean/Inversion/Calculus.lean b/Mathlib/Geometry/Euclidean/Inversion/Calculus.lean
@@ -100,7 +100,7 @@ theorem hasFDerivAt_inversion (hx : x ≠ c) :
     (LinearMap.eqOn_span' ?_) fun y hy ↦ ?_)
   · have : ((‖x‖ ^ 2) ^ 2)⁻¹ * (‖x‖ ^ 2) = (‖x‖ ^ 2)⁻¹ := by
       rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']
-    simp [Submodule.reflection_orthogonalComplement_singleton_eq_neg, real_inner_self_eq_norm_sq,
+    simp [Submodule.reflection_orthogonalComplement_singleton_eq_neg,
       two_mul, this, div_eq_mul_inv, mul_add, add_smul, mul_pow]
   · simp [Submodule.mem_orthogonal_singleton_iff_inner_right.1 hy,
       Submodule.reflection_mem_subspace_eq_self hy, div_eq_mul_inv, mul_pow]
diff --git a/Mathlib/Geometry/Euclidean/Triangle.lean b/Mathlib/Geometry/Euclidean/Triangle.lean
@@ -73,8 +73,9 @@ theorem sin_angle_mul_norm_eq_sin_angle_mul_norm (x y : V) :
       Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) := by
     simp [field, mul_assoc, sin_angle_mul_norm_mul_norm]
   rw [h_sin x y hx hy, h_sin y (x - y) hy (sub_ne_zero_of_ne hxy)]
+  simp only [inner_sub_left, inner_sub_right, real_inner_comm x y]
   have hsub : x - y ≠ 0 := sub_ne_zero_of_ne hxy
-  simp [field, inner_sub_left, inner_sub_right, real_inner_comm x y]
+  field_simp
   ring_nf
 
 /-- A variant of the law of sines, (two given sides are nonzero), vector angle form. -/
diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean
@@ -233,7 +233,7 @@ theorem stereo_right_inv (hv : ‖v‖ = 1) (w : (ℝ ∙ v)ᗮ) : stereoToFun v
   have h₁ : (ℝ ∙ v)ᗮ.orthogonalProjection v = 0 :=
     Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero v
   have h₂ : ⟪v, w⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
-  have h₃ : ⟪v, v⟫ = 1 := by simp [real_inner_self_eq_norm_mul_norm, hv]
+  have h₃ : ⟪v, v⟫ = 1 := by simp [hv]
   rw [h₁, h₂, h₃]
   match_scalars
   simp [field]
diff --git a/Mathlib/Topology/VectorBundle/Riemannian.lean b/Mathlib/Topology/VectorBundle/Riemannian.lean
@@ -204,8 +204,7 @@ lemma eventually_norm_symmL_trivializationAt_self_comp_lt (x : B) {r : ℝ} (hr
       grw [← le_opNorm]
       simp
     _ = δ * C * ‖G.symm w‖^2 + g' y w w := by ring
-    _ = δ * C * g x (G.symm w) (G.symm w) + g' y w w := by
-      simp [← real_inner_self_eq_norm_sq, hg]
+    _ = δ * C * g x (G.symm w) (G.symm w) + g' y w w := by simp [← hg]
     _ = δ * C * g' x w w + g' y w w := by
       rw [← hgx]; rfl
   have : (1 - δ * C) * g' x w w ≤ g' y w w := by linarith
@@ -309,8 +308,7 @@ lemma eventually_norm_symmL_trivializationAt_comp_self_lt (x : B) {r : ℝ} (hr
       grw [← le_opNorm]
       simp
     _ = δ * C * ‖G.symm w‖^2 + g' x w w := by ring
-    _ = δ * C * g x (G.symm w) (G.symm w) + g' x w w := by
-      simp [← real_inner_self_eq_norm_sq, hg]
+    _ = δ * C * g x (G.symm w) (G.symm w) + g' x w w := by simp [← hg]
     _ = δ * C * g' x w w + g' x w w := by
       congr
       rw [inCoordinates_apply_eq₂ h'x h'x (Set.mem_univ _)]
