k : Type u_1
E : Type u_2
PE : Type ?u.171730
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
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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
rw [← lineMap_apply_one_sub, ← lineMap_apply_one_sub _ _ r]
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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)
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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
revert h
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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)
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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)
generalize 1 - r = r'
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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)
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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)
clear! r
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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)
intro h
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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))
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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
simp_rw [lineMap_apply, slope, vsub_eq_sub, vadd_eq_add, smul_eq_mul]
case h
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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))
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]
no goals
case h
k : Type u_1
E : Type u_2
PE : Type ?u.171730
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
exact right_ne_zero_of_mul h.ne'