no goals
k : Type u_1
E : Type u_2
PE : Type ?u.138707
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
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')]