awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
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 [← 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)]

Premises used: Iff.mpr, sub_pos, add_sub_assoc, smul_le_smul_iff_of_pos_left, sub_smul, sub_le_iff_le_add', le_sub_iff_add_le, sub_sub_sub_cancel_left
-- 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 : k
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 ↔
    LE.le.{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 : 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
⊢ a ≤ midpoint k a b ↔ a ≤ b

Tactic:
left_le_lineMap_iff_le <| inv_pos.2 zero_lt_two

Premises used: Iff.mpr, inv_pos, left_le_lineMap_iff_le, zero_lt_two, midpoint
-- 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 : k
h : 0 < r
⊢ (lineMap a b : (a : k) → E) r ≤ a ↔ b ≤ a

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

Premises used: left_le_lineMap_iff_le
-- 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
⊢ midpoint k a b ≤ a ↔ b ≤ a

Tactic:
lineMap_le_left_iff_le <| inv_pos.2 zero_lt_two

Premises used: Iff.mpr, inv_pos, lineMap_le_left_iff_le, zero_lt_two, midpoint
-- 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 : k
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 ↔
    LE.le.{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 : 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
⊢ midpoint k a b ≤ b ↔ a ≤ b

Tactic:
lineMap_le_right_iff_le two_inv_lt_one

Premises used: two_inv_lt_one, lineMap_le_right_iff_le, midpoint
-- 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 : k
h : r < 1
⊢ b ≤ (lineMap a b : (a : k) → E) r ↔ b ≤ a

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

Premises used: lineMap_le_right_iff_le
-- 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
⊢ b ≤ midpoint k a b ↔ b ≤ a

Tactic:
right_le_lineMap_iff_le two_inv_lt_one

Premises used: two_inv_lt_one, right_le_lineMap_iff_le, midpoint
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
⊢ (lineMap (f a) (f b) : (a : k) → E) r ≤ f ((lineMap a b : (a : k) → k) r) ↔
    slope f a b ≤ slope f a ((lineMap a b : (a : k) → k) r)

Tactic:
map_le_lineMap_iff_slope_le_slope_left (E := Eᵒᵈ) (f := f) (a := a) (b := b) (r := r) h

Premises used: map_le_lineMap_iff_slope_le_slope_left, OrderDual
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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

Tactic:
lt_iff_lt_of_le_iff_le' (lineMap_le_map_iff_slope_le_slope_left h)
    (map_le_lineMap_iff_slope_le_slope_left h)

Premises used: lt_iff_lt_of_le_iff_le', map_le_lineMap_iff_slope_le_slope_left, lineMap_le_map_iff_slope_le_slope_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
⊢ (lineMap (f a) (f b) : (a : k) → E) r < f ((lineMap a b : (a : k) → k) r) ↔
    slope f a b < slope f a ((lineMap a b : (a : k) → k) r)

Tactic:
map_lt_lineMap_iff_slope_lt_slope_left (E := Eᵒᵈ) (f := f) (a := a) (b := b) (r := r) h

Premises used: map_lt_lineMap_iff_slope_lt_slope_left, OrderDual
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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 < (1 - r) * (b - a)
rw :
  f ((lineMap b a : (a : k) → k) (1 - r)) ≤ (lineMap (f b) (f a) : (a : k) → E) (1 - r) ↔
    slope f a b ≤ slope f ((lineMap b a : (a : k) → k) (1 - r)) b
⊢ f ((lineMap a b : (a : k) → k) r) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔
    slope f a b ≤ slope f ((lineMap a b : (a : k) → k) r) b

Tactic:
rw [← lineMap_apply_one_sub, ← lineMap_apply_one_sub _ _ r]

Premises used: AffineMap.lineMap_apply_one_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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 < (1 - r) * (b - a)
revert :
  ∀ (h : 0 < (1 - r) * (b - a)),
    f ((lineMap b a : (a : k) → k) (1 - r)) ≤ (lineMap (f b) (f a) : (a : k) → E) (1 - r) ↔
      slope f a b ≤ slope f ((lineMap b a : (a : k) → k) (1 - r)) b
⊢ f ((lineMap b a : (a : k) → k) (1 - r)) ≤ (lineMap (f b) (f a) : (a : k) → E) (1 - r) ↔
    slope f a b ≤ slope f ((lineMap b a : (a : k) → k) (1 - r)) b

Tactic:
revert h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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
generalize :
  ∀ (r' : k) (h : 0 < r' * (b - a)),
    f ((lineMap b a : (a : k) → k) r') ≤ (lineMap (f b) (f a) : (a : k) → E) r' ↔
      slope f a b ≤ slope f ((lineMap b a : (a : k) → k) r') b
⊢ ∀ (h : 0 < (1 - r) * (b - a)),
    f ((lineMap b a : (a : k) → k) (1 - r)) ≤ (lineMap (f b) (f a) : (a : k) → E) (1 - r) ↔
      slope f a b ≤ slope f ((lineMap b a : (a : k) → k) (1 - r)) b

Tactic:
generalize 1 - r = r'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
simp_rw :
  f (r' * (a - b) + b) ≤ r' • (f a - f b) + f b ↔
    (b - a)⁻¹ • (f b - f a) ≤ (b - (r' * (a - b) + b))⁻¹ • (f b - f (r' * (a - b) + b))
⊢ f ((lineMap b a : (a : k) → k) r') ≤ (lineMap (f b) (f a) : (a : k) → E) r' ↔
    slope f a b ≤ slope f ((lineMap b a : (a : k) → k) r') b

Tactic:
simp_rw [lineMap_apply, slope, vsub_eq_sub, vadd_eq_add, smul_eq_mul]

Premises used: slope, AffineMap.lineMap_apply, vadd_eq_add, smul_eq_mul, vsub_eq_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
h₁ : b - a ≠ 0
⊢ f (r' * (a - b) + b) ≤ r' • (f a - f b) + f b ↔
    (b - a)⁻¹ • (f b - f a) ≤ (b - (r' * (a - b) + b))⁻¹ • (f b - f (r' * (a - b) + b))

Tactic:
rw [sub_add_eq_sub_sub_swap, sub_self, zero_sub, neg_mul_eq_mul_neg, neg_sub,
    le_inv_smul_iff_of_pos h, smul_smul, mul_inv_cancel_right₀, le_sub_comm, ← neg_sub (f b),
    smul_neg, neg_add_eq_sub]

Premises used: neg_sub, sub_self, neg_add_eq_sub, smul_smul, smul_neg, mul_inv_cancel_right₀, neg_mul_eq_mul_neg, zero_sub, le_inv_smul_iff_of_pos, le_sub_comm, sub_add_eq_sub_sub_swap
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
⊢ b - a ≠ 0

Tactic:
right_ne_zero_of_mul h.ne'

Premises used: right_ne_zero_of_mul, LT.lt.ne'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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)
⊢ b - a ≠ 0

Tactic:
exact right_ne_zero_of_mul h.ne'

Premises used: right_ne_zero_of_mul, LT.lt.ne'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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 < (1 - r) * (b - a)
⊢ (lineMap (f a) (f b) : (a : k) → E) r ≤ f ((lineMap a b : (a : k) → k) r) ↔
    slope f ((lineMap a b : (a : k) → k) r) b ≤ slope f a b

Tactic:
map_le_lineMap_iff_slope_le_slope_right (E := Eᵒᵈ) (f := f) (a := a) (b := b) (r := r) h

Premises used: map_le_lineMap_iff_slope_le_slope_right, OrderDual
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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 < (1 - r) * (b - a)
⊢ f ((lineMap a b : (a : k) → k) r) < (lineMap (f a) (f b) : (a : k) → E) r ↔
    slope f a b < slope f ((lineMap a b : (a : k) → k) r) b

Tactic:
lt_iff_lt_of_le_iff_le' (lineMap_le_map_iff_slope_le_slope_right h)
    (map_le_lineMap_iff_slope_le_slope_right h)

Premises used: lineMap_le_map_iff_slope_le_slope_right, map_le_lineMap_iff_slope_le_slope_right, lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
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 < (1 - r) * (b - a)
⊢ (lineMap (f a) (f b) : (a : k) → E) r < f ((lineMap a b : (a : k) → k) r) ↔
    slope f ((lineMap a b : (a : k) → k) r) b < slope f a b

Tactic:
map_lt_lineMap_iff_slope_lt_slope_right (E := Eᵒᵈ) (f := f) (a := a) (b := b) (r := r) h

Premises used: map_lt_lineMap_iff_slope_lt_slope_right, OrderDual
-- 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
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
rw :
  slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f a b ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b
rw₁ :
  slope f a ((lineMap a b : (a : k) → k) r) ≤
      (lineMap (slope f ((lineMap a b : (a : k) → k) r) b) (slope f a ((lineMap a b : (a : k) → k) r)) : (a : k) → E)
        r ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b
rw₂ rw₃ :
  slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) 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 ((lineMap a b : (a : k) → k) r) b

Tactic:
rw [map_le_lineMap_iff_slope_le_slope_left (mul_pos h₀ (sub_pos.2 hab)), ←
    lineMap_slope_lineMap_slope_lineMap f a b r, right_le_lineMap_iff_le h₁]

Premises used: Iff.mpr, sub_pos, right_le_lineMap_iff_le, mul_pos, map_le_lineMap_iff_slope_le_slope_left, lineMap_slope_lineMap_slope_lineMap
-- 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
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ (lineMap (f a) (f b) : (a : k) → E) r ≤ f ((lineMap a b : (a : k) → k) r) ↔
    slope f ((lineMap a b : (a : k) → k) r) b ≤ slope f a ((lineMap a b : (a : k) → k) r)

Tactic:
map_le_lineMap_iff_slope_le_slope (E := Eᵒᵈ) hab h₀ h₁

Premises used: map_le_lineMap_iff_slope_le_slope, OrderDual
-- 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
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ 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 ((lineMap a b : (a : k) → k) r) b

Tactic:
lt_iff_lt_of_le_iff_le' (lineMap_le_map_iff_slope_le_slope hab h₀ h₁)
    (map_le_lineMap_iff_slope_le_slope hab h₀ h₁)

Premises used: lt_iff_lt_of_le_iff_le', lineMap_le_map_iff_slope_le_slope, map_le_lineMap_iff_slope_le_slope
-- 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
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ (lineMap (f a) (f b) : (a : k) → E) r < f ((lineMap a b : (a : k) → k) r) ↔
    slope f ((lineMap a b : (a : k) → k) r) b < slope f a ((lineMap a b : (a : k) → k) r)

Tactic:
map_lt_lineMap_iff_slope_lt_slope (E := Eᵒᵈ) hab h₀ h₁

Premises used: OrderDual, map_lt_lineMap_iff_slope_lt_slope
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : x₀ < b
⊢ 0 < slope f x₀ b ↔ f x₀ < f b

Tactic:
simp [slope, hb]

Premises used: slope
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : b < x₀
rw : 0 < slope f b x₀ ↔ f b < f x₀
rw₁ rw₂ : f b < f x₀ ↔ f b < f x₀
⊢ 0 < slope f x₀ b ↔ f b < f x₀

Tactic:
rw [slope_comm, slope_pos_iff hb]

Premises used: slope_comm, slope_pos_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : x₀ < b
hbf : 0 < slope f x₀ b
hf : f x₀ = 0
⊢ 0 < f b

Tactic:
simp_all [slope]

Premises used: slope
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : b < x₀
hbf : 0 < slope f x₀ b
hf : f x₀ = 0
rwa : b < x₀
⊢ f b < 0

Tactic:
rwa [slope_pos_iff_gt, hf] at hbf

Premises used: slope_pos_iff_gt
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : b < x₀
hbf : 0 < slope f x₀ b
hf : f x₀ = 0
⊢ b < x₀

Tactic:
hb
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ordered
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : b < x₀
hbf : 0 < slope f x₀ b
hf : f x₀ = 0
⊢ b < x₀

Tactic:
exact hb
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
s : AffineSubspace k P
⊢ (↑(v +ᵥ s) : Set P) = v +ᵥ (↑s : Set P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
s : AffineSubspace k P
⊢ v +ᵥ s = map (↑(AffineEquiv.constVAdd k P v) : P →ᵃ[k] P) s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
s : AffineSubspace k P
p : P
⊢ v +ᵥ p ∈ v +ᵥ s ↔ p ∈ s

Tactic:
vadd_mem_vadd_set_iff

Premises used: Set.Mem, Set.vadd_mem_vadd_set_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
h : ∀ (x : P), x ∈ HVAdd.hVAdd (β := AffineSubspace k P) v ⊥ ↔ Membership.mem (γ := AffineSubspace k P) ⊥ x
⊢ HVAdd.hVAdd (β := AffineSubspace k P) v ⊥ = ⊥

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
x : P
⊢ x ∈ HVAdd.hVAdd (β := AffineSubspace k P) v ⊥ ↔ Membership.mem (γ := AffineSubspace k P) ⊥ x

Tactic:
simp [pointwise_vadd_eq_map, map_bot]

Premises used: AffineSubspace.pointwise_vadd_eq_map, AffineSubspace.map_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
h : ∀ (x : P), x ∈ HVAdd.hVAdd (β := AffineSubspace k P) v ⊤ ↔ Membership.mem (γ := AffineSubspace k P) ⊤ x
⊢ HVAdd.hVAdd (β := AffineSubspace k P) v ⊤ = ⊤

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
x : P
⊢ x ∈ HVAdd.hVAdd (β := AffineSubspace k P) v ⊤ ↔ Membership.mem (γ := AffineSubspace k P) ⊤ x

Tactic:
simp [pointwise_vadd_eq_map, vadd_eq_iff_eq_neg_vadd]

Premises used: vadd_eq_iff_eq_neg_vadd, AffineSubspace.pointwise_vadd_eq_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
s : AffineSubspace k P
rw : Submodule.map (AffineMap.linear (↑(AffineEquiv.constVAdd k P v) : P →ᵃ[k] P)) s.direction = s.direction
⊢ (v +ᵥ s).direction = s.direction

Tactic:
rw [pointwise_vadd_eq_map, map_direction]

Premises used: AffineSubspace.map_direction, AffineSubspace.pointwise_vadd_eq_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
s : AffineSubspace k P
⊢ Submodule.map (AffineMap.linear (↑(AffineEquiv.constVAdd k P v) : P →ᵃ[k] P)) s.direction = s.direction

Tactic:
Submodule.map_id _

Premises used: Submodule.map_id
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
s : AffineSubspace k P
⊢ Submodule.map (AffineMap.linear (↑(AffineEquiv.constVAdd k P v) : P →ᵃ[k] P)) s.direction = s.direction

Tactic:
exact Submodule.map_id _

Premises used: Submodule.map_id
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
s : Set P
⊢ HVAdd.hVAdd (β := AffineSubspace k P) v (affineSpan k s) = affineSpan k (v +ᵥ s)

Tactic:
map_span _ s

Premises used: AffineSubspace.map_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
rw :
  map (f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁)) s =
    map (AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f) s
⊢ map f (v +ᵥ s) = HVAdd.hVAdd.{u_7, u_8, u_8} (α := V₂) ((f.linear : (a : V₁) → V₂) v : V₂) (map f s)

Tactic:
rw [pointwise_vadd_eq_map, pointwise_vadd_eq_map, map_map, map_map]

Premises used: AffineSubspace.pointwise_vadd_eq_map, AffineSubspace.map_map