-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_mul_inner_self_le (x y : F) : ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖ ≤ re ⟪x, x⟫ * re ⟪y, y⟫

Proof state:
case neg
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫_𝕜 = 0
⊢ 0 ≤ normSq x * (t * t) + 2 * ‖⟪x, y⟫_𝕜‖ * t + normSq y

Tactic:
have hzero' : ‖⟪x, y⟫‖ ≠ 0 := norm_ne_zero_iff.2 hzero

Result:
case neg
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫_𝕜 = 0
hzero' : ‖⟪x, y⟫_𝕜‖ ≠ 0
⊢ 0 ≤ normSq x * (t * t) + 2 * ‖⟪x, y⟫_𝕜‖ * t + normSq y

Proof state:
case h.e'_4.h.e'_5.h.e'_5
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫_𝕜 = 0
hzero' : ‖⟪x, y⟫_𝕜‖ ≠ 0
⊢ re ⟪x, x⟫_𝕜 * t ^ 2 * (‖⟪x, y⟫_𝕜‖ * ‖⟪x, y⟫_𝕜‖) = re (↑‖⟪x, y⟫_𝕜‖ * ↑‖⟪x, y⟫_𝕜‖ * ⟪x, x⟫_𝕜) * t * t

Tactic:
rw [← ofReal_mul, re_ofReal_mul]

Result:
case h.e'_4.h.e'_5.h.e'_5
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫_𝕜 = 0
hzero' : ‖⟪x, y⟫_𝕜‖ ≠ 0
⊢ re ⟪x, x⟫_𝕜 * t ^ 2 * (‖⟪x, y⟫_𝕜‖ * ‖⟪x, y⟫_𝕜‖) = ‖⟪x, y⟫_𝕜‖ * ‖⟪x, y⟫_𝕜‖ * re ⟪x, x⟫_𝕜 * t * t

Proof state:
case h.e'_4.h.e'_5.h.e'_5
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫_𝕜 = 0
hzero' : ‖⟪x, y⟫_𝕜‖ ≠ 0
⊢ normSq x * (t * t) * (‖⟪x, y⟫_𝕜‖ * ‖⟪x, y⟫_𝕜‖) = normSq (⟪x, y⟫_𝕜 • x) * t * t

Tactic:
rw [← sq, normSq, normSq, inner_smul_right, inner_smul_left, ← mul_assoc _ _ ⟪x, x⟫,
  mul_conj]

Result:
case h.e'_4.h.e'_5.h.e'_5
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫_𝕜 = 0
hzero' : ‖⟪x, y⟫_𝕜‖ ≠ 0
⊢ re ⟪x, x⟫_𝕜 * t ^ 2 * (‖⟪x, y⟫_𝕜‖ * ‖⟪x, y⟫_𝕜‖) = re (↑‖⟪x, y⟫_𝕜‖ ^ 2 * ⟪x, x⟫_𝕜) * t * t

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

Tactic:
rw [discrim, normSq, normSq, sq] at this

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
this : 2 * ‖⟪x, y⟫_𝕜‖ * (2 * ‖⟪x, y⟫_𝕜‖) - 4 * re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜 ≤ 0
⊢ ‖⟪x, y⟫_𝕜‖ * ‖⟪x, y⟫_𝕜‖ ≤ re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜

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

Tactic:
simp only [mul_assoc, ← sq, hzero, norm_zero, mul_zero, zero_mul, add_zero, ge_iff_le]

Result:
case pos
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ⟪x, y⟫_𝕜 = 0
⊢ 0 ≤ normSq x * t ^ 2 + normSq y