awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p₃ : P
⊢ midpoint R p₁ p₂ -ᵥ midpoint R p₁ p₃ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
have rw : midpoint R (p₁ -ᵥ p₁) (p₂ -ᵥ p₃) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
Tactic: rw [midpoint_vsub_midpoint, vsub_self, midpoint_eq_smul_add, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p₃ : P
rw :
  midpoint R (p₁ -ᵥ p₁) (p₂ -ᵥ p₃) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
⊢ midpoint R p₁ p₂ -ᵥ midpoint R p₁ p₃ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
have rw₁ : midpoint R 0 (p₂ -ᵥ p₃) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
Tactic: rw [midpoint_vsub_midpoint, vsub_self, midpoint_eq_smul_add, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p₃ : P
rw :
  midpoint R (p₁ -ᵥ p₁) (p₂ -ᵥ p₃) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
rw₁ :
  midpoint R 0 (p₂ -ᵥ p₃) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
⊢ midpoint R p₁ p₂ -ᵥ midpoint R p₁ p₃ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
have rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (0 + (p₂ -ᵥ p₃)) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
Tactic: rw [midpoint_vsub_midpoint, vsub_self, midpoint_eq_smul_add, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p₃ : P
rw :
  midpoint R (p₁ -ᵥ p₁) (p₂ -ᵥ p₃) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
rw₁ :
  midpoint R 0 (p₂ -ᵥ p₃) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (0 + (p₂ -ᵥ p₃)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
⊢ midpoint R p₁ p₂ -ᵥ midpoint R p₁ p₃ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
have rw₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₂ -ᵥ p₃)
Tactic: rw [midpoint_vsub_midpoint, vsub_self, midpoint_eq_smul_add, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p₃ : P
⊢ midpoint R p₁ p₃ -ᵥ midpoint R p₂ p₃ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
have rw : midpoint R (p₁ -ᵥ p₂) (p₃ -ᵥ p₃) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
Tactic: rw [midpoint_vsub_midpoint, vsub_self, midpoint_eq_smul_add, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p₃ : P
rw :
  midpoint R (p₁ -ᵥ p₂) (p₃ -ᵥ p₃) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
⊢ midpoint R p₁ p₃ -ᵥ midpoint R p₂ p₃ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
have rw₁ : midpoint R (p₁ -ᵥ p₂) 0 =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
Tactic: rw [midpoint_vsub_midpoint, vsub_self, midpoint_eq_smul_add, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p₃ : P
rw :
  midpoint R (p₁ -ᵥ p₂) (p₃ -ᵥ p₃) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
rw₁ :
  midpoint R (p₁ -ᵥ p₂) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
⊢ midpoint R p₁ p₃ -ᵥ midpoint R p₂ p₃ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
have rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂ + 0) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
Tactic: rw [midpoint_vsub_midpoint, vsub_self, midpoint_eq_smul_add, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
p₁ p₂ p₃ : P
rw :
  midpoint R (p₁ -ᵥ p₂) (p₃ -ᵥ p₃) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
rw₁ :
  midpoint R (p₁ -ᵥ p₂) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂ + 0) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
⊢ midpoint R p₁ p₃ -ᵥ midpoint R p₂ p₃ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
have rw₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₂)
Tactic: rw [midpoint_vsub_midpoint, vsub_self, midpoint_eq_smul_add, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : Ring R'
inst_5 : Invertible (α := R') 2
inst_6 : AddCommGroup F
inst_7 : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ f (x + y) = f 0 + f (x + y)
have rw : f (x + y) = 0 + f (x + y)
Tactic: rw [h0, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : Ring R'
inst_5 : Invertible (α := R') 2
inst_6 : AddCommGroup F
inst_7 : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
rw : f (x + y) = 0 + f (x + y)
⊢ f (x + y) = f 0 + f (x + y)
have rw₁ : f (x + y) = f (x + y)
Tactic: rw [h0, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : Ring R'
inst_5 : Invertible (α := R') 2
inst_6 : AddCommGroup F
inst_7 : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ midpoint R' (f 0) (f (x + y)) + midpoint R' (f 0) (f (x + y)) = f (midpoint R x y) + f (midpoint R x y)
have rw : f (midpoint R 0 (x + y)) + f (midpoint R 0 (x + y)) = f (midpoint R x y) + f (midpoint R x y)
Tactic: rw [← hm, midpoint_zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : Ring R'
inst_5 : Invertible (α := R') 2
inst_6 : AddCommGroup F
inst_7 : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
rw : f (midpoint R 0 (x + y)) + f (midpoint R 0 (x + y)) = f (midpoint R x y) + f (midpoint R x y)
⊢ midpoint R' (f 0) (f (x + y)) + midpoint R' (f 0) (f (x + y)) = f (midpoint R x y) + f (midpoint R x y)
have rw₁ : f (midpoint R x y) + f (midpoint R x y) = f (midpoint R x y) + f (midpoint R x y)
Tactic: rw [← hm, midpoint_zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : Ring R'
inst_5 : Invertible (α := R') 2
inst_6 : AddCommGroup F
inst_7 : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ f (midpoint R x y) + f (midpoint R x y) = f x + f y
have rw : midpoint R' (f x) (f y) + midpoint R' (f x) (f y) = f x + f y
Tactic: rw [hm, midpoint_add_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Midpoint (goal)
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst : Ring R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : Ring R'
inst_5 : Invertible (α := R') 2
inst_6 : AddCommGroup F
inst_7 : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
rw : midpoint R' (f x) (f y) + midpoint R' (f x) (f y) = f x + f y
⊢ f (midpoint R x y) + f (midpoint R x y) = f x + f y
have rw₁ : f x + f y = f x + f y
Tactic: rw [hm, midpoint_add_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.MidpointZero (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing R
inst_1 : CharZero R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
a b : P
⊢ (lineMap a b : (a : R) → P) (1 / 2) = midpoint R a b
have rw : (lineMap a b : (a : R) → P) 2⁻¹ = midpoint R a b
Tactic: rw [one_div, lineMap_inv_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.MidpointZero (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing R
inst_1 : CharZero R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
a b : P
rw : (lineMap a b : (a : R) → P) 2⁻¹ = midpoint R a b
⊢ (lineMap a b : (a : R) → P) (1 / 2) = midpoint R a b
have rw₁ : midpoint R a b = midpoint R a b
Tactic: rw [one_div, lineMap_inv_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.MidpointZero (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
a b : P
⊢ (homothety a (1 / 2) : (a : P) → P) b = midpoint k a b
have rw : (homothety a 2⁻¹ : (a : P) → P) b = midpoint k a b
Tactic: rw [one_div, homothety_inv_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.MidpointZero (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
a b : P
rw : (homothety a 2⁻¹ : (a : P) → P) b = midpoint k a b
⊢ (homothety a (1 / 2) : (a : P) → P) b = midpoint k a b
have rw₁ : midpoint k a b = midpoint k a b
Tactic: rw [one_div, homothety_inv_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a a' b : E
r : k
ha : a ≤ a'
hr : r ≤ 1
⊢ LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a' b : (a : k) → E) r : E)
have simp : (1 - r) • a + r • b ≤ (1 - r) • a' + r • b
Tactic: simp only [lineMap_apply_module]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a a' b : E
r : k
ha : a ≤ a'
hr : r ≤ 1
⊢ (1 - r) • a + r • b ≤ (1 - r) • a' + r • b
have bc : 0 ≤ 1 - r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a a' b : E
r : k
ha : a < a'
hr : r < 1
⊢ LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a' b : (a : k) → E) r : E)
have simp : (1 - r) • a + r • b < (1 - r) • a' + r • b
Tactic: simp only [lineMap_apply_module]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a a' b : E
r : k
ha : a < a'
hr : r < 1
⊢ (1 - r) • a + r • b < (1 - r) • a' + r • b
have bc : 0 < 1 - r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
a b b' : E
r : k
hb : b ≤ b'
hr : 0 ≤ r
⊢ LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b' : (a : k) → E) r : E)
have simp : (1 - r) • a + r • b ≤ (1 - r) • a + r • b'
Tactic: simp only [lineMap_apply_module]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
a b b' : E
r : k
hb : b < b'
hr : 0 < r
⊢ LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b' : (a : k) → E) r : E)
have simp : (1 - r) • a + r • b < (1 - r) • a + r • b'
Tactic: simp only [lineMap_apply_module]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a a' b b' : E
r : k
ha : a < a'
hb : b < b'
h₀ : 0 ≤ r
h₁ : r ≤ 1
⊢ LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a' b' : (a : k) → E) r : E)
have inl : ∀ (h₀ : LE.le.{u_1} (α := k) 0 0) (h₁ : LE.le.{u_1} (α := k) 0 1),
  LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) 0 : E) ((lineMap a' b' : (a : k) → E) 0 : E)
Tactic: rcases h₀.eq_or_lt with (rfl | h₀)
Cleared hypotheses: r, h₀, h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a a' b b' : E
r : k
ha : a < a'
hb : b < b'
h₀ : 0 ≤ r
h₁ : r ≤ 1
inl :
  ∀ (h₀ : LE.le.{u_1} (α := k) 0 0) (h₁ : LE.le.{u_1} (α := k) 0 1),
    LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) 0 : E) ((lineMap a' b' : (a : k) → E) 0 : E)
⊢ LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a' b' : (a : k) → E) r : E)
have inr : ∀ (h₀ : 0 < r), LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a' b' : (a : k) → E) r : E)
Tactic: rcases h₀.eq_or_lt with (rfl | h₀)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a b : E
r r' : k
inst_8 : PosSMulReflectLT k E
h : r < r'
⊢ LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) r' : E) ↔ a < b
have simp : (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
Tactic: simp only [lineMap_apply_module]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a b : E
r r' : k
inst_8 : PosSMulReflectLT k E
h : r < r'
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
have rw : (1 - r) • a < (1 - r') • a + r' • b - r • b ↔ a < b
Tactic: rw [← lt_sub_iff_add_lt, add_sub_assoc, ← sub_lt_iff_lt_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_lt_smul_iff_of_pos_left (sub_pos.2 h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a b : E
r r' : k
inst_8 : PosSMulReflectLT k E
h : r < r'
rw : (1 - r) • a < (1 - r') • a + r' • b - r • b ↔ a < b
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
have rw₁ : (1 - r) • a < (1 - r') • a + (r' • b - r • b) ↔ a < b
Tactic: rw [← lt_sub_iff_add_lt, add_sub_assoc, ← sub_lt_iff_lt_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_lt_smul_iff_of_pos_left (sub_pos.2 h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a b : E
r r' : k
inst_8 : PosSMulReflectLT k E
h : r < r'
rw : (1 - r) • a < (1 - r') • a + r' • b - r • b ↔ a < b
rw₁ : (1 - r) • a < (1 - r') • a + (r' • b - r • b) ↔ a < b
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
have rw₂ : (1 - r) • a - (1 - r') • a < r' • b - r • b ↔ a < b
Tactic: rw [← lt_sub_iff_add_lt, add_sub_assoc, ← sub_lt_iff_lt_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_lt_smul_iff_of_pos_left (sub_pos.2 h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a b : E
r r' : k
inst_8 : PosSMulReflectLT k E
h : r < r'
rw : (1 - r) • a < (1 - r') • a + r' • b - r • b ↔ a < b
rw₁ : (1 - r) • a < (1 - r') • a + (r' • b - r • b) ↔ a < b
rw₂ : (1 - r) • a - (1 - r') • a < r' • b - r • b ↔ a < b
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
have rw₃ : (1 - r - (1 - r')) • a < r' • b - r • b ↔ a < b
Tactic: rw [← lt_sub_iff_add_lt, add_sub_assoc, ← sub_lt_iff_lt_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_lt_smul_iff_of_pos_left (sub_pos.2 h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a b : E
r r' : k
inst_8 : PosSMulReflectLT k E
h : r < r'
rw : (1 - r) • a < (1 - r') • a + r' • b - r • b ↔ a < b
rw₁ : (1 - r) • a < (1 - r') • a + (r' • b - r • b) ↔ a < b
rw₂ : (1 - r) • a - (1 - r') • a < r' • b - r • b ↔ a < b
rw₃ : (1 - r - (1 - r')) • a < r' • b - r • b ↔ a < b
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
have rw₄ : (1 - r - (1 - r')) • a < (r' - r) • b ↔ a < b
Tactic: rw [← lt_sub_iff_add_lt, add_sub_assoc, ← sub_lt_iff_lt_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_lt_smul_iff_of_pos_left (sub_pos.2 h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a b : E
r r' : k
inst_8 : PosSMulReflectLT k E
h : r < r'
rw : (1 - r) • a < (1 - r') • a + r' • b - r • b ↔ a < b
rw₁ : (1 - r) • a < (1 - r') • a + (r' • b - r • b) ↔ a < b
rw₂ : (1 - r) • a - (1 - r') • a < r' • b - r • b ↔ a < b
rw₃ : (1 - r - (1 - r')) • a < r' • b - r • b ↔ a < b
rw₄ : (1 - r - (1 - r')) • a < (r' - r) • b ↔ a < b
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
have rw₅ : (r' - r) • a < (r' - r) • b ↔ a < b
Tactic: rw [← lt_sub_iff_add_lt, add_sub_assoc, ← sub_lt_iff_lt_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_lt_smul_iff_of_pos_left (sub_pos.2 h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a b : E
r r' : k
inst_8 : PosSMulReflectLT k E
h : r < r'
rw : (1 - r) • a < (1 - r') • a + r' • b - r • b ↔ a < b
rw₁ : (1 - r) • a < (1 - r') • a + (r' • b - r • b) ↔ a < b
rw₂ : (1 - r) • a - (1 - r') • a < r' • b - r • b ↔ a < b
rw₃ : (1 - r - (1 - r')) • a < r' • b - r • b ↔ a < b
rw₄ : (1 - r - (1 - r')) • a < (r' - r) • b ↔ a < b
rw₅ : (r' - r) • a < (r' - r) • b ↔ a < b
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
have rw₆ : a < b ↔ a < b
Tactic: rw [← lt_sub_iff_add_lt, add_sub_assoc, ← sub_lt_iff_lt_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_lt_smul_iff_of_pos_left (sub_pos.2 h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : PartialOrder k
inst_2 : IsOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
a b : E
r : k
inst_8 : PosSMulReflectLT k E
h : 0 < r
⊢ a < (lineMap a b : (a : k) → E) r ↔
    LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) 0 : E) ((lineMap a b : (a : k) → E) r : E)
have rw : a < (lineMap a b : (a : k) → E) r ↔ a < (lineMap a b : (a : k) → E) r
Tactic: rw [lineMap_apply_zero]