awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : r < 1
⊢ (lineMap a b : (a : k) → E) r < b ↔
    LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) 1 : E)
have rw : (lineMap a b : (a : k) → E) r < b ↔ (lineMap a b : (a : k) → E) r < b
Tactic: rw [lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) r' : E) ↔ r ≤ r'
have simp : r • (b - a) + a ≤ r' • (b - a) + a ↔ r ≤ r'
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 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ r • (b - a) + a ≤ r' • (b - a) + a ↔ r ≤ r'
have rw : r • (b - a) ≤ r' • (b - a) ↔ r ≤ r'
Tactic: rw [add_le_add_iff_right, smul_le_smul_iff_of_pos_right (sub_pos.mpr 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 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
rw : r • (b - a) ≤ r' • (b - a) ↔ r ≤ r'
⊢ r • (b - a) + a ≤ r' • (b - a) + a ↔ r ≤ r'
have rw₁ : r ≤ r' ↔ r ≤ r'
Tactic: rw [add_le_add_iff_right, smul_le_smul_iff_of_pos_right (sub_pos.mpr 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 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ a ≤ (lineMap a b : (a : k) → E) r ↔ 0 ≤ r
have rw : a ≤ (lineMap a b : (a : k) → E) r ↔
  LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) 0 : E) ((lineMap a b : (a : k) → E) r : E)
Tactic: rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
rw :
  a ≤ (lineMap a b : (a : k) → E) r ↔
    LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) 0 : E) ((lineMap a b : (a : k) → E) r : E)
⊢ a ≤ (lineMap a b : (a : k) → E) r ↔ 0 ≤ r
have rw₁ : a ≤ (lineMap a b : (a : k) → E) r ↔ a ≤ (lineMap a b : (a : k) → E) r
Tactic: rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ (lineMap a b : (a : k) → E) r ≤ a ↔ r ≤ 0
have rw : (lineMap a b : (a : k) → E) r ≤ a ↔
  LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) 0 : E)
Tactic: rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
rw :
  (lineMap a b : (a : k) → E) r ≤ a ↔
    LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) 0 : E)
⊢ (lineMap a b : (a : k) → E) r ≤ a ↔ r ≤ 0
have rw₁ : (lineMap a b : (a : k) → E) r ≤ a ↔ (lineMap a b : (a : k) → E) r ≤ a
Tactic: rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ b ≤ (lineMap a b : (a : k) → E) r ↔ 1 ≤ r
have rw : b ≤ (lineMap a b : (a : k) → E) r ↔
  LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) 1 : E) ((lineMap a b : (a : k) → E) r : E)
Tactic: rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
rw :
  b ≤ (lineMap a b : (a : k) → E) r ↔
    LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) 1 : E) ((lineMap a b : (a : k) → E) r : E)
⊢ b ≤ (lineMap a b : (a : k) → E) r ↔ 1 ≤ r
have rw₁ : b ≤ (lineMap a b : (a : k) → E) r ↔ b ≤ (lineMap a b : (a : k) → E) r
Tactic: rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ (lineMap a b : (a : k) → E) r ≤ b ↔ r ≤ 1
have rw : (lineMap a b : (a : k) → E) r ≤ b ↔
  LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) 1 : E)
Tactic: rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
rw :
  (lineMap a b : (a : k) → E) r ≤ b ↔
    LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) 1 : E)
⊢ (lineMap a b : (a : k) → E) r ≤ b ↔ r ≤ 1
have rw₁ : (lineMap a b : (a : k) → E) r ≤ b ↔ (lineMap a b : (a : k) → E) r ≤ b
Tactic: rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) r' : E) ↔ r < r'
have simp : r • (b - a) + a < r' • (b - a) + a ↔ r < r'
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 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ r • (b - a) + a < r' • (b - a) + a ↔ r < r'
have rw : r • (b - a) < r' • (b - a) ↔ r < r'
Tactic: rw [add_lt_add_iff_right, smul_lt_smul_iff_of_pos_right (sub_pos.mpr 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 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
rw : r • (b - a) < r' • (b - a) ↔ r < r'
⊢ r • (b - a) + a < r' • (b - a) + a ↔ r < r'
have rw₁ : r < r' ↔ r < r'
Tactic: rw [add_lt_add_iff_right, smul_lt_smul_iff_of_pos_right (sub_pos.mpr 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 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ a < (lineMap a b : (a : k) → E) r ↔ 0 < r
have rw : 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)
Tactic: rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
rw :
  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)
⊢ a < (lineMap a b : (a : k) → E) r ↔ 0 < r
have rw₁ : a < (lineMap a b : (a : k) → E) r ↔ a < (lineMap a b : (a : k) → E) r
Tactic: rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ (lineMap a b : (a : k) → E) r < a ↔ r < 0
have rw : (lineMap a b : (a : k) → E) r < a ↔
  LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) 0 : E)
Tactic: rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
rw :
  (lineMap a b : (a : k) → E) r < a ↔
    LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) 0 : E)
⊢ (lineMap a b : (a : k) → E) r < a ↔ r < 0
have rw₁ : (lineMap a b : (a : k) → E) r < a ↔ (lineMap a b : (a : k) → E) r < a
Tactic: rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ b < (lineMap a b : (a : k) → E) r ↔ 1 < r
have rw : b < (lineMap a b : (a : k) → E) r ↔
  LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) 1 : E) ((lineMap a b : (a : k) → E) r : E)
Tactic: rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
rw :
  b < (lineMap a b : (a : k) → E) r ↔
    LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) 1 : E) ((lineMap a b : (a : k) → E) r : E)
⊢ b < (lineMap a b : (a : k) → E) r ↔ 1 < r
have rw₁ : b < (lineMap a b : (a : k) → E) r ↔ b < (lineMap a b : (a : k) → E) r
Tactic: rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
⊢ (lineMap a b : (a : k) → E) r < b ↔ r < 1
have rw : (lineMap a b : (a : k) → E) r < b ↔
  LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) 1 : E)
Tactic: rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing 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
h : a < b
rw :
  (lineMap a b : (a : k) → E) r < b ↔
    LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) 1 : E)
⊢ (lineMap a b : (a : k) → E) r < b ↔ r < 1
have rw₁ : (lineMap a b : (a : k) → E) r < b ↔ (lineMap a b : (a : k) → E) r < b
Tactic: rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
a b : E
r r' : k
h : r < r'
⊢ LE.le.{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 : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
a b : E
r r' : k
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 [← le_sub_iff_add_le, add_sub_assoc, ← sub_le_iff_le_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_le_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 : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
a b : E
r r' : k
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 [← le_sub_iff_add_le, add_sub_assoc, ← sub_le_iff_le_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_le_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 : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
a b : E
r r' : k
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 [← le_sub_iff_add_le, add_sub_assoc, ← sub_le_iff_le_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_le_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 : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
a b : E
r r' : k
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 [← le_sub_iff_add_le, add_sub_assoc, ← sub_le_iff_le_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_le_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 : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
a b : E
r r' : k
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 [← le_sub_iff_add_le, add_sub_assoc, ← sub_le_iff_le_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_le_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 : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
a b : E
r r' : k
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 [← le_sub_iff_add_le, add_sub_assoc, ← sub_le_iff_le_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_le_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 : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
a b : E
r r' : k
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 [← le_sub_iff_add_le, add_sub_assoc, ← sub_le_iff_le_add', ← sub_smul, ← sub_smul,
    sub_sub_sub_cancel_left, smul_le_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 : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
a b : E
r : k
h : 0 < r
⊢ a ≤ (lineMap a b : (a : k) → E) r ↔
    LE.le.{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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
a b : E
r : k
h : r < 1
⊢ (lineMap a b : (a : k) → E) r ≤ b ↔
    LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) 1 : E)
have rw : (lineMap a b : (a : k) → E) r ≤ b ↔ (lineMap a b : (a : k) → E) r ≤ b
Tactic: rw [lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
inst_7 : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f ((lineMap a b : (a : k) → k) r) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f a b
have rw : f (r • (b -ᵥ a) +ᵥ a) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
Tactic: rw [lineMap_apply, lineMap_apply, slope, slope, vsub_eq_sub, vsub_eq_sub, vsub_eq_sub,
    vadd_eq_add, vadd_eq_add, smul_eq_mul, add_sub_cancel_right, smul_sub, smul_sub, smul_sub,
    sub_le_iff_le_add, mul_inv_rev, mul_smul, mul_smul, ← smul_sub, ← smul_sub, ← smul_add,
    smul_smul, ← mul_inv_rev, inv_smul_le_iff_of_pos h, smul_smul,
    mul_inv_cancel_right₀ (right_ne_zero_of_mul h.ne'), smul_add,
    smul_inv_smul₀ (left_ne_zero_of_mul h.ne')]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
inst_7 : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
rw : f (r • (b -ᵥ a) +ᵥ a) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
⊢ f ((lineMap a b : (a : k) → k) r) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f a b
have rw₁ : f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
Tactic: rw [lineMap_apply, lineMap_apply, slope, slope, vsub_eq_sub, vsub_eq_sub, vsub_eq_sub,
    vadd_eq_add, vadd_eq_add, smul_eq_mul, add_sub_cancel_right, smul_sub, smul_sub, smul_sub,
    sub_le_iff_le_add, mul_inv_rev, mul_smul, mul_smul, ← smul_sub, ← smul_sub, ← smul_add,
    smul_smul, ← mul_inv_rev, inv_smul_le_iff_of_pos h, smul_smul,
    mul_inv_cancel_right₀ (right_ne_zero_of_mul h.ne'), smul_add,
    smul_inv_smul₀ (left_ne_zero_of_mul h.ne')]