awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Ray
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

Tactic:
h.resolve_left (ne_of_gt <| sub_pos.2 ?_)

Premises used: Iff.mpr, sub_pos, ne_of_gt, Or.resolve_left
-- Module: Mathlib.LinearAlgebra.Ray
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
inr : r₂ * r < r₁
⊢ x = 0

Tactic:
refine h.resolve_left (ne_of_gt <| sub_pos.2 ?_)

Premises used: Iff.mpr, sub_pos, ne_of_gt, Or.resolve_left
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ r₂ * r < r₁

Tactic:
(mul_neg_of_pos_of_neg hr₂ hr).trans hr₁

Premises used: LT.lt.trans, mul_neg_of_pos_of_neg
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ r₂ * r < r₁

Tactic:
exact (mul_neg_of_pos_of_neg hr₂ hr).trans hr₁

Premises used: LT.lt.trans, mul_neg_of_pos_of_neg
-- Module: Mathlib.LinearAlgebra.Ray
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

Tactic:
eq_zero_of_sameRay_neg_smul_right (neg_lt_zero.2 (zero_lt_one' R)) ?_

Premises used: Iff.mpr, neg_lt_zero, zero_lt_one', eq_zero_of_sameRay_neg_smul_right
-- Module: Mathlib.LinearAlgebra.Ray
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)
refine : SameRay R x (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (-1) x)
⊢ x = 0

Tactic:
refine eq_zero_of_sameRay_neg_smul_right (neg_lt_zero.2 (zero_lt_one' R)) ?_

Premises used: Iff.mpr, neg_lt_zero, zero_lt_one', eq_zero_of_sameRay_neg_smul_right
-- Module: Mathlib.LinearAlgebra.Ray
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 rwa rwa₁ rwa₂ rwa₃ : SameRay R x (-x)
⊢ SameRay R x (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (-1) x)

Tactic:
rwa [neg_one_smul]

Premises used: neg_one_smul
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_4
v : RayVector R M
⊢ 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:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Ray
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)
rw₃ 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

Tactic:
rw [RayVector.ext_iff, coe_neg, coe_neg, neg_neg]

Premises used: RayVector.ext_iff, neg_neg, RayVector.coe_neg
-- Module: Mathlib.LinearAlgebra.Ray
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
v₁ v₂ : RayVector R M
⊢ -v₁ ≈ -v₂ ↔ v₁ ≈ v₂

Tactic:
sameRay_neg_iff

Premises used: sameRay_neg_iff
-- Module: Mathlib.LinearAlgebra.Ray
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
v : M
h : v ≠ 0
⊢ Eq (α := Ray R M) (-rayOfNeZero R v h) (rayOfNeZero R (-v) ⋯)

Tactic:
rfl

Premises used: rayOfNeZero, Quotient.map, Quot.map, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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
x_1 y : M
x : Ray R M
⊢ ∀ (v : M) (hv : v ≠ 0), Eq (α := Ray R M) (- -rayOfNeZero R v hv) (rayOfNeZero R v hv)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Ray
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
x_1 y : M
x : Ray R M
⊢ - -x = x

Tactic:
apply ind R (by simp) x

Premises used: Module.Ray.ind
-- Module: Mathlib.LinearAlgebra.Ray
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
h : ¬SameRay R x (-x)
⊢ Ne (α := Ray R M) (rayOfNeZero R x hx) (-rayOfNeZero R x hx)

Tactic:
rw [neg_rayOfNeZero, Ne, ray_eq_iff]

Premises used: neg_rayOfNeZero, Ne, ray_eq_iff
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ ¬SameRay R x (-x)

Tactic:
mt eq_zero_of_sameRay_self_neg hx

Premises used: mt, eq_zero_of_sameRay_self_neg
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ ¬SameRay R x (-x)

Tactic:
exact mt eq_zero_of_sameRay_self_neg hx

Premises used: mt, eq_zero_of_sameRay_self_neg
-- Module: Mathlib.LinearAlgebra.Ray
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
h : ∀ (x : M) (hx : x ≠ 0), Ne (α := Ray R M) (rayOfNeZero R x hx) (-rayOfNeZero R x hx)
⊢ x ≠ -x

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

Premises used: neg_rayOfNeZero, Ne, ray_eq_iff, Module.Ray.ind
-- Module: Mathlib.LinearAlgebra.Ray
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
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)
⊢ -u • v = -(u • v)

Tactic:
induction v using Module.Ray.ind

Premises used: Module.Ray.ind
-- Module: Mathlib.LinearAlgebra.Ray
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 : 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:
simp only [smul_rayOfNeZero, Units.smul_def, Units.val_neg, neg_smul, neg_rayOfNeZero]

Premises used: neg_smul, smul_rayOfNeZero, neg_rayOfNeZero, Units.val_neg, Units.smul_def
-- Module: Mathlib.LinearAlgebra.Ray
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
hu₁ : 0 < (↑(-u) : R)
⊢ u • v = -v

Tactic:
rw [← neg_inj, neg_neg, ← neg_units_smul, units_smul_of_pos]

Premises used: Module.Ray.neg_units_smul, neg_neg, Module.Ray.units_smul_of_pos, neg_inj
-- Module: Mathlib.LinearAlgebra.Ray
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
hu₁ : 0 < -(↑u : R)
hu₂ hu₃ hu₄ hu₅ : (↑u : R) < 0
⊢ 0 < (↑(-u) : R)

Tactic:
rwa [Units.val_neg, Right.neg_pos_iff]

Premises used: Right.neg_pos_iff, Units.val_neg
-- Module: Mathlib.LinearAlgebra.Ray
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
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:
simp
-- Module: Mathlib.LinearAlgebra.Ray
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
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)
⊢ 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)

Tactic:
induction v using Module.Ray.ind with | h g hg => simp

Premises used: Module.Ray.ind
-- 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
v₁ v₂ : M
h : v₁ ∈ MulAction.orbit.{u_1, u_2} (↥(Units.posSubgroup R)) v₂
rcases : ∀ (r : Rˣ) (hr : 0 < (↑r : R)), SameRay R (r • v₂) v₂
⊢ SameRay R v₁ v₂

Tactic:
rcases h with ⟨⟨r, hr : 0 < r.1⟩, rfl : r • v₂ = v₁⟩

Premises used: rfl
-- 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
v₂ : M
r : Rˣ
hr : 0 < (↑r : R)
⊢ SameRay R (r • v₂) v₂

Tactic:
SameRay.sameRay_pos_smul_left _ hr

Premises used: SameRay.sameRay_pos_smul_left
-- 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
v₂ : M
r : Rˣ
hr : 0 < (↑r : R)
⊢ SameRay R (r • v₂) v₂

Tactic:
exact SameRay.sameRay_pos_smul_left _ hr

Premises used: SameRay.sameRay_pos_smul_left
-- 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
u : Rˣ
v : Ray R M
this : 0 < (↑u : R) * (↑u : R)
⊢ 0 < (↑(u * u) : R)

Tactic:
this
-- 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
u : Rˣ
v : Ray R M
this : 0 < (↑u : R) * (↑u : R)
⊢ 0 < (↑(u * u) : R)

Tactic:
exact this
-- 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
u : Rˣ
v : Ray R M
this : 0 < (↑u : R) * (↑u : R)
rw : u • u • u⁻¹ • v = u • v
rw₁ rw₂ : u • v = u • v
⊢ (u * u) • u⁻¹ • v = u • v

Tactic:
rw [mul_smul, smul_inv_smul]

Premises used: smul_inv_smul, SemigroupAction.mul_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
v : M
r : R
⊢ SameRay R v (r • v) ↔ 0 ≤ r ∨ v = 0

Tactic:
⟨fun hrv => or_iff_not_imp_left.2 fun hr => eq_zero_of_sameRay_neg_smul_right (not_le.1 hr) hrv,
    or_imp.2 ⟨SameRay.sameRay_nonneg_smul_right v, fun h => h.symm ▸ SameRay.zero_left _⟩⟩

Premises used: not_le, Iff.mpr, Eq.rec, or_imp, SameRay.sameRay_nonneg_smul_right, SameRay.zero_left, Classical.or_iff_not_imp_left, And.intro, Iff.intro, Iff.mp, HSMul.hSMul, eq_zero_of_sameRay_neg_smul_right, OfNat.ofNat, Eq.symm
-- 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
v : M
hv : v ≠ 0
r : R
hr : r ≠ 0
⊢ SameRay R v (r • v) ↔ 0 < r

Tactic:
simp only [sameRay_smul_right_iff, hv, or_false, hr.symm.le_iff_lt]

Premises used: Ne.le_iff_lt, Ne.symm, or_false, sameRay_smul_right_iff
-- 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
v : M
r : R
⊢ SameRay R (r • v) v ↔ 0 ≤ r ∨ v = 0

Tactic:
SameRay.sameRay_comm.trans sameRay_smul_right_iff

Premises used: SameRay.sameRay_comm, Iff.trans, sameRay_smul_right_iff
-- 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
v : M
hv : v ≠ 0
r : R
hr : r ≠ 0
⊢ SameRay R (r • v) v ↔ 0 < r

Tactic:
SameRay.sameRay_comm.trans (sameRay_smul_right_iff_of_ne hv hr)

Premises used: SameRay.sameRay_comm, sameRay_smul_right_iff_of_ne, Iff.trans
-- 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
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
rw₄ rw₅ : r ≤ 0 ∨ v = 0 ↔ r ≤ 0 ∨ v = 0
⊢ SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0

Tactic:
rw [← sameRay_neg_iff, neg_neg, ← neg_smul, sameRay_smul_right_iff, neg_nonneg]

Premises used: neg_smul, neg_neg, neg_nonneg, sameRay_smul_right_iff, sameRay_neg_iff
-- 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
v : M
r : R
hv : v ≠ 0
hr : r ≠ 0
⊢ SameRay R (-v) (r • v) ↔ r < 0

Tactic:
simp only [sameRay_neg_smul_right_iff, hv, or_false, hr.le_iff_lt]

Premises used: Ne.le_iff_lt, sameRay_neg_smul_right_iff, or_false
-- 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
v : M
r : R
⊢ SameRay R (r • v) (-v) ↔ r ≤ 0 ∨ v = 0

Tactic:
SameRay.sameRay_comm.trans sameRay_neg_smul_right_iff

Premises used: SameRay.sameRay_comm, sameRay_neg_smul_right_iff, Iff.trans
-- 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
v : M
r : R
hv : v ≠ 0
hr : r ≠ 0
⊢ SameRay R (r • v) (-v) ↔ r < 0

Tactic:
SameRay.sameRay_comm.trans <| sameRay_neg_smul_right_iff_of_ne hv hr

Premises used: SameRay.sameRay_comm, sameRay_neg_smul_right_iff_of_ne, Iff.trans
-- 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
u : Rˣ
v : M
hv : v ≠ 0
⊢ HSMul.hSMul (β := Ray R M) u (rayOfNeZero R v hv) = rayOfNeZero R v hv ↔ 0 < (↑u : R)

Tactic:
simp only [smul_rayOfNeZero, ray_eq_iff, Units.smul_def, sameRay_smul_left_iff_of_ne hv u.ne_zero]

Premises used: smul_rayOfNeZero, Units.ne_zero, sameRay_smul_left_iff_of_ne, Units.smul_def, ray_eq_iff
-- 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
u : Rˣ
v : Ray R M
h : ∀ (v : M) (hv : v ≠ 0), HSMul.hSMul (β := Ray R M) u (rayOfNeZero R v hv) = rayOfNeZero R v hv ↔ 0 < (↑u : R)
⊢ u • v = v ↔ 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]

Premises used: smul_rayOfNeZero, Units.smul_def, ray_eq_iff, Module.Ray.ind
-- 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
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
rw₅ rw₆ : (↑u : R) < 0 ↔ (↑u : R) < 0
⊢ 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]

Premises used: Module.Ray.neg_units_smul, neg_pos, units_smul_eq_self_iff, neg_neg, Units.val_neg, neg_inj
-- 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
pos : ∀ (hx : x = 0), SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
neg : ∀ (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]

Tactic:
by_cases hx : x = 0
-- 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
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Tactic:
simpa [hx] using fun h : LinearIndependent R ![0, y] => h.ne_zero 0 rfl

Premises used: LinearIndependent.ne_zero, OfNat.ofNat, rfl
-- 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
pos : ∀ (hy : y = 0), SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
neg : ∀ (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]

Tactic:
by_cases hy : y = 0
-- 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
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Tactic:
simpa [hy] using fun h : LinearIndependent R ![x, 0] => h.ne_zero 1 rfl

Premises used: LinearIndependent.ne_zero, OfNat.ofNat, rfl
-- 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
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
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Tactic:
simp_rw [Fintype.not_linearIndependent_iff]

Premises used: Fintype.not_linearIndependent_iff
-- 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
⊢ 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:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- 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
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
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)
⊢ 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 => ?_⟩
-- 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 : 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
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
⊢ ∃ (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⟩))