awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
hx : ¬x = 0
pos : ∀ (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)
have neg : ∀ (hy : ¬y = 0), SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ (r₂⁻¹ * r₁) • x = y
have rw : r₂⁻¹ • r₁ • x = y
Tactic: rw [mul_smul, h, inv_smul_smul₀ hr₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ (r₂⁻¹ * r₁) • x = y
have rw₁ : r₂⁻¹ • r₂ • y = y
Tactic: rw [mul_smul, h, inv_smul_smul₀ hr₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ (r₂⁻¹ * r₁) • x = y
have rw₂ : y = y
Tactic: rw [mul_smul, h, inv_smul_smul₀ hr₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ ∃ (r : R), 0 ≤ r ∧ r • x = y
have inl : ∀ (h : SameRay R x 0), ∃ (r : R), 0 ≤ r ∧ r • x = 0
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ ∃ (r : R), 0 ≤ r ∧ r • x = y
have inr : ∀ (hy : y ≠ 0), ∃ (r : R), 0 ≤ r ∧ r • x = y
Tactic: obtain rfl | hy := eq_or_ne y 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
have inl : ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ 0 = a • (0 + v₂) ∧ v₂ = b • (0 + v₂)
Tactic: rcases h with (rfl | rfl | ⟨r₁, r₂, h₁, h₂, H⟩)
Cleared hypotheses: v₁, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂)
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
have inr : ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + 0) ∧ 0 = b • (v₁ + 0)
Tactic: rcases h with (rfl | rfl | ⟨r₁, r₂, h₁, h₂, H⟩)
Cleared hypotheses: v₂, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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)
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
have 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₂)
Tactic: rcases h with (rfl | rfl | ⟨r₁, r₂, h₁, h₂, H⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ 0 = a • (0 + v₂) ∧ v₂ = b • (0 + v₂)
have 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₂)
Tactic: use 0, 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + 0) ∧ 0 = b • (v₁ + 0)
have 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)
Tactic: use 1, 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (hypothesis)
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₂
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
have h₁₂ : 0 < r₁ + r₂
Tactic: have h₁₂ : 0 < r₁ + r₂ := add_pos h₁ h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂)
have inr : r₂ / (r₁ + r₂) + r₁ / (r₁ + r₂) = 1
Tactic: refine
      ⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
have inr₁ : v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)
Tactic: refine
      ⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂)
⊢ ∃ (a : R) (b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
have inr₂ : v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
Tactic: refine
      ⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂
⊢ r₂ / (r₁ + r₂) + r₁ / (r₁ + r₂) = 1
have inr : (r₂ + r₁) / (r₁ + r₂) = 1
Tactic: rw [← add_div, add_comm, div_self h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ r₂ / (r₁ + r₂) + r₁ / (r₁ + r₂) = 1
have inr₁ : (r₁ + r₂) / (r₁ + r₂) = 1
Tactic: rw [← add_div, add_comm, div_self h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ r₂ / (r₁ + r₂) + r₁ / (r₁ + r₂) = 1
have inr₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [← add_div, add_comm, div_self h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)
have inr : 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']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂)
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)
have inr₁ : 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']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂)
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)
have inr₂ : v₁ = (r₁ + r₂)⁻¹ • (r₂ • v₁ + r₂ • v₂)
Tactic: rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂)
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)
have inr₃ : v₁ = (r₁ + r₂)⁻¹ • (r₂ • v₁ + r₁ • v₁)
Tactic: rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₁)
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)
have inr₄ : v₁ = (r₁ + r₂)⁻¹ • (r₂ + r₁) • v₁
Tactic: rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₁
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)
have inr₅ : v₁ = (r₁ + r₂)⁻¹ • (r₁ + r₂) • v₁
Tactic: rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₁
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)
have inr₆ : v₁ = v₁
Tactic: rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
have inr : 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']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂)
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
have inr₁ : 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']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂)
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
have inr₂ : v₂ = (r₁ + r₂)⁻¹ • (r₁ • v₁ + r₁ • v₂)
Tactic: rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂)
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
have inr₃ : v₂ = (r₁ + r₂)⁻¹ • (r₂ • v₂ + r₁ • v₂)
Tactic: rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂)
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
have inr₄ : v₂ = (r₁ + r₂)⁻¹ • (r₂ + r₁) • v₂
Tactic: rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
have inr₅ : v₂ = (r₁ + r₂)⁻¹ • (r₁ + r₂) • v₂
Tactic: rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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₂
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
have inr₆ : v₂ = v₂
Tactic: rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
have refine : ∀ (h : ∃ (r : R), 0 < r ∧ r • x = y), SameRay R x y
Tactic: refine ⟨fun h => ?_, fun h => h.exists_pos_left hx hy⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ SameRay R x y
have rcases : ∀ (r : R) (hr : 0 < r) (hy : r • x ≠ 0), SameRay R x (r • x)
Tactic: rcases h with ⟨r, hr, rfl⟩
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 ∧ y ≠ 0
have mp : (∃ (r : R), 0 < r ∧ r • x = y) → SameRay R x y ∧ y ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ (∃ (r : R), 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0
have mpr : SameRay R x y ∧ y ≠ 0 → ∃ (r : R), 0 < r ∧ r • x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
have refine : ∀ (h : ∃ (r : R), 0 ≤ r ∧ r • x = y), SameRay R x y
Tactic: refine ⟨fun h => ?_, fun h => h.exists_nonneg_left hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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
⊢ SameRay R x y
have rcases : ∀ (r : R) (hr : 0 ≤ r), SameRay R x (r • x)
Tactic: rcases h with ⟨r, hr, rfl⟩
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 ∧ x = r • y) ↔ SameRay R x y
have rw : (∃ (r : R), 0 < r ∧ x = r • y) ↔ SameRay R y x
Tactic: rw [SameRay.sameRay_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 ∧ x = r • y) ↔ SameRay R y x
have simp_rw : (∃ (r : R), 0 < r ∧ r • y = x) ↔ SameRay R y x
Tactic: simp_rw [eq_comm (a := x)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0
have rw : (∃ (r : R), 0 < r ∧ x = r • y) ↔ SameRay R y x ∧ x ≠ 0
Tactic: rw [SameRay.sameRay_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 ∧ x = r • y) ↔ SameRay R y x ∧ x ≠ 0
have simp_rw : (∃ (r : R), 0 < r ∧ r • y = x) ↔ SameRay R y x ∧ x ≠ 0
Tactic: simp_rw [eq_comm (a := x)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 ∧ x = r • y) ↔ SameRay R x y
have rw : (∃ (r : R), 0 ≤ r ∧ x = r • y) ↔ SameRay R y x
Tactic: rw [SameRay.sameRay_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
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 ∧ x = r • y) ↔ SameRay R y x
have simp_rw : (∃ (r : R), 0 ≤ r ∧ r • y = x) ↔ SameRay R y x
Tactic: simp_rw [eq_comm (a := x)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
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)
⊢ (preReflection x f : (a : M) → M) x = -x
have rw : x - (x + x) = -x
Tactic: rw [preReflection_apply, h, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
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
g : Dual R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
⊢ preReflection ((preReflection x f : (a : M) → M) y)
      (((preReflection (R := R) f ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x) : End R (Dual R M)) :
          (a : Dual R M) → Dual R M)
        g) =
    preReflection x f ∘ₗ preReflection y g ∘ₗ preReflection x f
have h₁ : ∀ (m : M),
  Eq (α := M)
    (((preReflection ((preReflection x f : (a : M) → M) y)
              (((preReflection (R := R) f ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x) : End R (Dual R M)) :
                  (a : Dual R M) → Dual R M)
                g) :
            End R M) :
          (a : M) → M)
        m :
      M)
    ((preReflection x f ∘ₗ preReflection y g ∘ₗ preReflection x f : (a : M) → M) m : M)
Tactic: ext m