-- Mathlib/LinearAlgebra/Ray.lean
theorem sameRay_or_sameRay_neg_iff_not_linearIndependent {x y : M} :
    SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Proof state:
case neg.refine_1.inl.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hx0 : x = 0
⊢ ∃ g, ∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
exact False.elim (hx hx0)

Result:
no goals

Proof state:
case neg.refine_2.intro.intro.inr.inr.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ m 0 • x = m 1 • -y

Tactic:
rwa [smul_neg]

Result:
no goals

Proof state:
case neg.refine_1.inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ ![r₁, r₂] 0 • ![x, y] 0 + ![r₁, r₂] 1 • ![x, y] 1 = 0 ∧ (![r₁, r₂] 0 ≠ 0 ∨ ![r₁, r₂] 1 ≠ 0)

Tactic:
simp [h, hr₁.ne.symm]

Result:
no goals

Proof state:
case neg.refine_1.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hy0 : -y = 0
⊢ ∃ g, ∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
exact False.elim (hy (neg_eq_zero.1 hy0))

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ∃ g, ∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case neg.refine_1
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
h : SameRay R x y ∨ SameRay R x (-y)
⊢ ∃ g, ∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0

case neg.refine_2
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
h : ∃ g, ∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Proof state:
case neg.refine_2.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
rcases lt_trichotomy (m 0) 0 with (hm0 | hm0 | hm0) <;>
  rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)

Result:
case neg.refine_2.intro.intro.inl.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)

case neg.refine_2.intro.intro.inl.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)

case neg.refine_2.intro.intro.inl.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)

case neg.refine_2.intro.intro.inr.inl.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)

case neg.refine_2.intro.intro.inr.inl.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)

case neg.refine_2.intro.intro.inr.inl.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)

case neg.refine_2.intro.intro.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)

case neg.refine_2.intro.intro.inr.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)

case neg.refine_2.intro.intro.inr.inr.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)

Proof state:
case neg.refine_1.inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ ∑ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i • ![x, y] i = 0 ∧ ∃ i, ![r₁, r₂] i ≠ 0

Tactic:
rw [Fin.sum_univ_two, Fin.exists_fin_two]

Result:
case neg.refine_1.inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ ![r₁, r₂] 0 • ![x, y] 0 + ![r₁, r₂] 1 • ![x, y] 1 = 0 ∧ (![r₁, r₂] 0 ≠ 0 ∨ ![r₁, r₂] 1 ≠ 0)

Proof state:
case neg.refine_2.intro.intro.inr.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
⊢ False

Tactic:
simp [hm1, hx, hm0.ne.symm] at hm

Result:
no goals