awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hx0 : x = 0
⊢ ∃ (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i) 0 ∧ ∃ (i : Fin (Nat.succ 0).succ), g i ≠ 0

Tactic:
False.elim (hx hx0)

Premises used: False.elim
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hx0 : x = 0
⊢ ∃ (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i) 0 ∧ ∃ (i : Fin (Nat.succ 0).succ), g i ≠ 0

Tactic:
exact False.elim (hx hx0)

Premises used: False.elim
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hy0 : y = 0
⊢ ∃ (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i) 0 ∧ ∃ (i : Fin (Nat.succ 0).succ), g i ≠ 0

Tactic:
False.elim (hy hy0)

Premises used: False.elim
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hy0 : y = 0
⊢ ∃ (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i) 0 ∧ ∃ (i : Fin (Nat.succ 0).succ), g i ≠ 0

Tactic:
exact False.elim (hy hy0)

Premises used: False.elim
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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
⊢ ∃ (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i) 0 ∧ ∃ (i : Fin (Nat.succ 0).succ), g i ≠ 0

Tactic:
⟨![r₁, -r₂], ?_⟩

Premises used: Exists.intro, Matrix.vecEmpty, Matrix.vecCons, Neg.neg
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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
neg :
  Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, ![r₁, -r₂] i • ![x, y] i) 0 ∧
    ∃ (i : Fin (Nat.succ 0).succ), ![r₁, -r₂] i ≠ 0
⊢ ∃ (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i) 0 ∧ ∃ (i : Fin (Nat.succ 0).succ), g i ≠ 0

Tactic:
refine ⟨![r₁, -r₂], ?_⟩
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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
neg : ![r₁, -r₂] 0 • ![x, y] 0 + ![r₁, -r₂] 1 • ![x, y] 1 = 0 ∧ (![r₁, -r₂] 0 ≠ 0 ∨ ![r₁, -r₂] 1 ≠ 0)
⊢ Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, ![r₁, -r₂] i • ![x, y] i) 0 ∧
    ∃ (i : Fin (Nat.succ 0).succ), ![r₁, -r₂] i ≠ 0

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

Premises used: Fin.exists_fin_two, Fin.sum_univ_two
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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]

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hy0 : -y = 0
⊢ ∃ (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i) 0 ∧ ∃ (i : Fin (Nat.succ 0).succ), g i ≠ 0

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

Premises used: False.elim, neg_eq_zero, Iff.mp
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hy0 : -y = 0
⊢ ∃ (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i) 0 ∧ ∃ (i : Fin (Nat.succ 0).succ), g i ≠ 0

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

Premises used: False.elim, neg_eq_zero, Iff.mp
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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
⊢ ∃ (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i) 0 ∧ ∃ (i : Fin (Nat.succ 0).succ), g i ≠ 0

Tactic:
⟨![r₁, r₂], ?_⟩

Premises used: Exists.intro, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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
neg :
  Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i • ![x, y] i) 0 ∧
    ∃ (i : Fin (Nat.succ 0).succ), ![r₁, r₂] i ≠ 0
⊢ ∃ (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i) 0 ∧ ∃ (i : Fin (Nat.succ 0).succ), g i ≠ 0

Tactic:
refine ⟨![r₁, r₂], ?_⟩
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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
neg : ![r₁, r₂] 0 • ![x, y] 0 + ![r₁, r₂] 1 • ![x, y] 1 = 0 ∧ (![r₁, r₂] 0 ≠ 0 ∨ ![r₁, r₂] 1 ≠ 0)
⊢ Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i • ![x, y] i) 0 ∧
    ∃ (i : Fin (Nat.succ 0).succ), ![r₁, r₂] i ≠ 0

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

Premises used: Fin.exists_fin_two, Fin.sum_univ_two
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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]

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
h :
  ∃ (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i) 0 ∧ ∃ (i : Fin (Nat.succ 0).succ), g i ≠ 0
neg :
  ∀ (m : Fin (Nat.succ 0).succ → R) (hm : Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, m i • ![x, y] i) 0)
    (hmne : ∃ (i : Fin (Nat.succ 0).succ), m i ≠ 0), SameRay R x y ∨ SameRay R x (-y)
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
rcases h with ⟨m, hm, hmne⟩
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, m i • ![x, y] i) 0
hmne : ∃ (i : Fin (Nat.succ 0).succ), m i ≠ 0
⊢ m 0 • ![x, y] 0 = -(m 1 • ![x, y] 1)

Tactic:
rw [Fin.sum_univ_two, add_eq_zero_iff_eq_neg] at hm

Premises used: add_eq_zero_iff_eq_neg, Fin.sum_univ_two
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : Eq.{u_2 + 1} (α := M) (∑ i : Fin (Nat.succ 0).succ, m i • ![x, y] i) 0
hmne : ∃ (i : Fin (Nat.succ 0).succ), m i ≠ 0
hm₁ : m 0 • ![x, y] 0 = -(m 1 • ![x, y] 1)
⊢ ∃ (i : Fin (Nat.succ 0).succ), m i ≠ 0

Tactic:
rw [Fin.sum_univ_two, add_eq_zero_iff_eq_neg] at hm

Premises used: add_eq_zero_iff_eq_neg, Fin.sum_univ_two
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
neg : ∀ (hm0 : m 0 < 0), SameRay R x y ∨ SameRay R x (-y)
neg₁ : ∀ (hm0 : m 0 = 0), SameRay R x y ∨ SameRay R x (-y)
neg₂ : ∀ (hm0 : 0 < m 0), SameRay R x y ∨ SameRay R x (-y)
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
rcases lt_trichotomy (m 0) 0 with (hm0 | hm0 | hm0)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 < 0
neg : ∀ (hm1 : m 1 < 0), SameRay R x y ∨ SameRay R x (-y)
neg₁ : ∀ (hm1 : m 1 = 0), SameRay R x y ∨ SameRay R x (-y)
neg₂ : ∀ (hm1 : 0 < m 1), SameRay R x y ∨ SameRay R x (-y)
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 = 0
neg : ∀ (hm1 : m 1 < 0), SameRay R x y ∨ SameRay R x (-y)
neg₁ : ∀ (hm1 : m 1 = 0), SameRay R x y ∨ SameRay R x (-y)
neg₂ : ∀ (hm1 : 0 < m 1), SameRay R x y ∨ SameRay R x (-y)
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : 0 < m 0
neg : ∀ (hm1 : m 1 < 0), SameRay R x y ∨ SameRay R x (-y)
neg₁ : ∀ (hm1 : m 1 = 0), SameRay R x y ∨ SameRay R x (-y)
neg₂ : ∀ (hm1 : 0 < m 1), SameRay R x y ∨ SameRay R x (-y)
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
Or.inr (Or.inr (Or.inr ⟨-m 0, -m 1, Left.neg_pos_iff.2 hm0, Left.neg_pos_iff.2 hm1, ?_⟩))

Premises used: Iff.mpr, Left.neg_pos_iff, And.intro, Exists.intro, OfNat.ofNat, Neg.neg, Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 < 0
neg : -m 0 • x = -m 1 • -y
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
refine
        Or.inr (Or.inr (Or.inr ⟨-m 0, -m 1, Left.neg_pos_iff.2 hm0, Left.neg_pos_iff.2 hm1, ?_⟩))

Premises used: Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 < 0
⊢ -m 0 • x + m 0 • x - (-m 1 • -y + -(m 1 • y)) = 0

Tactic:
module
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 < 0
a : -m 0 • x + m 0 • x - (-m 1 • -y + -(m 1 • y)) = 0
⊢ -m 0 • x = -m 1 • -y

Tactic:
linear_combination (norm := module) -hm
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 = 0
neg : False
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
exfalso
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 = 0
⊢ False

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

Premises used: LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 < 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
Or.inl (Or.inr (Or.inr ⟨-m 0, m 1, Left.neg_pos_iff.2 hm0, hm1, ?_⟩))

Premises used: Iff.mpr, Left.neg_pos_iff, And.intro, Exists.intro, Or.inl, OfNat.ofNat, Neg.neg, Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 < 0
hm1 : 0 < m 1
neg : -m 0 • x = m 1 • y
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
refine Or.inl (Or.inr (Or.inr ⟨-m 0, m 1, Left.neg_pos_iff.2 hm0, hm1, ?_⟩))

Premises used: Or.inl, Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 < 0
hm1 : 0 < m 1
⊢ -m 0 • x + m 0 • x - (m 1 • y + -(m 1 • y)) = 0

Tactic:
module
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 < 0
hm1 : 0 < m 1
a : -m 0 • x + m 0 • x - (m 1 • y + -(m 1 • y)) = 0
⊢ -m 0 • x = m 1 • y

Tactic:
linear_combination (norm := module) -hm
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 < 0
neg : False
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
exfalso
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 < 0
⊢ False

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

Premises used: LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
⊢ m 0 ≠ 0 ∨ m 1 ≠ 0

Tactic:
rw [Fin.exists_fin_two] at hmne

Premises used: Fin.exists_fin_two
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
hmne₁ : m 0 ≠ 0 ∨ m 1 ≠ 0
⊢ m 0 = 0

Tactic:
rw [Fin.exists_fin_two] at hmne

Premises used: Fin.exists_fin_two
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
hmne₁ : m 0 ≠ 0 ∨ m 1 ≠ 0
hm0₁ : m 0 = 0
⊢ m 1 = 0

Tactic:
rw [Fin.exists_fin_two] at hmne

Premises used: Fin.exists_fin_two
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : m 0 ≠ 0 ∨ m 1 ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
False.elim (not_and_or.2 hmne ⟨hm0, hm1⟩)

Premises used: Iff.mpr, False.elim, And.intro, not_and_or
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : m 0 ≠ 0 ∨ m 1 ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
exact False.elim (not_and_or.2 hmne ⟨hm0, hm1⟩)

Premises used: Iff.mpr, False.elim, And.intro, not_and_or
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 = 0
hm1 : 0 < m 1
neg : False
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
exfalso
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : m 0 = 0
hm1 : 0 < m 1
⊢ False

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

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
Or.inl (Or.inr (Or.inr ⟨m 0, -m 1, hm0, Left.neg_pos_iff.2 hm1, ?_⟩))

Premises used: Iff.mpr, Left.neg_pos_iff, And.intro, Exists.intro, Or.inl, OfNat.ofNat, Neg.neg, Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
neg : m 0 • x = -m 1 • y
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
refine Or.inl (Or.inr (Or.inr ⟨m 0, -m 1, hm0, Left.neg_pos_iff.2 hm1, ?_⟩))

Premises used: Or.inl, Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
neg neg₁ neg₂ neg₃ : m 0 • x = -(m 1 • y)
⊢ m 0 • x = -m 1 • y

Tactic:
rwa [neg_smul]

Premises used: neg_smul
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
neg : False
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
exfalso
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
⊢ False

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

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree 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 : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
Or.inr (Or.inr (Or.inr ⟨m 0, m 1, hm0, hm1, ?_⟩))

Premises used: And.intro, Exists.intro, OfNat.ofNat, Or.inr