-- 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 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

Tactic:
by_cases hs : s = 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
hs : s = 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
hs : ¬s = 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
⊢ s • y = -r • x

Tactic:
rwa [neg_smul, ← add_eq_zero_iff_eq_neg']

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)
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
have hrs : r * r * s * s ≠ 0 := by simp [hr, hs]

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)
hrs : r * r * s * s ≠ 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))
⊢ r * (r * (B x) x) * (s * (s * (B y) y)) = r * r * s * s * ((B x) x * (B y) y)

Tactic:
ring

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
⊢ ∀ (z : M), 0 ≤ (B z) z

Tactic:
intro z

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 z : M
⊢ 0 ≤ (B z) z

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) = s * (r * (B x) y) * (r * (s * (B y) x))
⊢ s * (r * (B x) y) * (r * (s * (B y) x)) = r * r * s * s * ((B x) y * (B y) x)

Tactic:
ring

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)
hrs : r * r * s * s ≠ 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
exact le_of_eq <| mul_right_injective₀ hrs this

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
⊢ ¬LinearIndependent R ![x, y] → (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
intro 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 : ¬LinearIndependent R ![x, y]
⊢ (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
⊢ (B x) y * (B y) x < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Tactic:
have hle : ∀ z, 0 ≤ B z z := by
  intro z
  by_cases hz : z = 0; simp [hz]
  exact le_of_lt (hp z hz)

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
⊢ (B x) y * (B y) x < (B x) x * (B y) y ↔ LinearIndependent R ![x, 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
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 : (B (r • x)) (r • x) * (B (s • y)) (s • y) = (B (r • x)) (s • y) * (B (s • y)) (r • x)
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
simp only [map_smul, smul_apply, smul_eq_mul] 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 * (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

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 : ∃ s t, s • x + t • y = 0 ∧ (s = 0 → t ≠ 0)
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
obtain ⟨r, s, hl, h0⟩ := h

Result:
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