-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
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)
rw : f (r • (b -ᵥ a) +ᵥ a) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
rw₁ : f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
rw₂ :
  f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b -ᵥ a) +ᵥ a) - a)⁻¹ • (f (r • (b -ᵥ a) +ᵥ a) -ᵥ f a) ≤ slope f a b
rw₃ :
  f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b -ᵥ a) +ᵥ a) - a)⁻¹ • (f (r • (b -ᵥ a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b -ᵥ f a)
rw₄ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b -ᵥ f a)
rw₅ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b - f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₆ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b - f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₇ :
  f (r • (b - a) + a) ≤ r • (f b - f a) +ᵥ f a ↔
    (r • (b - a) + a - a)⁻¹ • (f (r • (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₈ :
  f (r • (b - a) + a) ≤ r • (f b - f a) + f a ↔
    (r • (b - a) + a - a)⁻¹ • (f (r • (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₉ :
  f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔
    (r * (b - a) + a - a)⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₀ :
  f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔ (r * (b - a))⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₁ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₂ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • f (r * (b - a) + a) - (r * (b - a))⁻¹ • f a ≤ (b - a)⁻¹ • (f b - f a)
rw₁₃ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • f (r * (b - a) + a) - (r * (b - a))⁻¹ • f a ≤ (b - a)⁻¹ • f b - (b - a)⁻¹ • f a
rw₁₄ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • f (r * (b - a) + a) ≤ (b - a)⁻¹ • f b - (b - a)⁻¹ • f a + (r * (b - a))⁻¹ • f a
rw₁₅ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    ((b - a)⁻¹ * r⁻¹) • f (r * (b - a) + a) ≤ (b - a)⁻¹ • f b - (b - a)⁻¹ • f a + ((b - a)⁻¹ * r⁻¹) • f 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
have rw₁₆ : f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
  (b - a)⁻¹ • r⁻¹ • f (r * (b - a) + a) ≤ (b - a)⁻¹ • f b - (b - a)⁻¹ • f a + ((b - a)⁻¹ * r⁻¹) • f a
Tactic: 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_right, 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_of_pos 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')]