-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem image_le_of_liminf_slope_right_le_deriv_boundary {f : ℝ → ℝ} {a b : ℝ}
    (hf : ContinuousOn f (Icc a b)) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ContinuousOn B (Icc a b))
    (hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x)
    -- `bound` actually says `liminf (f z - f x) / (z - x) ≤ B' x`
    (bound : ∀ x ∈ Ico a b, ∀ r, B' x < r → ∃ᶠ z in 𝓝[>] x, slope f x z < r) :
    ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x

Proof state:
case bound
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x✝ : ℝ
hx : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
a✝¹ : x ∈ Ico a b
a✝ : f x = B x + r * (x - a)
⊢ B' x < B' x + r * 1

Tactic:
rw [mul_one]

Result:
case bound
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x✝ : ℝ
hx : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
a✝¹ : x ∈ Ico a b
a✝ : f x = B x + r * (x - a)
⊢ B' x < B' x + r

Proof state:
case bound
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x✝ : ℝ
hx : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
a✝¹ : x ∈ Ico a b
a✝ : f x = B x + r * (x - a)
⊢ B' x < B' x + r

Tactic:
exact (lt_add_iff_pos_right _).2 hr

Result:
no goals

Proof state:
case bound
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ∀ x ∈ Ico a b, f x = B x + r * (x - a) → B' x < B' x + r * 1

Tactic:
intro x _ _

Result:
case bound
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x✝ : ℝ
hx : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
a✝¹ : x ∈ Ico a b
a✝ : f x = B x + r * (x - a)
⊢ B' x < B' x + r * 1

Proof state:
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → f x ≤ B x

Tactic:
intro x hx

Result:
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ B x

Proof state:
case a
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ x ∈ Icc a b

Tactic:
exact hx

Result:
no goals

Proof state:
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ f x ≤ B x + r * (x - a)

Tactic:
apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound

Result:
case ha
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ f a ≤ B a + r * (a - a)

case hB
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ContinuousOn (fun x => B x + r * (x - a)) (Icc a b)

case hB'
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ∀ x ∈ Ico a b, HasDerivWithinAt (fun x => B x + r * (x - a)) (?m.17301 x) (Ici x) x

case bound
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ∀ x ∈ Ico a b, f x = B x + r * (x - a) → B' x < ?m.17301 x

case a
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ x ∈ Icc a b

f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ℝ → ℝ

Proof state:
case hB'
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt (fun x => B x + r * (x - a)) (?m.17301 x) (Ici x) x

Tactic:
exact (hB' x hx).add (((hasDerivWithinAt_id x (Ici x)).sub_const a).const_mul r)

Result:
no goals

Proof state:
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
this : ContinuousWithinAt (fun r => B x + r * (x - a)) (Ioi 0) 0
⊢ f x ≤ B x

Tactic:
convert continuousWithinAt_const.closure_le _ this (Hr x hx) using 1 <;> simp

Result:
no goals

Proof state:
case hB
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ContinuousOn (fun x => B x + r * (x - a)) (Icc a b)

Tactic:
exact hB.add (continuousOn_const.mul (continuousOn_id.sub continuousOn_const))

Result:
no goals