awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
h : (rx * ry) • (x + y) = ry • rx • x + rx • ry • y
⊢ (rx * ry) • (x + y) = (ry * rz₁ + rx * rz₂) • z
have h₁ : (ry * rz₁ + rx * rz₂) • z = ry • rz₁ • z + rx • rz₂ • z
Tactic: convert! congr(ry • $Hx + rx • $Hy) using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
u : Rˣ
hu : 0 < (↑u : R)
v : Ray R M
⊢ u • v = v
have h : ∀ (v : M) (hv : v ≠ 0), HSMul.hSMul (β := Ray R M) u (rayOfNeZero R v hv) = rayOfNeZero R v hv
Tactic: induction v using Module.Ray.ind
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
u : Rˣ
hu : 0 < (↑u : R)
v : M
hv : v ≠ 0
⊢ HSMul.hSMul (β := Ray R M) u (rayOfNeZero R v hv) = rayOfNeZero R v hv
have h : SameRay R (u • v) v
Tactic: rw [smul_rayOfNeZero, ray_eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
⊢ SameRay R (-x) y ↔ SameRay R x (-y)
have rw : SameRay R (- -x) (-y) ↔ SameRay R x (-y)
Tactic: rw [← sameRay_neg_iff, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
rw : SameRay R (- -x) (-y) ↔ SameRay R x (-y)
⊢ SameRay R (-x) y ↔ SameRay R x (-y)
have rw₁ : SameRay R x (-y) ↔ SameRay R x (-y)
Tactic: rw [← sameRay_neg_iff, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
r : R
hr : r < 0
h : SameRay R x (r • x)
⊢ x = 0
have inl : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rcases h with (rfl | h₀ | ⟨r₁, r₂, hr₁, hr₂, h⟩)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
r : R
hr : r < 0
h : SameRay R x (r • x)
inl : Eq.{u_2 + 1} (α := M) 0 0
⊢ x = 0
have inr : ∀ (h₀ : r • x = 0), x = 0
Tactic: rcases h with (rfl | h₀ | ⟨r₁, r₂, hr₁, hr₂, h⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
r : R
hr : r < 0
h : SameRay R x (r • x)
inl : Eq.{u_2 + 1} (α := M) 0 0
inr : ∀ (h₀ : r • x = 0), x = 0
⊢ x = 0
have inr₁ : ∀ (r₁ r₂ : R) (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) (h : r₁ • x = r₂ • r • x), x = 0
Tactic: rcases h with (rfl | h₀ | ⟨r₁, r₂, hr₁, hr₂, h⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0
have h₁ : r₁ - r₂ * r = 0 ∨ x = 0
Tactic: rw [← sub_eq_zero, smul_smul, ← sub_smul, smul_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ x = 0
have inr : r₂ * r < r₁
Tactic: refine h.resolve_left (ne_of_gt <| sub_pos.2 ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
h : SameRay R x (-x)
⊢ x = 0
have refine : SameRay R x (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (-1) x)
Tactic: refine eq_zero_of_sameRay_neg_smul_right (neg_lt_zero.2 (zero_lt_one' R)) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : PartialOrder R_1
inst_2 : IsStrictOrderedRing R_1
M : Type u_2
N : Type u_3
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R_1 M
inst_6 : Module R_1 N
x y : M
R : Type u_4
v : RayVector R M
⊢ - -v = v
have rw : Eq.{u_2 + 1} (α := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) (- -v)) : M)
  (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M)
Tactic: rw [RayVector.ext_iff, coe_neg, coe_neg, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : PartialOrder R_1
inst_2 : IsStrictOrderedRing R_1
M : Type u_2
N : Type u_3
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R_1 M
inst_6 : Module R_1 N
x y : M
R : Type u_4
v : RayVector R M
rw :
  Eq.{u_2 + 1} (α := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) (- -v)) : M)
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M)
⊢ - -v = v
have rw₁ : Eq.{u_2 + 1} (α := M) (-(↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) (-v)) : M))
  (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M)
Tactic: rw [RayVector.ext_iff, coe_neg, coe_neg, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : PartialOrder R_1
inst_2 : IsStrictOrderedRing R_1
M : Type u_2
N : Type u_3
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R_1 M
inst_6 : Module R_1 N
x y : M
R : Type u_4
v : RayVector R M
rw :
  Eq.{u_2 + 1} (α := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) (- -v)) : M)
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M)
rw₁ :
  Eq.{u_2 + 1} (α := M) (-(↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) (-v)) : M))
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M)
⊢ - -v = v
have rw₂ : Eq.{u_2 + 1} (α := M) (- -(↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M))
  (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M)
Tactic: rw [RayVector.ext_iff, coe_neg, coe_neg, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : PartialOrder R_1
inst_2 : IsStrictOrderedRing R_1
M : Type u_2
N : Type u_3
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R_1 M
inst_6 : Module R_1 N
x y : M
R : Type u_4
v : RayVector R M
rw :
  Eq.{u_2 + 1} (α := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) (- -v)) : M)
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M)
rw₁ :
  Eq.{u_2 + 1} (α := M) (-(↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) (-v)) : M))
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M)
rw₂ :
  Eq.{u_2 + 1} (α := M) (- -(↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M))
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M)
⊢ - -v = v
have rw₃ : Eq.{u_2 + 1} (α := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M)
  (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v) : M)
Tactic: rw [RayVector.ext_iff, coe_neg, coe_neg, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ Ne (α := Ray R M) (rayOfNeZero R x hx) (-rayOfNeZero R x hx)
have h : ¬SameRay R x (-x)
Tactic: rw [neg_rayOfNeZero, Ne, ray_eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
x : Ray R M
⊢ x ≠ -x
have h : ∀ (x : M) (hx : x ≠ 0), Ne (α := Ray R M) (rayOfNeZero R x hx) (-rayOfNeZero R x hx)
Tactic: induction x using Module.Ray.ind with | h x hx =>
  rw [neg_rayOfNeZero, Ne, ray_eq_iff]
  exact mt eq_zero_of_sameRay_self_neg hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
u : Rˣ
v : Ray R M
⊢ -u • v = -(u • v)
have h : ∀ (v : M) (hv : v ≠ 0),
  HSMul.hSMul (β := Ray R M) (-u) (rayOfNeZero R v hv) = -HSMul.hSMul (β := Ray R M) u (rayOfNeZero R v hv)
Tactic: induction v using Module.Ray.ind
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
u : Rˣ
hu : (↑u : R) < 0
v : Ray R M
⊢ u • v = -v
have hu₁ : 0 < (↑(-u) : R)
Tactic: rw [← neg_inj, neg_neg, ← neg_units_smul, units_smul_of_pos]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
u : Rˣ
hu : (↑u : R) < 0
v : Ray R M
⊢ 0 < (↑(-u) : R)
have hu₁ : 0 < -(↑u : R)
Tactic: rwa [Units.val_neg, Right.neg_pos_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
N : Type u_3
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
f : M ≃ₗ[R] N
v : Ray R M
⊢ Eq.{u_3 + 1} (α := Ray R N)
    (((map f : Equiv.{u_2 + 1, u_3 + 1} (Ray R M) (Ray R N)) : (a : Ray R M) → Ray R N) (-v) : Ray R N)
    (-((map f : Equiv.{u_2 + 1, u_3 + 1} (Ray R M) (Ray R N)) : (a : Ray R M) → Ray R N) v : Ray R N)
have h : ∀ (g : M) (hg : g ≠ 0),
  Eq.{u_3 + 1} (α := Ray R N)
    (((map f : Equiv.{u_2 + 1, u_3 + 1} (Ray R M) (Ray R N)) : (a : Ray R M) → Ray R N) (-rayOfNeZero R g hg) : Ray R N)
    (-((map f : Equiv.{u_2 + 1, u_3 + 1} (Ray R M) (Ray R N)) : (a : Ray R M) → Ray R N) (rayOfNeZero R g hg) : Ray R N)
Tactic: induction v using Module.Ray.ind with | h g hg => simp
Cleared hypotheses: v
-- 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
v₁ v₂ : M
h : v₁ ∈ MulAction.orbit.{u_1, u_2} (↥(Units.posSubgroup R)) v₂
⊢ SameRay R v₁ v₂
have rcases : ∀ (r : Rˣ) (hr : 0 < (↑r : R)), SameRay R (r • v₂) v₂
Tactic: rcases h with ⟨⟨r, hr : 0 < r.1⟩, rfl : r • v₂ = v₁⟩
Cleared hypotheses: v₁, 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
u : Rˣ
v : Ray R M
this : 0 < (↑u : R) * (↑u : R)
⊢ (u * u) • u⁻¹ • v = u • v
have rw : u • u • u⁻¹ • v = u • v
Tactic: rw [mul_smul, smul_inv_smul]
-- 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
u : Rˣ
v : Ray R M
this : 0 < (↑u : R) * (↑u : R)
rw : u • u • u⁻¹ • v = u • v
⊢ (u * u) • u⁻¹ • v = u • v
have rw₁ : u • v = u • v
Tactic: rw [mul_smul, smul_inv_smul]
-- 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
v : M
r : R
⊢ SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0
have rw : SameRay R (- -v) (-(r • v)) ↔ r ≤ 0 ∨ v = 0
Tactic: rw [← sameRay_neg_iff, neg_neg, ← neg_smul, sameRay_smul_right_iff, neg_nonneg]
-- 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
v : M
r : R
rw : SameRay R (- -v) (-(r • v)) ↔ r ≤ 0 ∨ v = 0
⊢ SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0
have rw₁ : SameRay R v (-(r • v)) ↔ r ≤ 0 ∨ v = 0
Tactic: rw [← sameRay_neg_iff, neg_neg, ← neg_smul, sameRay_smul_right_iff, neg_nonneg]
-- 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
v : M
r : R
rw : SameRay R (- -v) (-(r • v)) ↔ r ≤ 0 ∨ v = 0
rw₁ : SameRay R v (-(r • v)) ↔ r ≤ 0 ∨ v = 0
⊢ SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0
have rw₂ : SameRay R v (-r • v) ↔ r ≤ 0 ∨ v = 0
Tactic: rw [← sameRay_neg_iff, neg_neg, ← neg_smul, sameRay_smul_right_iff, neg_nonneg]
-- 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
v : M
r : R
rw : SameRay R (- -v) (-(r • v)) ↔ r ≤ 0 ∨ v = 0
rw₁ : SameRay R v (-(r • v)) ↔ r ≤ 0 ∨ v = 0
rw₂ : SameRay R v (-r • v) ↔ r ≤ 0 ∨ v = 0
⊢ SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0
have rw₃ : 0 ≤ -r ∨ v = 0 ↔ r ≤ 0 ∨ v = 0
Tactic: rw [← sameRay_neg_iff, neg_neg, ← neg_smul, sameRay_smul_right_iff, neg_nonneg]
-- 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
v : M
r : R
rw : SameRay R (- -v) (-(r • v)) ↔ r ≤ 0 ∨ v = 0
rw₁ : SameRay R v (-(r • v)) ↔ r ≤ 0 ∨ v = 0
rw₂ : SameRay R v (-r • v) ↔ r ≤ 0 ∨ v = 0
rw₃ : 0 ≤ -r ∨ v = 0 ↔ r ≤ 0 ∨ v = 0
⊢ SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0
have rw₄ : r ≤ 0 ∨ v = 0 ↔ r ≤ 0 ∨ v = 0
Tactic: rw [← sameRay_neg_iff, neg_neg, ← neg_smul, sameRay_smul_right_iff, neg_nonneg]
-- 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
u : Rˣ
v : Ray R M
⊢ u • v = v ↔ 0 < (↑u : R)
have h : ∀ (v : M) (hv : v ≠ 0), HSMul.hSMul (β := Ray R M) u (rayOfNeZero R v hv) = rayOfNeZero R v hv ↔ 0 < (↑u : R)
Tactic: induction v using Module.Ray.ind with | h v hv =>
  simp only [smul_rayOfNeZero, ray_eq_iff, Units.smul_def, sameRay_smul_left_iff_of_ne hv u.ne_zero]
Cleared hypotheses: v
-- 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
u : Rˣ
v : Ray R M
⊢ u • v = -v ↔ (↑u : R) < 0
have rw : -(u • v) = - -v ↔ (↑u : R) < 0
Tactic: rw [← neg_inj, neg_neg, ← Module.Ray.neg_units_smul, units_smul_eq_self_iff, Units.val_neg,
    neg_pos]
-- 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
u : Rˣ
v : Ray R M
rw : -(u • v) = - -v ↔ (↑u : R) < 0
⊢ u • v = -v ↔ (↑u : R) < 0
have rw₁ : -(u • v) = v ↔ (↑u : R) < 0
Tactic: rw [← neg_inj, neg_neg, ← Module.Ray.neg_units_smul, units_smul_eq_self_iff, Units.val_neg,
    neg_pos]
-- 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
u : Rˣ
v : Ray R M
rw : -(u • v) = - -v ↔ (↑u : R) < 0
rw₁ : -(u • v) = v ↔ (↑u : R) < 0
⊢ u • v = -v ↔ (↑u : R) < 0
have rw₂ : -u • v = v ↔ (↑u : R) < 0
Tactic: rw [← neg_inj, neg_neg, ← Module.Ray.neg_units_smul, units_smul_eq_self_iff, Units.val_neg,
    neg_pos]
-- 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
u : Rˣ
v : Ray R M
rw : -(u • v) = - -v ↔ (↑u : R) < 0
rw₁ : -(u • v) = v ↔ (↑u : R) < 0
rw₂ : -u • v = v ↔ (↑u : R) < 0
⊢ u • v = -v ↔ (↑u : R) < 0
have rw₃ : 0 < (↑(-u) : R) ↔ (↑u : R) < 0
Tactic: rw [← neg_inj, neg_neg, ← Module.Ray.neg_units_smul, units_smul_eq_self_iff, Units.val_neg,
    neg_pos]
-- 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
u : Rˣ
v : Ray R M
rw : -(u • v) = - -v ↔ (↑u : R) < 0
rw₁ : -(u • v) = v ↔ (↑u : R) < 0
rw₂ : -u • v = v ↔ (↑u : R) < 0
rw₃ : 0 < (↑(-u) : R) ↔ (↑u : R) < 0
⊢ u • v = -v ↔ (↑u : R) < 0
have rw₄ : 0 < -(↑u : R) ↔ (↑u : R) < 0
Tactic: rw [← neg_inj, neg_neg, ← Module.Ray.neg_units_smul, units_smul_eq_self_iff, Units.val_neg,
    neg_pos]
-- 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
u : Rˣ
v : Ray R M
rw : -(u • v) = - -v ↔ (↑u : R) < 0
rw₁ : -(u • v) = v ↔ (↑u : R) < 0
rw₂ : -u • v = v ↔ (↑u : R) < 0
rw₃ : 0 < (↑(-u) : R) ↔ (↑u : R) < 0
rw₄ : 0 < -(↑u : R) ↔ (↑u : R) < 0
⊢ u • v = -v ↔ (↑u : R) < 0
have rw₅ : (↑u : R) < 0 ↔ (↑u : R) < 0
Tactic: rw [← neg_inj, neg_neg, ← Module.Ray.neg_units_smul, units_smul_eq_self_iff, Units.val_neg,
    neg_pos]
-- 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 ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
have pos : ∀ (hx : x = 0), SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent 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 ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
have neg : ∀ (hx : ¬x = 0), SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent 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 ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
have pos : ∀ (hy : y = 0), SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
Tactic: by_cases hy : y = 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
pos : ∀ (hy : y = 0), SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
have neg : ∀ (hy : ¬y = 0), SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
Tactic: by_cases hy : y = 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
hy : ¬y = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
have neg : SameRay R x y ∨ SameRay R x (-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: simp_rw [Fintype.not_linearIndependent_iff]
-- 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
⊢ SameRay R x y ∨ SameRay R x (-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 : ∀ (h : SameRay R x y ∨ SameRay R x (-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: refine ⟨fun h => ?_, fun 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
neg :
  ∀ (h : SameRay R x y ∨ SameRay R x (-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
⊢ SameRay R x y ∨ SameRay R x (-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₁ : ∀
  (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)
Tactic: refine ⟨fun h => ?_, fun 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)
⊢ ∃ (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 : ∀ (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: rcases h with ((hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩) | (hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩))
Cleared hypotheses: h