awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 : SameRay R x y ∨ SameRay R x (-y)
neg :
  ∀ (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
⊢ ∃ (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
have neg₁ : ∀ (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: rcases h with ((hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩) | (hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 : SameRay R x y ∨ SameRay R x (-y)
neg :
  ∀ (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
neg₁ :
  ∀ (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
⊢ ∃ (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
have neg₂ : ∀ (r₁ r₂ : R) (hr₁ : 0 < r₁),
  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: rcases h with ((hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩) | (hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 : SameRay R x y ∨ SameRay R x (-y)
neg :
  ∀ (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
neg₁ :
  ∀ (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
neg₂ :
  ∀ (r₁ r₂ : R) (hr₁ : 0 < r₁),
    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
neg₃ :
  ∀ (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
⊢ ∃ (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
have neg₄ : ∀ (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: rcases h with ((hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩) | (hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 : SameRay R x y ∨ SameRay R x (-y)
neg :
  ∀ (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
neg₁ :
  ∀ (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
neg₂ :
  ∀ (r₁ r₂ : R) (hr₁ : 0 < r₁),
    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
neg₃ :
  ∀ (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
neg₄ :
  ∀ (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
⊢ ∃ (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
have neg₅ : ∀ (r₁ r₂ : R) (hr₁ : 0 < r₁),
  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: rcases h with ((hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩) | (hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
have 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
Tactic: refine ⟨![r₁, -r₂], ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ 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
have neg : ![r₁, -r₂] 0 • ![x, y] 0 + ![r₁, -r₂] 1 • ![x, y] 1 = 0 ∧ (![r₁, -r₂] 0 ≠ 0 ∨ ![r₁, -r₂] 1 ≠ 0)
Tactic: rw [Fin.sum_univ_two, Fin.exists_fin_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
have 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
Tactic: refine ⟨![r₁, r₂], ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ 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
have neg : ![r₁, r₂] 0 • ![x, y] 0 + ![r₁, r₂] 1 • ![x, y] 1 = 0 ∧ (![r₁, r₂] 0 ≠ 0 ∨ ![r₁, r₂] 1 ≠ 0)
Tactic: rw [Fin.sum_univ_two, Fin.exists_fin_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ SameRay R x y ∨ SameRay R x (-y)
have 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)
Tactic: rcases h with ⟨m, hm, hmne⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (hypothesis)
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
⊢ SameRay R x y ∨ SameRay R x (-y)
have hm₁ : m 0 • ![x, y] 0 = -(m 1 • ![x, y] 1)
Tactic: rw [Fin.sum_univ_two, add_eq_zero_iff_eq_neg] at hm
Cleared hypotheses: hm, hmne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg : ∀ (hm0 : m 0 < 0), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 0) 0 with (hm0 | hm0 | hm0)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg₁ : ∀ (hm0 : m 0 = 0), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 0) 0 with (hm0 | hm0 | hm0)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg₂ : ∀ (hm0 : 0 < m 0), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 0) 0 with (hm0 | hm0 | hm0)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg : ∀ (hm1 : m 1 < 0), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg₁ : ∀ (hm1 : m 1 = 0), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg₂ : ∀ (hm1 : 0 < m 1), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg : ∀ (hm1 : m 1 < 0), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg₁ : ∀ (hm1 : m 1 = 0), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg₂ : ∀ (hm1 : 0 < m 1), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg : ∀ (hm1 : m 1 < 0), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg₁ : ∀ (hm1 : m 1 = 0), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
⊢ SameRay R x y ∨ SameRay R x (-y)
have neg₂ : ∀ (hm1 : 0 < m 1), SameRay R x y ∨ SameRay R x (-y)
Tactic: rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
have neg : -m 0 • x = -m 1 • -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, ?_⟩))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 1 • -y
have a : -m 0 • x + m 0 • x - (-m 1 • -y + -(m 1 • y)) = 0
Tactic: linear_combination (norm := module) -hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
have neg : -m 0 • x = m 1 • y
Tactic: refine Or.inl (Or.inr (Or.inr ⟨-m 0, m 1, Left.neg_pos_iff.2 hm0, hm1, ?_⟩))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 1 • y
have a : -m 0 • x + m 0 • x - (m 1 • y + -(m 1 • y)) = 0
Tactic: linear_combination (norm := module) -hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (hypothesis)
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)
have hmne₁ : m 0 ≠ 0 ∨ m 1 ≠ 0
Tactic: rw [Fin.exists_fin_two] at hmne
Cleared hypotheses: hmne, hm0, hm1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
have neg : m 0 • x = -m 1 • y
Tactic: refine Or.inl (Or.inr (Or.inr ⟨m 0, -m 1, hm0, Left.neg_pos_iff.2 hm1, ?_⟩))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
have neg : m 0 • x = m 1 • -y
Tactic: refine Or.inr (Or.inr (Or.inr ⟨m 0, m 1, hm0, hm1, ?_⟩))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
have rw : SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
Tactic: rw [← sameRay_or_sameRay_neg_iff_not_linearIndependent]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
have pos : ∀ (hx : x = 0), SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
pos : ∀ (hx : x = 0), SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
have neg : ∀ (hx : ¬x = 0), SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
have pos : ∀ (hy : y = 0), SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
Tactic: by_cases hy : y = 0