-- Mathlib/LinearAlgebra/SesquilinearForm.lean
/-- Strict **Cauchy-Schwarz** is equivalent to linear independence for positive definite forms. -/
lemma apply_mul_apply_lt_iff_linearIndependent [NoZeroSMulDivisors R M]
    (hp : ∀ x, x ≠ 0 → 0 < B x x) (x y : M) :
    (B x y) * (B y x) < (B x x) * (B y y) ↔ LinearIndependent R ![x, y]

Proof state:
case mp.intro.intro.intro
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
by_cases hr : r = 0

Result:
case pos
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : r = 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

case neg
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
⊢ (B x) x * (B y) y ≤ (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
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y z : M
⊢ 0 ≤ (B z) z

Tactic:
by_cases hz : z = 0

Result:
case pos
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y z : M
hz : z = 0
⊢ 0 ≤ (B z) z

case neg
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y z : M
hz : ¬z = 0
⊢ 0 ≤ (B z) z

Proof state:
case pos
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : s = 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
simp_all

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
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this : r * r * s * s * ((B x) x * (B y) y) = r * r * s * s * ((B x) y * (B y) x)
⊢ r * r * s * s ≠ 0

Tactic:
simp [hr, hs]

Result:
no goals

Proof state:
case mp
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
h : ¬LinearIndependent R ![x, y]
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
rw [LinearIndependent.pair_iff] at h

Result:
case mp
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
h : ¬∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
⊢ (B x) x * (B y) y ≤ (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
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this : r * (r * (B x) x) * (s * (s * (B y) y)) = s * (r * (B x) y) * (r * (s * (B y) x))
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
rw [show r * (r * (B x) x) * (s * (s * (B y) y)) = (r * r * s * s) * ((B x) x * (B y) y) by
  ring, show s * (r * (B x) y) * (r * (s * (B y) x)) = (r * r * s * s) * ((B x) y * (B y) x)
  by ring] at this

Result:
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this : r * r * s * s * ((B x) x * (B y) y) = r * r * s * s * ((B x) y * (B y) x)
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Proof state:
case pos
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : r = 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
simp_all

Result:
no goals