-- 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 h.e'_4.h.e'_5.h.e'_6
𝕜 : 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
⊢ 2 * ‖⟪x, y⟫_𝕜‖ * t * ‖⟪x, y⟫_𝕜‖ = 2 * ‖⟪x, y⟫_𝕜‖ ^ 2 * t

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 : ℝ
⊢ 0 ≤ normSq x * (t * t) + 2 * ‖⟪x, y⟫_𝕜‖ * t + normSq y

Tactic:
by_cases hzero : ⟪x, y⟫ = 0

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 * t) + 2 * ‖⟪x, y⟫_𝕜‖ * t + normSq y

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

Proof state:
case h.e'_4.h.e'_5.h.e'_6
𝕜 : 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
⊢ 2 * ‖⟪x, y⟫_𝕜‖ * t * ‖⟪x, y⟫_𝕜‖ = 2 * re ⟪⟪x, y⟫_𝕜 • x, y⟫_𝕜 * t

Tactic:
rw [inner_smul_left, mul_comm _ ⟪x, y⟫_𝕜, mul_conj, ← ofReal_pow, ofReal_re]

Result:
case h.e'_4.h.e'_5.h.e'_6
𝕜 : 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
⊢ 2 * ‖⟪x, y⟫_𝕜‖ * t * ‖⟪x, y⟫_𝕜‖ = 2 * ‖⟪x, y⟫_𝕜‖ ^ 2 * t

Proof state:
case h.e'_4.h.e'_5.h.e'_6
𝕜 : 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
⊢ 2 * ‖⟪x, y⟫_𝕜‖ * t = 2 * re ⟪⟪x, y⟫_𝕜 • x, y⟫_𝕜 * (t / ‖⟪x, y⟫_𝕜‖)

Tactic:
field_simp

Result:
case h.e'_4.h.e'_5.h.e'_6
𝕜 : 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
⊢ 2 * ‖⟪x, y⟫_𝕜‖ * t * ‖⟪x, y⟫_𝕜‖ = 2 * re ⟪⟪x, y⟫_𝕜 • x, y⟫_𝕜 * 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) = normSq (⟪x, y⟫_𝕜 • x) * (t / ‖⟪x, y⟫_𝕜‖) * (t / ‖⟪x, y⟫_𝕜‖)

Tactic:
field_simp

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
⊢ normSq x * (t * t) * (‖⟪x, y⟫_𝕜‖ * ‖⟪x, y⟫_𝕜‖) = normSq (⟪x, y⟫_𝕜 • x) * t * t

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 ^ 2 + normSq y

Tactic:
obtain ⟨hx, hy⟩ : (0 ≤ normSqF x ∧ 0 ≤ normSqF y) := ⟨inner_self_nonneg, inner_self_nonneg⟩

Result:
case pos.intro
𝕜 : 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
hx : 0 ≤ normSq x
hy : 0 ≤ normSq y
⊢ 0 ≤ normSq x * t ^ 2 + 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⟫_𝕜‖) = ‖⟪x, y⟫_𝕜‖ * ‖⟪x, y⟫_𝕜‖ * re ⟪x, x⟫_𝕜 * t * t

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
⊢ ‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖ ≤ re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜

Tactic:
suffices discrim (normSqF x) (2 * ‖⟪x, y⟫_𝕜‖) (normSqF y) ≤ 0 by
  rw [norm_inner_symm y x]
  rw [discrim, normSq, normSq, sq] at this
  linarith

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

Proof state:
case pos.intro
𝕜 : 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
hx : 0 ≤ normSq x
hy : 0 ≤ normSq y
⊢ 0 ≤ normSq x * t ^ 2 + normSq y

Tactic:
positivity

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
⊢ discrim (normSq x) (2 * ‖⟪x, y⟫_𝕜‖) (normSq y) ≤ 0

Tactic:
refine discrim_le_zero fun t ↦ ?_

Result:
𝕜 : 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 * ‖⟪x, y⟫_𝕜‖ * t + normSq 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
this : discrim (normSq x) (2 * ‖⟪x, y⟫_𝕜‖) (normSq y) ≤ 0
⊢ ‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖ ≤ re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜

Tactic:
rw [norm_inner_symm y x]

Result:
𝕜 : 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⟫_𝕜

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⟫_𝕜‖ ^ 2 * ⟪x, x⟫_𝕜) * t * t

Tactic:
nth_rw 2 [sq]

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⟫_𝕜‖ * ↑‖⟪x, y⟫_𝕜‖ * ⟪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 : 2 * ‖⟪x, y⟫_𝕜‖ * (2 * ‖⟪x, y⟫_𝕜‖) - 4 * re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜 ≤ 0
⊢ ‖⟪x, y⟫_𝕜‖ * ‖⟪x, y⟫_𝕜‖ ≤ re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜

Tactic:
linarith

Result:
no goals

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
hzero' : ‖⟪x, y⟫_𝕜‖ ≠ 0
⊢ 0 ≤ normSq x * (t * t) + 2 * ‖⟪x, y⟫_𝕜‖ * t + normSq y

Tactic:
convert cauchy_schwarz_aux' (𝕜 := 𝕜) (⟪x, y⟫ • x) y (t / ‖⟪x, y⟫‖) using 3

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
⊢ normSq x * (t * t) = normSq (⟪x, y⟫_𝕜 • x) * (t / ‖⟪x, y⟫_𝕜‖) * (t / ‖⟪x, y⟫_𝕜‖)

case h.e'_4.h.e'_5.h.e'_6
𝕜 : 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
⊢ 2 * ‖⟪x, y⟫_𝕜‖ * t = 2 * re ⟪⟪x, y⟫_𝕜 • x, y⟫_𝕜 * (t / ‖⟪x, y⟫_𝕜‖)