-- Mathlib/Analysis/InnerProductSpace/Defs.lean
/-- An auxiliary equality useful to prove the **Cauchy–Schwarz inequality**. Here we use the
standard argument involving the discriminant of quadratic form. -/
lemma cauchy_schwarz_aux' (x y : F) (t : ℝ) : 0 ≤ normSqF x * t * t + 2 * re ⟪x, y⟫ * t
    + normSqF y

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

Tactic:
rw
[re_inner_smul_ofReal_smul_self, inner_smul_ofReal_left, inner_smul_ofReal_right]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ re (⟪↑t • x, ↑t • x⟫_𝕜 + ⟪↑t • x, y⟫_𝕜 + ⟪y, ↑t • x⟫_𝕜 + ⟪y, y⟫_𝕜) =
    re ⟪↑t • x, ↑t • x⟫_𝕜 + re ⟪↑t • x, y⟫_𝕜 + re ⟪y, ↑t • x⟫_𝕜 + re ⟪y, y⟫_𝕜

Tactic:
simp only [map_add]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ normSq x * t * t + re ⟪x, y⟫_𝕜 * t + re ⟪y, x⟫_𝕜 * t + normSq y =
    normSq x * t * t + re ⟪x, y⟫_𝕜 * t + re ⟪x, y⟫_𝕜 * t + normSq y

Tactic:
rw [inner_re_symm]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ normSq x * t * t + re ⟪x, y⟫_𝕜 * t + re ⟪y, x⟫_𝕜 * t + re ⟪y, y⟫_𝕜 =
    normSq x * t * t + re ⟪x, y⟫_𝕜 * t + re ⟪y, x⟫_𝕜 * t + normSq y

Tactic:
rw [← normSq]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ 0 ≤ normSq x * t * t + 2 * re ⟪x, y⟫_𝕜 * t + normSq y

Tactic:
calc 0 ≤ re ⟪(ofReal t : 𝕜) • x + y, (ofReal t : 𝕜) • x + y⟫ := inner_self_nonneg
_ = re (⟪(ofReal t : 𝕜) • x, (ofReal t : 𝕜) • x⟫ + ⟪(ofReal t : 𝕜) • x, y⟫
    + ⟪y, (ofReal t : 𝕜) • x⟫ + ⟪y, y⟫) := by rw [inner_add_add_self ((ofReal t : 𝕜) • x) y]
_ = re ⟪(ofReal t : 𝕜) • x, (ofReal t : 𝕜) • x⟫
    + re ⟪(ofReal t : 𝕜) • x, y⟫ + re ⟪y, (ofReal t : 𝕜) • x⟫ + re ⟪y, y⟫ := by
    simp only [map_add]
_ = normSq x * t * t + re (⟪x, y⟫ * t) + re (⟪y, x⟫ * t) + re ⟪y, y⟫ := by rw
  [re_inner_smul_ofReal_smul_self, inner_smul_ofReal_left, inner_smul_ofReal_right]
_ = normSq x * t * t + re ⟪x, y⟫ * t + re ⟪y, x⟫ * t + re ⟪y, y⟫ := by rw [mul_comm ⟪x,y⟫ _,
  RCLike.re_ofReal_mul, mul_comm t _, mul_comm ⟪y,x⟫ _, RCLike.re_ofReal_mul, mul_comm t _]
_ = normSq x * t * t + re ⟪x, y⟫ * t + re ⟪y, x⟫ * t + normSq y := by rw [← normSq]
_ = normSq x * t * t + re ⟪x, y⟫ * t + re ⟪x, y⟫ * t + normSq y := by rw [inner_re_symm]
_ = normSq x * t * t + 2 * re ⟪x, y⟫ * t + normSq y := by ring

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ re ⟪↑t • x + y, ↑t • x + y⟫_𝕜 = re (⟪↑t • x, ↑t • x⟫_𝕜 + ⟪↑t • x, y⟫_𝕜 + ⟪y, ↑t • x⟫_𝕜 + ⟪y, y⟫_𝕜)

Tactic:
rw [inner_add_add_self ((ofReal t : 𝕜) • x) y]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ normSq x * t * t + re ⟪x, y⟫_𝕜 * t + re ⟪x, y⟫_𝕜 * t + normSq y = normSq x * t * t + 2 * re ⟪x, y⟫_𝕜 * t + normSq y

Tactic:
ring

Result:
no goals

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

Tactic:
rw [mul_comm ⟪x,y⟫ _,
RCLike.re_ofReal_mul, mul_comm t _, mul_comm ⟪y,x⟫ _, RCLike.re_ofReal_mul, mul_comm t _]

Result:
no goals