-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem map_le_lineMap_iff_slope_le_slope_right (h : 0 < (1 - r) * (b - a)) :
    f c ≤ lineMap (f a) (f b) r ↔ slope f a b ≤ slope f c b

Proof state:
k : Type u_1
E : Type u_2
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)

Tactic:
intro h

Result:
k : Type u_1
E : Type u_2
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

Proof state:
k : Type u_1
E : Type u_2
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))

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]

Result:
case h
k : Type u_1
E : Type u_2
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

Proof state:
case h
k : Type u_1
E : Type u_2
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

Tactic:
exact right_ne_zero_of_mul h.ne'

Result:
no goals

Proof state:
k : Type u_1
E : Type u_2
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)

Tactic:
clear! r

Result:
k : Type u_1
E : Type u_2
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)

Proof state:
k : Type u_1
E : Type u_2
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

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

Result:
k : Type u_1
E : Type u_2
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))

Proof state:
k : Type u_1
E : Type u_2
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)

Tactic:
generalize 1 - r = r'

Result:
k : Type u_1
E : Type u_2
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)

Proof state:
k : Type u_1
E : Type u_2
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

Tactic:
revert h

Result:
k : Type u_1
E : Type u_2
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)

Proof state:
k : Type u_1
E : Type u_2
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

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

Result:
k : Type u_1
E : Type u_2
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