-- 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
hs : ¬s = 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
suffices
    (B (r • x) (r • x)) * (B (s • y) (s • y)) = (B (r • x) (s • y)) * (B (s • y) (r • x)) by
  simp only [map_smul, smul_apply, smul_eq_mul] at this
  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
  have hrs : r * r * s * s ≠ 0 := by simp [hr, hs]
  exact le_of_eq <| mul_right_injective₀ hrs this

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

Proof state:
case mpr
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) x * (B y) y ≤ (B x) y * (B y) x → ¬LinearIndependent R ![x, y]

Tactic:
intro h

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

Proof state:
case mpr
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 : (B x) x * (B y) y ≤ (B x) y * (B y) x
⊢ ¬LinearIndependent R ![x, y]

Tactic:
refine not_linearIndependent_of_apply_mul_apply_eq B hp x y (le_antisymm
  (apply_mul_apply_le_of_forall_zero_le B hle x y) h)

Result:
no goals

Proof state:
case mpr
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) y * (B y) x < (B x) x * (B y) y

Tactic:
contrapose!

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

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

Tactic:
simp [hz]

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

Tactic:
constructor

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

case mpr
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) y * (B y) x < (B x) x * (B y) 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
hs : ¬s = 0
⊢ (B (r • x)) (r • x) * (B (s • y)) (s • y) = (B (r • x)) (s • y) * (B (s • y)) (r • x)

Tactic:
simp [show s • y = - r • x by rwa [neg_smul, ← add_eq_zero_iff_eq_neg']]

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

Tactic:
contrapose!

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
⊢ ¬LinearIndependent R ![x, y] → (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 : R), s • x + t • y = 0 → s = 0 ∧ t = 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

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

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

Tactic:
exact le_of_lt (hp z hz)

Result:
no goals