awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
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
neg : m 0 • x = m 1 • -y
⊢ SameRay R x y ∨ SameRay R x (-y)

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

Premises used: Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ (i : Fin (Nat.succ 0).succ), m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
neg neg₁ neg₂ neg₃ : m 0 • x = -(m 1 • y)
⊢ m 0 • x = m 1 • -y

Tactic:
rwa [smul_neg]

Premises used: smul_neg
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
rw : 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) ↔ ¬LinearIndependent R ![x, y]

Tactic:
rw [← sameRay_or_sameRay_neg_iff_not_linearIndependent]

Premises used: sameRay_or_sameRay_neg_iff_not_linearIndependent
-- 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 ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
neg : ∀ (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)

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 ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)

Tactic:
simp [hx]
-- 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 ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
neg : ∀ (hy : ¬y = 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)

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 ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)

Tactic:
simp [hx, hy]
-- 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 ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)

Tactic:
simp [hx, hy]
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
h_1 : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
rw : r₂⁻¹ • r₁ • x = y
rw₁ : r₂⁻¹ • r₂ • y = y
rw₂ rw₃ : y = y
⊢ (r₂⁻¹ * r₁) • x = y

Tactic:
rw [mul_smul, h, inv_smul_smul₀ hr₂.ne']

Premises used: inv_smul_smul₀, LT.lt.ne', SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ (r : R), 0 < r ∧ x = r • y

Tactic:
(h.symm.exists_pos_left hy hx).imp fun _ => And.imp_right Eq.symm

Premises used: Exists.imp, SameRay.symm, And.imp_right, SameRay.exists_pos_left, Eq.symm
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
h : SameRay R x y
hx : x ≠ 0
inl : ∀ (h : SameRay R x 0), ∃ (r : R), 0 ≤ r ∧ r • x = 0
inr : ∀ (hy : y ≠ 0), ∃ (r : R), 0 ≤ r ∧ r • x = y
⊢ ∃ (r : R), 0 ≤ r ∧ r • x = y

Tactic:
obtain rfl | hy := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
hx : x ≠ 0
h : SameRay R x 0
⊢ ∃ (r : R), 0 ≤ r ∧ r • x = 0

Tactic:
⟨0, le_rfl, zero_smul _ _⟩

Premises used: le_rfl, zero_smul, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
hx : x ≠ 0
h : SameRay R x 0
⊢ ∃ (r : R), 0 ≤ r ∧ r • x = 0

Tactic:
exact ⟨0, le_rfl, zero_smul _ _⟩
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ (r : R), 0 ≤ r ∧ r • x = y

Tactic:
(h.exists_pos_left hx hy).imp fun _ => And.imp_left le_of_lt

Premises used: le_of_lt, And.imp_left, Exists.imp, SameRay.exists_pos_left
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ (r : R), 0 ≤ r ∧ r • x = y

Tactic:
exact (h.exists_pos_left hx hy).imp fun _ => And.imp_left le_of_lt

Premises used: le_of_lt, And.imp_left, Exists.imp, SameRay.exists_pos_left
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
h : SameRay R x y
hy : y ≠ 0
⊢ ∃ (r : R), 0 ≤ r ∧ x = r • y

Tactic:
(h.symm.exists_nonneg_left hy).imp fun _ => And.imp_right Eq.symm

Premises used: Exists.imp, SameRay.symm, SameRay.exists_nonneg_left, And.imp_right, Eq.symm
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field 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 : SameRay R v₁ v₂
inl : ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ 0 = a • (0 + v₂) ∧ v₂ = b • (0 + v₂)
inr : ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + 0) ∧ 0 = b • (v₁ + 0)
inr₁ :
  ∀ (r₁ r₂ : R) (h₁ : 0 < r₁) (h₂ : 0 < r₂) (H : r₁ • v₁ = r₂ • v₂),
    ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)

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

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
v₂ : M
h :
  LE.le.{u_1} (α := R) 0 0 ∧
    LE.le.{u_1} (α := R) 0 1 ∧
      HAdd.hAdd (α := R) 0 1 = 1 ∧
        0 = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (0 + v₂) ∧ v₂ = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (0 + v₂)
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ 0 = a • (0 + v₂) ∧ v₂ = b • (0 + v₂)

Tactic:
use 0, 1
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
v₂ : M
⊢ LE.le.{u_1} (α := R) 0 0 ∧
    LE.le.{u_1} (α := R) 0 1 ∧
      HAdd.hAdd (α := R) 0 1 = 1 ∧
        0 = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (0 + v₂) ∧ v₂ = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (0 + v₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
v₁ : M
h :
  LE.le.{u_1} (α := R) 0 1 ∧
    LE.le.{u_1} (α := R) 0 0 ∧
      HAdd.hAdd (α := R) 1 0 = 1 ∧
        v₁ = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (v₁ + 0) ∧ 0 = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (v₁ + 0)
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + 0) ∧ 0 = b • (v₁ + 0)

Tactic:
use 1, 0
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
v₁ : M
⊢ LE.le.{u_1} (α := R) 0 1 ∧
    LE.le.{u_1} (α := R) 0 0 ∧
      HAdd.hAdd (α := R) 1 0 = 1 ∧
        v₁ = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (v₁ + 0) ∧ 0 = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (v₁ + 0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field 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
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
⊢ 0 < r₁ + r₂

Tactic:
have h₁₂ : 0 < r₁ + r₂ := add_pos h₁ h₂
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field 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
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)

Tactic:
⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, ?_, ?_, ?_⟩

Premises used: HDiv.hDiv, LT.lt.le, HAdd.hAdd, And.intro, Exists.intro, div_nonneg
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field 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
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
inr : r₂ / (r₁ + r₂) + r₁ / (r₁ + r₂) = 1
inr₁ : v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)
inr₂ : v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)

Tactic:
refine
      ⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, ?_, ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field 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
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
inr : (r₂ + r₁) / (r₁ + r₂) = 1
inr₁ : (r₁ + r₂) / (r₁ + r₂) = 1
inr₂ inr₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ r₂ / (r₁ + r₂) + r₁ / (r₁ + r₂) = 1

Tactic:
rw [← add_div, add_comm, div_self h₁₂.ne']

Premises used: add_comm, LT.lt.ne', div_self, add_div
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field 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
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
inr : v₁ = ((r₁ + r₂)⁻¹ * r₂) • (v₁ + v₂)
inr₁ : v₁ = (r₁ + r₂)⁻¹ • r₂ • (v₁ + v₂)
inr₂ : v₁ = (r₁ + r₂)⁻¹ • (r₂ • v₁ + r₂ • v₂)
inr₃ : v₁ = (r₁ + r₂)⁻¹ • (r₂ • v₁ + r₁ • v₁)
inr₄ : v₁ = (r₁ + r₂)⁻¹ • (r₂ + r₁) • v₁
inr₅ : v₁ = (r₁ + r₂)⁻¹ • (r₁ + r₂) • v₁
inr₆ inr₇ : v₁ = v₁
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)

Tactic:
rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']

Premises used: inv_smul_smul₀, add_comm, LT.lt.ne', add_smul, div_eq_inv_mul, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field 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
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
inr : v₂ = ((r₁ + r₂)⁻¹ * r₁) • (v₁ + v₂)
inr₁ : v₂ = (r₁ + r₂)⁻¹ • r₁ • (v₁ + v₂)
inr₂ : v₂ = (r₁ + r₂)⁻¹ • (r₁ • v₁ + r₁ • v₂)
inr₃ : v₂ = (r₁ + r₂)⁻¹ • (r₂ • v₂ + r₁ • v₂)
inr₄ : v₂ = (r₁ + r₂)⁻¹ • (r₂ + r₁) • v₂
inr₅ : v₂ = (r₁ + r₂)⁻¹ • (r₁ + r₂) • v₂
inr₆ inr₇ : v₂ = v₂
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)

Tactic:
rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']

Premises used: inv_smul_smul₀, add_comm, LT.lt.ne', add_smul, div_eq_inv_mul, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field 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 : SameRay R v₁ v₂
⊢ ∃ (u : M) (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • u ∧ v₂ = b • u

Tactic:
⟨v₁ + v₂, h.exists_eq_smul_add⟩

Premises used: SameRay.exists_eq_smul_add, HAdd.hAdd, Exists.intro
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ (r : R), 0 < r ∧ r • x = y) ↔ SameRay R x y

Tactic:
⟨fun h => ?_, fun h => h.exists_pos_left hx hy⟩

Premises used: Iff.intro, SameRay.exists_pos_left
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
refine : ∀ (h : ∃ (r : R), 0 < r ∧ r • x = y), SameRay R x y
⊢ (∃ (r : R), 0 < r ∧ r • x = y) ↔ SameRay R x y

Tactic:
refine ⟨fun h => ?_, fun h => h.exists_pos_left hx hy⟩
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
h : ∃ (r : R), 0 < r ∧ r • x = y
rcases : ∀ (r : R) (hr : 0 < r) (hy : r • x ≠ 0), SameRay R x (r • x)
⊢ SameRay R x y

Tactic:
rcases h with ⟨r, hr, rfl⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
hy : r • x ≠ 0
⊢ SameRay R x (r • x)

Tactic:
SameRay.sameRay_pos_smul_right x hr

Premises used: SameRay.sameRay_pos_smul_right
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
hy : r • x ≠ 0
⊢ SameRay R x (r • x)

Tactic:
exact SameRay.sameRay_pos_smul_right x hr

Premises used: SameRay.sameRay_pos_smul_right
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
mp : (∃ (r : R), 0 < r ∧ r • x = y) → SameRay R x y ∧ y ≠ 0
mpr : SameRay R x y ∧ y ≠ 0 → ∃ (r : R), 0 < r ∧ r • x = y
⊢ (∃ (r : R), 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
⊢ SameRay R x (r • x) ∧ r • x ≠ 0

Tactic:
simp [hx, hr.le, hr.ne']

Premises used: LT.lt.le, LT.lt.ne'
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
hxy : SameRay R x y
hy : y ≠ 0
⊢ ∃ (r : R), 0 < r ∧ r • x = y

Tactic:
(exists_pos_left_iff_sameRay hx hy).2 hxy

Premises used: Iff.mpr, exists_pos_left_iff_sameRay
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
hxy : SameRay R x y
hy : y ≠ 0
⊢ ∃ (r : R), 0 < r ∧ r • x = y

Tactic:
exact (exists_pos_left_iff_sameRay hx hy).2 hxy

Premises used: Iff.mpr, exists_pos_left_iff_sameRay
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ (r : R), 0 ≤ r ∧ r • x = y) ↔ SameRay R x y

Tactic:
⟨fun h => ?_, fun h => h.exists_nonneg_left hx⟩

Premises used: SameRay.exists_nonneg_left, Iff.intro
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
refine : ∀ (h : ∃ (r : R), 0 ≤ r ∧ r • x = y), SameRay R x y
⊢ (∃ (r : R), 0 ≤ r ∧ r • x = y) ↔ SameRay R x y

Tactic:
refine ⟨fun h => ?_, fun h => h.exists_nonneg_left hx⟩
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
h : ∃ (r : R), 0 ≤ r ∧ r • x = y
rcases : ∀ (r : R) (hr : 0 ≤ r), SameRay R x (r • x)
⊢ SameRay R x y

Tactic:
rcases h with ⟨r, hr, rfl⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 ≤ r
⊢ SameRay R x (r • x)

Tactic:
SameRay.sameRay_nonneg_smul_right x hr

Premises used: SameRay.sameRay_nonneg_smul_right
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 ≤ r
⊢ SameRay R x (r • x)

Tactic:
exact SameRay.sameRay_nonneg_smul_right x hr

Premises used: SameRay.sameRay_nonneg_smul_right
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
rw : (∃ (r : R), 0 < r ∧ x = r • y) ↔ SameRay R y x
⊢ (∃ (r : R), 0 < r ∧ x = r • y) ↔ SameRay R x y

Tactic:
rw [SameRay.sameRay_comm]

Premises used: SameRay.sameRay_comm
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
simp_rw : (∃ (r : R), 0 < r ∧ r • y = x) ↔ SameRay R y x
⊢ (∃ (r : R), 0 < r ∧ x = r • y) ↔ SameRay R y x

Tactic:
simp_rw [eq_comm (a := x)]

Premises used: eq_comm
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ (r : R), 0 < r ∧ r • y = x) ↔ SameRay R y x

Tactic:
exists_pos_left_iff_sameRay hy hx

Premises used: exists_pos_left_iff_sameRay
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ (r : R), 0 < r ∧ r • y = x) ↔ SameRay R y x

Tactic:
exact exists_pos_left_iff_sameRay hy hx

Premises used: exists_pos_left_iff_sameRay
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hy : y ≠ 0
rw : (∃ (r : R), 0 < r ∧ x = r • y) ↔ SameRay R y x ∧ x ≠ 0
⊢ (∃ (r : R), 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0

Tactic:
rw [SameRay.sameRay_comm]

Premises used: SameRay.sameRay_comm
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hy : y ≠ 0
simp_rw : (∃ (r : R), 0 < r ∧ r • y = x) ↔ SameRay R y x ∧ x ≠ 0
⊢ (∃ (r : R), 0 < r ∧ x = r • y) ↔ SameRay R y x ∧ x ≠ 0

Tactic:
simp_rw [eq_comm (a := x)]

Premises used: eq_comm
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ (r : R), 0 < r ∧ r • y = x) ↔ SameRay R y x ∧ x ≠ 0

Tactic:
exists_pos_left_iff_sameRay_and_ne_zero hy

Premises used: exists_pos_left_iff_sameRay_and_ne_zero
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ (r : R), 0 < r ∧ r • y = x) ↔ SameRay R y x ∧ x ≠ 0

Tactic:
exact exists_pos_left_iff_sameRay_and_ne_zero hy

Premises used: exists_pos_left_iff_sameRay_and_ne_zero
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hy : y ≠ 0
rw : (∃ (r : R), 0 ≤ r ∧ x = r • y) ↔ SameRay R y x
⊢ (∃ (r : R), 0 ≤ r ∧ x = r • y) ↔ SameRay R x y

Tactic:
rw [SameRay.sameRay_comm]

Premises used: SameRay.sameRay_comm
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hy : y ≠ 0
simp_rw : (∃ (r : R), 0 ≤ r ∧ r • y = x) ↔ SameRay R y x
⊢ (∃ (r : R), 0 ≤ r ∧ x = r • y) ↔ SameRay R y x

Tactic:
simp_rw [eq_comm (a := x)]

Premises used: eq_comm
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ (r : R), 0 ≤ r ∧ r • y = x) ↔ SameRay R y x

Tactic:
exists_nonneg_left_iff_sameRay (R := R) hy

Premises used: exists_nonneg_left_iff_sameRay
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ (r : R), 0 ≤ r ∧ r • y = x) ↔ SameRay R y x

Tactic:
exact exists_nonneg_left_iff_sameRay (R := R) hy

Premises used: exists_nonneg_left_iff_sameRay
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
⊢ (preReflection x f : (a : M) → M) y = y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x

Tactic:
simp [preReflection]

Premises used: Module.preReflection
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
rw : x - (x + x) = -x
⊢ (preReflection x f : (a : M) → M) x = -x

Tactic:
rw [preReflection_apply, h, two_smul]

Premises used: two_smul, Module.preReflection_apply
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
⊢ x - (x + x) = -x

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
y : M
⊢ (preReflection x f : (a : M) → M) ((preReflection x f : (a : M) → M) y : M) = y

Tactic:
simp [map_sub, h, two_smul, preReflection_apply]

Premises used: map_sub, two_smul, Module.preReflection_apply