-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem cauchy_schwarz_aux (x y : F) : normSqF (⟪x, y⟫ • x - ⟪x, x⟫ • y)
    = normSqF x * (normSqF x * normSqF y - ‖⟪x, y⟫‖ ^ 2)

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ normSq (⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y) = normSq x * (normSq x * normSq y - ‖⟪x, y⟫_𝕜‖ ^ 2)

Tactic:
rw [← @ofReal_inj 𝕜, ofReal_normSq_eq_inner_self]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y, ⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y⟫_𝕜 = ↑(normSq x * (normSq x * normSq y - ‖⟪x, y⟫_𝕜‖ ^ 2))

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ↑‖⟪x, y⟫_𝕜‖ ^ 2 * ↑(normSq x) - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2 - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2 +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x * (normSq x * normSq y) - normSq x * ‖⟪x, y⟫_𝕜‖ ^ 2)

Tactic:
push_cast

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ↑‖⟪x, y⟫_𝕜‖ ^ 2 * ↑(normSq x) - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2 - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2 +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, y⟫_𝕜 * ((starRingEnd 𝕜) ⟪x, y⟫_𝕜 * ↑(normSq x)) - ↑(normSq x) * ((starRingEnd 𝕜) ⟪x, y⟫_𝕜 * ⟪x, y⟫_𝕜) -
        ⟪x, y⟫_𝕜 * (↑(normSq x) * ⟪y, x⟫_𝕜) +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x * (normSq x * normSq y) - normSq x * ‖⟪x, y⟫_𝕜‖ ^ 2)

Tactic:
rw [← mul_assoc, mul_conj, RCLike.conj_mul, mul_left_comm, ← inner_conj_symm y, mul_conj]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ↑‖⟪x, y⟫_𝕜‖ ^ 2 * ↑(normSq x) - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2 - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2 +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x * (normSq x * normSq y) - normSq x * ‖⟪x, y⟫_𝕜‖ ^ 2)

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y, ⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y⟫_𝕜 = ↑(normSq x * (normSq x * normSq y - ‖⟪x, y⟫_𝕜‖ ^ 2))

Tactic:
simp only [inner_sub_sub_self, inner_smul_left, inner_smul_right, conj_ofReal, mul_sub, ←
  ofReal_normSq_eq_inner_self x, ← ofReal_normSq_eq_inner_self y]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, y⟫_𝕜 * ((starRingEnd 𝕜) ⟪x, y⟫_𝕜 * ↑(normSq x)) - ↑(normSq x) * ((starRingEnd 𝕜) ⟪x, y⟫_𝕜 * ⟪x, y⟫_𝕜) -
        ⟪x, y⟫_𝕜 * (↑(normSq x) * ⟪y, x⟫_𝕜) +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x * (normSq x * normSq y) - normSq x * ‖⟪x, y⟫_𝕜‖ ^ 2)

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ↑‖⟪x, y⟫_𝕜‖ ^ 2 * ↑(normSq x) - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2 - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2 +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2

Tactic:
ring

Result:
no goals