awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.MidpointZero
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
rw₁ rw₂ : midpoint R a b = midpoint R a b
⊢ (lineMap a b : (a : R) → P) (1 / 2) = midpoint R a b

Tactic:
rw [one_div, lineMap_inv_two]

Premises used: lineMap_inv_two, one_div
-- Module: Mathlib.LinearAlgebra.AffineSpace.MidpointZero
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : Invertible (α := R) 2
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
a b : P
⊢ (homothety a (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) : (a : P) → P) b = midpoint R a b

Tactic:
rfl

Premises used: midpoint, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.MidpointZero
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 2⁻¹ : (a : P) → P) b = midpoint k a b

Tactic:
rfl

Premises used: midpoint, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.MidpointZero
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
rw₁ rw₂ : midpoint k a b = midpoint k a b
⊢ (homothety a (1 / 2) : (a : P) → P) b = midpoint k a b

Tactic:
rw [one_div, homothety_inv_two]

Premises used: one_div, homothety_inv_two
-- Module: Mathlib.LinearAlgebra.AffineSpace.MidpointZero
Goal:
k : Type u_1
ι : Type u_2
V : ι → Type u_3
P : ι → Type u_4
inst : Ring k
inst_1 : Invertible (α := k) 2
inst_2 : (i : ι) → AddCommGroup (V i)
inst_3 : (i : ι) → Module.{u_1, u_3} k (V i)
inst_4 : (i : ι) → AddTorsor.{u_3, u_4} (V i) (P i)
f g : (i : ι) → P i
i : ι
⊢ midpoint k f g i = midpoint k (f i) (g i)

Tactic:
rfl

Premises used: midpoint, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
simp : (1 - r) • a + r • b ≤ (1 - r) • a' + r • b
⊢ LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a' b : (a : k) → E) r : E)

Tactic:
simp only [lineMap_apply_module]

Premises used: AffineMap.lineMap_apply_module
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
bc : 0 ≤ 1 - r
⊢ (1 - r) • a + r • b ≤ (1 - r) • a' + r • b

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
⊢ 0 ≤ 1 - r

Tactic:
sub_nonneg.2 hr

Premises used: Iff.mpr, sub_nonneg
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
⊢ 0 ≤ 1 - r

Tactic:
exact sub_nonneg.2 hr

Premises used: Iff.mpr, sub_nonneg
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
simp : (1 - r) • a + r • b < (1 - r) • a' + r • b
⊢ LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a' b : (a : k) → E) r : E)

Tactic:
simp only [lineMap_apply_module]

Premises used: AffineMap.lineMap_apply_module
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
bc : 0 < 1 - r
⊢ (1 - r) • a + r • b < (1 - r) • a' + r • b

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
⊢ 0 < 1 - r

Tactic:
sub_pos.2 hr

Premises used: Iff.mpr, sub_pos
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
⊢ 0 < 1 - r

Tactic:
exact sub_pos.2 hr

Premises used: Iff.mpr, sub_pos
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
simp : (1 - r) • a + r • b ≤ (1 - r) • a + r • b'
⊢ LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b' : (a : k) → E) r : E)

Tactic:
simp only [lineMap_apply_module]

Premises used: AffineMap.lineMap_apply_module
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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 bc : 0 ≤ r
⊢ (1 - r) • a + r • b ≤ (1 - r) • a + r • b'

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
simp : (1 - r) • a + r • b < (1 - r) • a + r • b'
⊢ LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b' : (a : k) → E) r : E)

Tactic:
simp only [lineMap_apply_module]

Premises used: AffineMap.lineMap_apply_module
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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 bc : 0 < r
⊢ (1 - r) • a + r • b < (1 - r) • a + r • b'

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
⊢ LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a' b' : (a : k) → E) r : E)

Tactic:
(lineMap_mono_left ha h₁).trans (lineMap_mono_right hb h₀)

Premises used: LE.le.trans, lineMap_mono_left, lineMap_mono_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
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)
⊢ 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₀)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
ha : a < a'
hb : b < b'
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:
simpa
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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₀_1 : 0 ≤ r
h₁ : r ≤ 1
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:
(lineMap_mono_left ha.le h₁).trans_lt (lineMap_strict_mono_right hb h₀)

Premises used: LT.lt.le, lineMap_mono_left, LE.le.trans_lt, lineMap_strict_mono_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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₀_1 : 0 ≤ r
h₁ : r ≤ 1
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:
exact (lineMap_mono_left ha.le h₁).trans_lt (lineMap_strict_mono_right hb h₀)

Premises used: LT.lt.le, lineMap_mono_left, LE.le.trans_lt, lineMap_strict_mono_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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'
simp : (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
⊢ LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) r' : E) ↔ a < b

Tactic:
simp only [lineMap_apply_module]

Premises used: AffineMap.lineMap_apply_module
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
rw₆ rw₇ : a < b ↔ a < b
⊢ (1 - r) • a + r • b < (1 - r') • a + 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)]

Premises used: Iff.mpr, sub_pos, add_sub_assoc, sub_smul, sub_lt_iff_lt_add', smul_lt_smul_iff_of_pos_left, lt_sub_iff_add_lt, sub_sub_sub_cancel_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
rw rw₁ : a < (lineMap a b : (a : k) → E) r ↔ a < (lineMap a b : (a : k) → E) 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)

Tactic:
rw [lineMap_apply_zero]

Premises used: AffineMap.lineMap_apply_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
⊢ (lineMap a b : (a : k) → E) r < a ↔ b < a

Tactic:
left_lt_lineMap_iff_lt (E := Eᵒᵈ) h

Premises used: left_lt_lineMap_iff_lt
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
rw rw₁ : (lineMap a b : (a : k) → E) r < b ↔ (lineMap a b : (a : k) → E) r < b
⊢ (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_apply_one]

Premises used: AffineMap.lineMap_apply_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
⊢ b < (lineMap a b : (a : k) → E) r ↔ b < a

Tactic:
lineMap_lt_right_iff_lt (E := Eᵒᵈ) h

Premises used: lineMap_lt_right_iff_lt
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
simp : r • (b - a) + a ≤ r' • (b - a) + a ↔ r ≤ r'
⊢ LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) r' : E) ↔ r ≤ r'

Tactic:
simp only [lineMap_apply_module']

Premises used: AffineMap.lineMap_apply_module'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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'
rw₁ rw₂ : r ≤ r' ↔ r ≤ r'
⊢ r • (b - a) + a ≤ r' • (b - a) + a ↔ r ≤ r'

Tactic:
rw [add_le_add_iff_right, smul_le_smul_iff_of_pos_right (sub_pos.mpr h)]

Premises used: Iff.mpr, sub_pos, smul_le_smul_iff_of_pos_right, add_le_add_iff_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
rw₁ rw₂ : a ≤ (lineMap a b : (a : k) → E) r ↔ a ≤ (lineMap a b : (a : k) → E) r
⊢ a ≤ (lineMap a b : (a : k) → E) r ↔ 0 ≤ r

Tactic:
rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_zero]

Premises used: lineMap_le_lineMap_iff_of_lt', AffineMap.lineMap_apply_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
rw₁ rw₂ : (lineMap a b : (a : k) → E) r ≤ a ↔ (lineMap a b : (a : k) → E) r ≤ a
⊢ (lineMap a b : (a : k) → E) r ≤ a ↔ r ≤ 0

Tactic:
rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_zero]

Premises used: lineMap_le_lineMap_iff_of_lt', AffineMap.lineMap_apply_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
rw₁ rw₂ : b ≤ (lineMap a b : (a : k) → E) r ↔ b ≤ (lineMap a b : (a : k) → E) r
⊢ b ≤ (lineMap a b : (a : k) → E) r ↔ 1 ≤ r

Tactic:
rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_one]

Premises used: lineMap_le_lineMap_iff_of_lt', AffineMap.lineMap_apply_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
rw₁ rw₂ : (lineMap a b : (a : k) → E) r ≤ b ↔ (lineMap a b : (a : k) → E) r ≤ b
⊢ (lineMap a b : (a : k) → E) r ≤ b ↔ r ≤ 1

Tactic:
rw [← lineMap_le_lineMap_iff_of_lt' h, lineMap_apply_one]

Premises used: lineMap_le_lineMap_iff_of_lt', AffineMap.lineMap_apply_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
simp : r • (b - a) + a < r' • (b - a) + a ↔ r < r'
⊢ LT.lt.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) r' : E) ↔ r < r'

Tactic:
simp only [lineMap_apply_module']

Premises used: AffineMap.lineMap_apply_module'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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'
rw₁ rw₂ : r < r' ↔ r < r'
⊢ r • (b - a) + a < r' • (b - a) + a ↔ r < r'

Tactic:
rw [add_lt_add_iff_right, smul_lt_smul_iff_of_pos_right (sub_pos.mpr h)]

Premises used: Iff.mpr, sub_pos, smul_lt_smul_iff_of_pos_right, add_lt_add_iff_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
rw₁ rw₂ : a < (lineMap a b : (a : k) → E) r ↔ a < (lineMap a b : (a : k) → E) r
⊢ a < (lineMap a b : (a : k) → E) r ↔ 0 < r

Tactic:
rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_zero]

Premises used: AffineMap.lineMap_apply_zero, lineMap_lt_lineMap_iff_of_lt'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
rw₁ rw₂ : (lineMap a b : (a : k) → E) r < a ↔ (lineMap a b : (a : k) → E) r < a
⊢ (lineMap a b : (a : k) → E) r < a ↔ r < 0

Tactic:
rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_zero]

Premises used: AffineMap.lineMap_apply_zero, lineMap_lt_lineMap_iff_of_lt'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
rw₁ rw₂ : b < (lineMap a b : (a : k) → E) r ↔ b < (lineMap a b : (a : k) → E) r
⊢ b < (lineMap a b : (a : k) → E) r ↔ 1 < r

Tactic:
rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_one]

Premises used: AffineMap.lineMap_apply_one, lineMap_lt_lineMap_iff_of_lt'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
rw₁ rw₂ : (lineMap a b : (a : k) → E) r < b ↔ (lineMap a b : (a : k) → E) r < b
⊢ (lineMap a b : (a : k) → E) r < b ↔ r < 1

Tactic:
rw [← lineMap_lt_lineMap_iff_of_lt' h, lineMap_apply_one]

Premises used: AffineMap.lineMap_apply_one, lineMap_lt_lineMap_iff_of_lt'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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 a' b b' : E
inst_8 : Invertible (α := k) 2
ha : a ≤ a'
hb : b ≤ b'
⊢ midpoint k a b ≤ midpoint k a' b'

Tactic:
lineMap_mono_endpoints ha hb (invOf_nonneg.2 zero_le_two) <| invOf_le_one one_le_two

Premises used: Iff.mpr, invOf_nonneg, lineMap_mono_endpoints, one_le_two, zero_le_two, midpoint, invOf_le_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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'
simp : (1 - r) • a + r • b ≤ (1 - r') • a + r' • b ↔ a ≤ b
⊢ LE.le.{u_2} (α := E) ((lineMap a b : (a : k) → E) r : E) ((lineMap a b : (a : k) → E) r' : E) ↔ a ≤ b

Tactic:
simp only [lineMap_apply_module]

Premises used: AffineMap.lineMap_apply_module