awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Ray
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 : M
S : Type u_5
inst_5 : CommSemiring S
inst_6 : PartialOrder S
inst_7 : Algebra S R
inst_8 : Module S M
inst_9 : SMulPosMono S R
inst_10 : IsScalarTower S R M
a : S
h : SameRay R x y
ha : 0 ≤ a
hy : y = 0
rw : HSMul.hSMul (β := M) a 0 = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) 0 0
⊢ a • y = 0

Tactic:
rw [hy, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.LinearAlgebra.Ray
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 : M
S : Type u_5
inst_5 : CommSemiring S
inst_6 : PartialOrder S
inst_7 : Algebra S R
inst_8 : Module S M
inst_9 : SMulPosMono S R
inst_10 : IsScalarTower S R M
a : S
h : SameRay R x y
ha : 0 ≤ a
⊢ SameRay R (a • x) y

Tactic:
(h.symm.nonneg_smul_right ha).symm

Premises used: SameRay.nonneg_smul_right, SameRay.symm
-- Module: Mathlib.LinearAlgebra.Ray
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 : M
S : Type u_5
inst_5 : CommSemiring S
inst_6 : PartialOrder S
inst_7 : Algebra S R
inst_8 : Module S M
inst_9 : SMulPosMono S R
inst_10 : IsScalarTower S R M
a : S
h : SameRay R x y
ha : 0 < a
⊢ SameRay R x (a • y)

Tactic:
h.nonneg_smul_right ha.le

Premises used: SameRay.nonneg_smul_right, LT.lt.le
-- Module: Mathlib.LinearAlgebra.Ray
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 : M
S : Type u_5
inst_5 : CommSemiring S
inst_6 : PartialOrder S
inst_7 : Algebra S R
inst_8 : Module S M
inst_9 : SMulPosMono S R
inst_10 : IsScalarTower S R M
a : S
h : SameRay R x y
hr : 0 < a
⊢ SameRay R (a • x) y

Tactic:
h.nonneg_smul_left hr.le

Premises used: SameRay.nonneg_smul_left, LT.lt.le
-- Module: Mathlib.LinearAlgebra.Ray
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
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hx : x = 0
rw : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
rw₁ rw₂ : Eq.{u_3 + 1} (α := N) 0 0
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)

Tactic:
rw [hx, map_zero]

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.Ray
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
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hy : y = 0
rw : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
rw₁ rw₂ : Eq.{u_3 + 1} (α := N) 0 0
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) y : N) (0 : N)

Tactic:
rw [hy, map_zero]

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.Ray
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
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
f : M →ₗ[R] N
h_1 : SameRay R x y
h_2 : ∃ (r₁ : R) (r₂ : R), 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
rw : (f : (a : M) → N) (r₁ • x) = HSMul.hSMul (β := N) r₂ ((f : (a : M) → N) y : N)
rw₁ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (r₁ • x) : N) ((f : (a : M) → N) (r₂ • y) : N)
rw₂ rw₃ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (r₂ • y) : N) ((f : (a : M) → N) (r₂ • y) : N)
⊢ HSMul.hSMul (β := N) r₁ ((f : (a : M) → N) x : N) = HSMul.hSMul (β := N) r₂ ((f : (a : M) → N) y : N)

Tactic:
rw [← f.map_smul, ← f.map_smul, h]

Premises used: LinearMap.map_smul
-- Module: Mathlib.LinearAlgebra.Ray
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
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
F : Type u_6
inst_7 : FunLike F M N
inst_8 : LinearMapClass F R M N
f : F
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ SameRay.{u_1, u_3} R (M := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ↔ SameRay R x y

Tactic:
simp only [SameRay, map_zero, ← hf.eq_iff, map_smul]

Premises used: Function.Injective.eq_iff, map_zero, SameRay, map_smul
-- Module: Mathlib.LinearAlgebra.Ray
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
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
e : M ≃ₗ[R] N
⊢ SameRay.{u_1, u_3} R (M := N) ((e : (a : M) → N) x : N) ((e : (a : M) → N) y : N) ↔ SameRay R x y

Tactic:
Function.Injective.sameRay_map_iff (EquivLike.injective e)

Premises used: EquivLike.injective, Function.Injective.sameRay_map_iff
-- Module: Mathlib.LinearAlgebra.Ray
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 : M
S : Type u_6
inst_5 : Monoid S
inst_6 : DistribMulAction S M
inst_7 : SMulCommClass R S M
h : SameRay R x y
s : S
⊢ SameRay R (s • x) (s • y)

Tactic:
h.map (s • (LinearMap.id : M →ₗ[R] M))

Premises used: LinearMap.id, SameRay.map, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.Ray
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
inl : ∀ (hx : SameRay R 0 z), SameRay R (0 + y) z
inr : ∀ (hx₀ : x ≠ 0), SameRay R (x + y) z
⊢ SameRay R (x + y) z

Tactic:
rcases eq_or_ne x 0 with (rfl | hx₀)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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
y z : M
hy : SameRay R y z
hx : SameRay R 0 z
inl inl₁ inl₂ inl₃ : SameRay R y z
⊢ SameRay R (0 + y) z

Tactic:
rwa [zero_add]

Premises used: zero_add
-- Module: Mathlib.LinearAlgebra.Ray
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
inr : ∀ (hy : SameRay R 0 z), SameRay R (x + 0) z
inr₁ : ∀ (hy₀ : y ≠ 0), SameRay R (x + y) z
⊢ SameRay R (x + y) z

Tactic:
rcases eq_or_ne y 0 with (rfl | hy₀)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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 z : M
hx : SameRay R x z
hx₀ : x ≠ 0
hy : SameRay R 0 z
inr inr₁ inr₂ inr₃ : SameRay R x z
⊢ SameRay R (x + 0) z

Tactic:
rwa [add_zero]

Premises used: add_zero
-- Module: Mathlib.LinearAlgebra.Ray
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
inr : ∀ (hx : SameRay R x 0) (hy : SameRay R y 0), SameRay R (x + y) 0
inr₁ : ∀ (hz₀ : z ≠ 0), SameRay R (x + y) z
⊢ SameRay R (x + y) z

Tactic:
rcases eq_or_ne z 0 with (rfl | hz₀)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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 : M
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hx : SameRay R x 0
hy : SameRay R y 0
⊢ SameRay R (x + y) 0

Tactic:
apply zero_right

Premises used: SameRay.zero_right
-- Module: Mathlib.LinearAlgebra.Ray
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
inr : ∀ (rx rz₁ : R) (hrx : 0 < rx) (hrz₁ : 0 < rz₁) (Hx : rx • x = rz₁ • z), SameRay R (x + y) z
⊢ SameRay R (x + y) z

Tactic:
rcases hx.exists_pos hx₀ hz₀ with ⟨rx, rz₁, hrx, hrz₁, Hx⟩

Premises used: SameRay.exists_pos
-- Module: Mathlib.LinearAlgebra.Ray
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
inr : ∀ (ry rz₂ : R) (hry : 0 < ry) (hrz₂ : 0 < rz₂) (Hy : ry • y = rz₂ • z), SameRay R (x + y) z
⊢ SameRay R (x + y) z

Tactic:
rcases hy.exists_pos hy₀ hz₀ with ⟨ry, rz₂, hry, hrz₂, Hy⟩

Premises used: SameRay.exists_pos
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ SameRay R (x + y) z

Tactic:
Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, ?_, ?_⟩)

Premises used: HMul.hMul, mul_pos, HAdd.hAdd, And.intro, Exists.intro, SameRay, Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
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
inr : 0 < ry * rz₁ + rx * rz₂
inr₁ : (rx * ry) • (x + y) = (ry * rz₁ + rx * rz₂) • z
⊢ SameRay R (x + y) z

Tactic:
refine Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, ?_, ?_⟩)

Premises used: Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ 0 < ry * rz₁ + rx * rz₂

Tactic:
positivity
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ ry • rx • x + rx • ry • y = ry • rz₁ • z + rx • rz₂ • z

Tactic:
congr(ry • $Hx + rx • $Hy)

Premises used: congrArg, id, HAdd.hAdd, congr, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.Ray
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
h₁ : (ry * rz₁ + rx * rz₂) • z = ry • rz₁ • z + rx • rz₂ • z
⊢ (rx * ry) • (x + y) = (ry * rz₁ + rx * rz₂) • z

Tactic:
convert! congr(ry • $Hx + rx • $Hy) using 1
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ (rx * ry) • (x + y) = ry • rx • x + rx • ry • y

Tactic:
module
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ (ry * rz₁ + rx * rz₂) • z = ry • rz₁ • z + rx • rz₂ • z

Tactic:
module
-- Module: Mathlib.LinearAlgebra.Ray
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
hy : SameRay R x y
hz : SameRay R x z
⊢ SameRay R x (y + z)

Tactic:
(hy.symm.add_left hz.symm).symm

Premises used: SameRay.add_left, SameRay.symm
-- Module: Mathlib.LinearAlgebra.Ray
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
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
ι : Type u_4
inst_7 : DecidableEq ι
x y z : RayVector R M
hxy :
  SameRay.{u_1, u_2} R (M := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) x) : M)
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) y) : M)
hyz :
  SameRay.{u_1, u_2} R (M := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) y) : M)
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) z) : M)
⊢ SameRay.{u_1, u_2} R (M := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) x) : M)
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) z) : M)

Tactic:
hxy.trans hyz fun hy => (y.2 hy).elim

Premises used: False.elim, SameRay.trans, Subtype.property
-- Module: Mathlib.LinearAlgebra.Ray
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
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
ι : Type u_4
inst_7 : DecidableEq ι
x y z : RayVector R M
hxy :
  SameRay.{u_1, u_2} R (M := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) x) : M)
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) y) : M)
hyz :
  SameRay.{u_1, u_2} R (M := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) y) : M)
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) z) : M)
⊢ SameRay.{u_1, u_2} R (M := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) x) : M)
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) z) : M)

Tactic:
exact hxy.trans hyz fun hy => (y.2 hy).elim

Premises used: False.elim, SameRay.trans, Subtype.property
-- Module: Mathlib.LinearAlgebra.Ray
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
v₁ v₂ : RayVector R M
⊢ v₁ ≈ v₂ ↔
    SameRay.{u_1, u_2} R (M := M) (↑((RayVector.equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v₁) : M)
      (↑((RayVector.equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) v₂) : M)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.LinearAlgebra.Ray
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
C : Ray R M → Prop
h : ∀ (v : M) (hv : v ≠ 0), C (rayOfNeZero R v hv)
x : Ray R M
⊢ C x

Tactic:
Quotient.ind (Subtype.rec <| h) x

Premises used: Quotient.ind, Subtype.rec
-- Module: Mathlib.LinearAlgebra.Ray
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
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
ι : Type u_4
inst_7 : DecidableEq ι
inst_8 : Nontrivial M
⊢ Nonempty.{u_2 + 1} (Ray R M)

Tactic:
Nonempty.map Quotient.mk' inferInstance

Premises used: inferInstance, Quotient.mk', Nonempty.map
-- Module: Mathlib.LinearAlgebra.Ray
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
v₁ v₂ : M
hv₁ : v₁ ≠ 0
hv₂ : v₂ ≠ 0
⊢ Eq (α := Ray R M) (rayOfNeZero R v₁ hv₁) (rayOfNeZero R v₂ hv₂) ↔ SameRay R v₁ v₂

Tactic:
Quotient.eq'

Premises used: Module.Ray, rayOfNeZero, Quotient.eq', Quotient.mk'
-- Module: Mathlib.LinearAlgebra.Ray
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
v : M
h : v ≠ 0
r : R
hr : 0 < r
hrv : r • v ≠ 0
⊢ Eq (α := Ray R M) (rayOfNeZero R (r • v) hrv) (rayOfNeZero R v h)

Tactic:
(ray_eq_iff _ _).2 <| SameRay.sameRay_pos_smul_left v hr

Premises used: Iff.mpr, ray_eq_iff, SameRay.sameRay_pos_smul_left
-- Module: Mathlib.LinearAlgebra.Ray
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
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
e : M ≃ₗ[R] N
v : M
hv : v ≠ 0
⊢ Eq.{u_3 + 1} (α := Ray R N)
    (((map e : Equiv.{u_2 + 1, u_3 + 1} (Ray R M) (Ray R N)) : (a : Ray R M) → Ray R N) (rayOfNeZero R v hv) : Ray R N)
    (rayOfNeZero R ((e : (a : M) → N) v) ⋯ : Ray R N)

Tactic:
rfl

Premises used: rayOfNeZero, Quot.map, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ Eq (α := Ray R M ≃ Ray R M) (map (LinearEquiv.refl R M)) (Equiv.refl (Ray R M))

Tactic:
Equiv.ext <| Module.Ray.ind R fun _ _ => rfl

Premises used: Equiv.ext, rfl, Module.Ray.ind
-- Module: Mathlib.LinearAlgebra.Ray
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
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
e : M ≃ₗ[R] N
⊢ Eq (α := Equiv.{u_3 + 1, u_2 + 1} (Ray R N) (Ray R M)) (Equiv.symm (map e)) (map e.symm)

Tactic:
rfl

Premises used: Module.Ray, Module.Ray.map, Quotient, Quot.map, Quotient.congr, Quot.congr, Equiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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
e : M ≃ₗ[R] M
v : Ray R M
⊢ e • v = (map e : (a : Ray R M) → Ray R M) v

Tactic:
rfl

Premises used: Subtype.map, Quotient.map, Quot.map, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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
G : Type u_5
inst_5 : Group G
inst_6 : DistribMulAction G M
inst_7 : SMulCommClass R G M
g : G
v : M
hv : v ≠ 0
⊢ HSMul.hSMul (β := Ray R M) g (rayOfNeZero R v hv) = rayOfNeZero R (g • v) ⋯

Tactic:
rfl

Premises used: Subtype.map, rayOfNeZero, Quotient.map, Quot.map, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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
h : ∀ (v : M) (hv : v ≠ 0), HSMul.hSMul (β := Ray R M) u (rayOfNeZero R v hv) = rayOfNeZero R v hv
⊢ u • v = v

Tactic:
induction v using Module.Ray.ind

Premises used: Module.Ray.ind
-- Module: Mathlib.LinearAlgebra.Ray
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
h : SameRay R (u • v) v
⊢ HSMul.hSMul (β := Ray R M) u (rayOfNeZero R v hv) = rayOfNeZero R v hv

Tactic:
rw [smul_rayOfNeZero, ray_eq_iff]

Premises used: smul_rayOfNeZero, ray_eq_iff
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ SameRay R (u • v) v

Tactic:
SameRay.sameRay_pos_smul_left _ hu

Premises used: SameRay.sameRay_pos_smul_left
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ SameRay R (u • v) v

Tactic:
exact SameRay.sameRay_pos_smul_left _ hu

Premises used: SameRay.sameRay_pos_smul_left
-- Module: Mathlib.LinearAlgebra.Ray
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 : Ray R M
⊢ ⟦x.someRayVector⟧ = x

Tactic:
Quotient.out_eq _

Premises used: Quotient.out_eq, Module.Ray.someRayVector
-- Module: Mathlib.LinearAlgebra.Ray
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 : Ray R M
⊢ x.someVector ≠ 0

Tactic:
x.someRayVector.property

Premises used: Module.Ray.someVector, Subtype.property, Module.Ray.someRayVector
-- Module: Mathlib.LinearAlgebra.Ray
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 : Ray R M
⊢ rayOfNeZero R x.someVector ⋯ = x

Tactic:
(congr_arg _ (Subtype.coe_eta _ _) :).trans x.out_eq

Premises used: rayOfNeZero, congr_arg, Subtype.coe_eta, Quotient.out_eq, Module.Ray.someVector, Eq.trans
-- 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 y : M
⊢ SameRay R (-x) (-y) ↔ SameRay R x y

Tactic:
simp only [SameRay, neg_eq_zero, smul_neg, neg_inj]

Premises used: neg_eq_zero, smul_neg, neg_inj, SameRay
-- 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 y : M
rw : SameRay R (- -x) (-y) ↔ SameRay R x (-y)
rw₁ rw₂ : SameRay R x (-y) ↔ SameRay R x (-y)
⊢ SameRay R (-x) y ↔ SameRay R x (-y)

Tactic:
rw [← sameRay_neg_iff, neg_neg]

Premises used: neg_neg, 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
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
inr₁ : ∀ (r₁ r₂ : R) (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) (h : r₁ • x = r₂ • r • x), x = 0
⊢ x = 0

Tactic:
rcases h with (rfl | h₀ | ⟨r₁, r₂, hr₁, hr₂, h⟩)

Premises used: 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
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
r : R
hr : r < 0
⊢ Eq.{u_2 + 1} (α := M) 0 0

Tactic:
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
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₀ : r • x = 0
⊢ x = 0

Tactic:
simpa [hr.ne] using h₀

Premises used: LT.lt.ne
-- 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₁ • x = r₂ • r • x
⊢ r₁ - r₂ * r = 0 ∨ x = 0

Tactic:
rw [← sub_eq_zero, smul_smul, ← sub_smul, smul_eq_zero] at h

Premises used: sub_eq_zero, sub_smul, smul_smul, smul_eq_zero