-- Mathlib/Analysis/ODE/Gronwall.lean
theorem le_gronwallBound_of_liminf_deriv_right_le {f f' : ℝ → ℝ} {δ K ε : ℝ} {a b : ℝ}
    (hf : ContinuousOn f (Icc a b))
    (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r → ∃ᶠ z in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r)
    (ha : f a ≤ δ) (bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε) :
    ∀ x ∈ Icc a b, f x ≤ gronwallBound δ K ε (x - a)

Proof state:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ f x ≤ gronwallBound δ K ε' (x - a)

Tactic:
apply image_le_of_liminf_slope_right_lt_deriv_boundary hf hf'

Result:
case ha
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ f a ≤ gronwallBound δ K ε' (a - a)

case hB
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ ∀ (x : ℝ), HasDerivAt (fun x => gronwallBound δ K ε' (x - a)) (?m.20314 x) x

case bound
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ ∀ x ∈ Ico a b, f x = gronwallBound δ K ε' (x - a) → f' x < ?m.20314 x

case a
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ x ∈ Icc a b

f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ ℝ → ℝ

Proof state:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ (fun ε' => gronwallBound δ K ε' (x - a)) ε

Tactic:
convert continuousWithinAt_const.closure_le _ _ (H x hx)

Result:
case convert_2
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ ε ∈ closure (Ioi ε)

case convert_3
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ ContinuousWithinAt (fun y => gronwallBound δ K y (x - a)) (Ioi ε) ε

Proof state:
case bound
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
x : ℝ
hx : x ∈ Ico a b
hfB : f x = gronwallBound δ K ε' (x - a)
⊢ f' x < K * f x + ε'

Tactic:
apply lt_of_le_of_lt (bound x hx)

Result:
case bound
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
x : ℝ
hx : x ∈ Ico a b
hfB : f x = gronwallBound δ K ε' (x - a)
⊢ K * f x + ε < K * f x + ε'