[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a ≤ a'
hr : r ≤ 1
⊢ ↑(lineMap a b) r ≤ ↑(lineMap a' b) r
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a ≤ a'
hr : r ≤ 1
⊢ (1 - r) • a + r • b ≤ (1 - r) • a' + r • b
[PROOFSTEP]
exact add_le_add_right (smul_le_smul_of_nonneg ha (sub_nonneg.2 hr)) _
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a < a'
hr : r < 1
⊢ ↑(lineMap a b) r < ↑(lineMap a' b) r
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a < a'
hr : r < 1
⊢ (1 - r) • a + r • b < (1 - r) • a' + r • b
[PROOFSTEP]
exact add_lt_add_right (smul_lt_smul_of_pos ha (sub_pos.2 hr)) _
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
hb : b ≤ b'
hr : 0 ≤ r
⊢ ↑(lineMap a b) r ≤ ↑(lineMap a b') r
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
hb : b ≤ b'
hr : 0 ≤ r
⊢ (1 - r) • a + r • b ≤ (1 - r) • a + r • b'
[PROOFSTEP]
exact add_le_add_left (smul_le_smul_of_nonneg hb hr) _
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
hb : b < b'
hr : 0 < r
⊢ ↑(lineMap a b) r < ↑(lineMap a b') r
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
hb : b < b'
hr : 0 < r
⊢ (1 - r) • a + r • b < (1 - r) • a + r • b'
[PROOFSTEP]
exact add_lt_add_left (smul_lt_smul_of_pos hb hr) _
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a < a'
hb : b < b'
h₀ : 0 ≤ r
h₁ : r ≤ 1
⊢ ↑(lineMap a b) r < ↑(lineMap a' b') r
[PROOFSTEP]
rcases h₀.eq_or_lt with (rfl | h₀)
[GOAL]
case inl
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r' : k
ha : a < a'
hb : b < b'
h₀ : 0 ≤ 0
h₁ : 0 ≤ 1
⊢ ↑(lineMap a b) 0 < ↑(lineMap a' b') 0
[PROOFSTEP]
simpa
[GOAL]
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a < a'
hb : b < b'
h₀✝ : 0 ≤ r
h₁ : r ≤ 1
h₀ : 0 < r
⊢ ↑(lineMap a b) r < ↑(lineMap a' b') r
[PROOFSTEP]
exact (lineMap_mono_left ha.le h₁).trans_lt (lineMap_strict_mono_right hb h₀)
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
h : r < r'
⊢ ↑(lineMap a b) r < ↑(lineMap a b) r' ↔ a < b
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
h : r < r'
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
[PROOFSTEP]
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 (sub_pos.2 h)]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
h : 0 < r
⊢ a < ↑(lineMap a b) r ↔ ↑(lineMap a b) 0 < ↑(lineMap a b) r
[PROOFSTEP]
rw [lineMap_apply_zero]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
h : r < 1
⊢ ↑(lineMap a b) r < b ↔ ↑(lineMap a b) r < ↑(lineMap a b) 1
[PROOFSTEP]
rw [lineMap_apply_one]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < r'
⊢ ↑(lineMap a b) r ≤ ↑(lineMap a b) r' ↔ a ≤ b
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < r'
⊢ (1 - r) • a + r • b ≤ (1 - r') • a + r' • b ↔ a ≤ b
[PROOFSTEP]
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 (sub_pos.2 h)]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : 0 < r
⊢ a ≤ ↑(lineMap a b) r ↔ ↑(lineMap a b) 0 ≤ ↑(lineMap a b) r
[PROOFSTEP]
rw [lineMap_apply_zero]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < 1
⊢ ↑(lineMap a b) r ≤ b ↔ ↑(lineMap a b) r ≤ ↑(lineMap a b) 1
[PROOFSTEP]
rw [lineMap_apply_one]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (↑(lineMap a b) r) ≤ ↑(lineMap (f a) (f b)) r ↔ slope f a (↑(lineMap a b) r) ≤ slope f a b
[PROOFSTEP]
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, 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 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')]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
h : 0 < (1 - r) * (b - a)
⊢ f (↑(lineMap a b) r) ≤ ↑(lineMap (f a) (f b)) r ↔ slope f a b ≤ slope f (↑(lineMap a b) r) b
[PROOFSTEP]
rw [← lineMap_apply_one_sub, ← lineMap_apply_one_sub _ _ r]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
h : 0 < (1 - r) * (b - a)
⊢ f (↑(lineMap b a) (1 - r)) ≤ ↑(lineMap (f b) (f a)) (1 - r) ↔ slope f a b ≤ slope f (↑(lineMap b a) (1 - r)) b
[PROOFSTEP]
revert h
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
⊢ 0 < (1 - r) * (b - a) →
    (f (↑(lineMap b a) (1 - r)) ≤ ↑(lineMap (f b) (f a)) (1 - r) ↔ slope f a b ≤ slope f (↑(lineMap b a) (1 - r)) b)
[PROOFSTEP]
generalize 1 - r = r'
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r r' : k
⊢ 0 < r' * (b - a) → (f (↑(lineMap b a) r') ≤ ↑(lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f (↑(lineMap b a) r') b)
[PROOFSTEP]
clear! r
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r' : k
⊢ 0 < r' * (b - a) → (f (↑(lineMap b a) r') ≤ ↑(lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f (↑(lineMap b a) r') b)
[PROOFSTEP]
intro h
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f (↑(lineMap b a) r') ≤ ↑(lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f (↑(lineMap b a) r') b
[PROOFSTEP]
simp_rw [lineMap_apply, slope, vsub_eq_sub, vadd_eq_add, smul_eq_mul]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ 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))
[PROOFSTEP]
rw [sub_add_eq_sub_sub_swap, sub_self, zero_sub, neg_mul_eq_mul_neg, neg_sub, le_inv_smul_iff h, smul_smul,
  mul_inv_cancel_right₀, le_sub_comm, ← neg_sub (f b), smul_neg, neg_add_eq_sub]
[GOAL]
case h
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ b - a ≠ 0
[PROOFSTEP]
exact right_ne_zero_of_mul h.ne'
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ f (↑(lineMap a b) r) ≤ ↑(lineMap (f a) (f b)) r ↔ slope f a (↑(lineMap a b) r) ≤ slope f (↑(lineMap a b) r) b
[PROOFSTEP]
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₁]
