case inl
𝕜 : Type u_1
E : Type ?u.652623
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
y : F
⊢ ‖inner 0 y‖ * ‖inner y 0‖ ≤ ↑re (inner 0 0) * ↑re (inner y y)

case inr
𝕜 : Type u_1
E : Type ?u.652623
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
hx : x ≠ 0
⊢ ‖inner x y‖ * ‖inner y x‖ ≤ ↑re (inner x x) * ↑re (inner y y)
𝕜 : Type u_1
E : Type ?u.652623
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ ‖inner x y‖ * ‖inner y x‖ ≤ ↑re (inner x x) * ↑re (inner y y)
rcases eq_or_ne x 0 with (rfl | hx)
no goals
case inl
𝕜 : Type u_1
E : Type ?u.652623
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
y : F
⊢ ‖inner 0 y‖ * ‖inner y 0‖ ≤ ↑re (inner 0 0) * ↑re (inner y y)
simpa only [inner_zero_left, map_zero, MulZeroClass.zero_mul, norm_zero] using le_rfl
case inr
𝕜 : Type u_1
E : Type ?u.652623
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
hx : x ≠ 0
hx' : 0 < normSq x
⊢ ‖inner x y‖ * ‖inner y x‖ ≤ ↑re (inner x x) * ↑re (inner y y)
case inr
𝕜 : Type u_1
E : Type ?u.652623
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
hx : x ≠ 0
⊢ ‖inner x y‖ * ‖inner y x‖ ≤ ↑re (inner x x) * ↑re (inner y y)
have hx' : 0 < normSqF x := inner_self_nonneg.lt_of_ne' (mt normSq_eq_zero.1 hx)
case inr
𝕜 : Type u_1
E : Type ?u.652623
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
hx : x ≠ 0
hx' : 0 < normSq x
⊢ 0 ≤ normSq (inner x y • x - inner x x • y)
case inr
𝕜 : Type u_1
E : Type ?u.652623
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
hx : x ≠ 0
hx' : 0 < normSq x
⊢ ‖inner x y‖ * ‖inner y x‖ ≤ ↑re (inner x x) * ↑re (inner y y)
rw [← sub_nonneg, ← mul_nonneg_iff_right_nonneg_of_pos hx', ← normSq, ← normSq,
  norm_inner_symm y, ← sq, ← cauchy_schwarz_aux]
no goals
case inr
𝕜 : Type u_1
E : Type ?u.652623
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
hx : x ≠ 0
hx' : 0 < normSq x
⊢ 0 ≤ normSq (inner x y • x - inner x x • y)
exact inner_self_nonneg