-- Mathlib/LinearAlgebra/SesquilinearForm.lean
/-- The **Cauchy-Schwarz inequality** for positive semidefinite forms. -/
lemma apply_mul_apply_le_of_forall_zero_le (hs : ∀ x, 0 ≤ B x x) (x y : M) :
    (B x y) * (B y x) ≤ (B x x) * (B y y)

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
have aux (x y : M) : 0 ≤ (B x x) * ((B x x) * (B y y) - (B x y) * (B y x)) := by
  rw [← apply_smul_sub_smul_sub_eq B x y]
  exact hs (B x y • x - B x x • y)

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Proof state:
case inr.inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
suffices B x y = - B y x by simpa [this, hx, hy] using mul_self_nonneg (B y x)

Result:
case inr.inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ (B x) y = -(B y) x

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x✝ y✝ x y : M
⊢ 0 ≤ (B ((B x) y • x - (B x) x • y)) ((B x) y • x - (B x) x • y)

Tactic:
exact hs (B x y • x - B x x • y)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
rcases lt_or_le 0 (B x x) with hx | hx

Result:
case inl
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : 0 < (B x) x
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

case inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x ≤ 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
this : (B x) y = -(B y) x
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
simpa [this, hx, hy] using mul_self_nonneg (B y x)

Result:
no goals

Proof state:
case inr.inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ (B x) y + (B y) x = 0

Tactic:
apply le_antisymm

Result:
case inr.inr.a
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ (B x) y + (B y) x ≤ 0

case inr.inr.a
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ 0 ≤ (B x) y + (B y) x

Proof state:
case inr.inr.a
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ (B x) y + (B y) x ≤ 0

Tactic:
simpa [hx, hy, le_neg_iff_add_nonpos_left] using hs (x - y)

Result:
no goals

Proof state:
case inr.inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y ≤ 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
replace hy : B y y = 0 := le_antisymm hy (hs y)

Result:
case inr.inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Proof state:
case inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
rcases lt_or_le 0 (B y y) with hy | hy

Result:
case inr.inl
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : 0 < (B y) y
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

case inr.inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y ≤ 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Proof state:
case inr.inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ (B x) y = -(B y) x

Tactic:
rw [eq_neg_iff_add_eq_zero]

Result:
case inr.inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ (B x) y + (B y) x = 0

Proof state:
case inr.inr.a
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ 0 ≤ (B x) y + (B y) x

Tactic:
simpa [hx, hy] using hs (x + y)

Result:
no goals