awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ∀ (x : ℝ), HasDerivAt B (B' x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → f x ≤ B x

Tactic:
image_le_of_liminf_slope_right_lt_deriv_boundary' hf hf' ha
    (fun x _ => (hB x).continuousAt.continuousWithinAt) (fun x _ => (hB x).hasDerivWithinAt) bound

Premises used: HasDerivAt.hasDerivWithinAt, ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, image_le_of_liminf_slope_right_lt_deriv_boundary'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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
ha₁ : f a ≤ B a + r * (a - a)
hB₁ : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ B x + r * (x - a)) (Icc a b)
hB'₁ : ∀ x ∈ Ico a b, HasDerivWithinAt (fun (x : ℝ) ↦ B x + r * (x - a)) (B' x + r * 1) (Ici x) x
bound₁ : ∀ x ∈ Ico a b, f x = B x + r * (x - a) → B' x < B' x + r * 1
a₁ : x ∈ Icc a b
apply : ℝ → ℝ
⊢ f x ≤ B x + r * (x - a)

Tactic:
apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound

Premises used: image_le_of_liminf_slope_right_lt_deriv_boundary'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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
ha₁ : f a ≤ B a + r * 0
ha₂ : f a ≤ B a + 0
ha₃ ha₄ ha₅ ha₆ : f a ≤ B a
⊢ f a ≤ B a + r * (a - a)

Tactic:
rwa [sub_self, mul_zero, add_zero]

Premises used: sub_self, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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 (Y := ℝ) (fun (x : ℝ) ↦ B x + r * (x - a)) (Icc a b)

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

Premises used: ContinuousOn.sub, continuousOn_const, ContinuousOn.add, continuousOn_id, ContinuousOn.mul
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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 (Y := ℝ) (fun (x : ℝ) ↦ B x + r * (x - a)) (Icc a b)

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

Premises used: ContinuousOn.sub, continuousOn_const, ContinuousOn.add, continuousOn_id, ContinuousOn.mul
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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_1 : ℝ
hx_1 : x_1 ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ B x + r * (x - a)) (B' x + r * 1) (Ici x) x

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

Premises used: Set.Ici, HasDerivWithinAt.sub_const, HasDerivWithinAt.add, HasDerivWithinAt.const_mul, hasDerivWithinAt_id
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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_1 : ℝ
hx_1 : x_1 ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ B x + r * (x - a)) (B' x + r * 1) (Ici x) x

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

Premises used: Set.Ici, HasDerivWithinAt.sub_const, HasDerivWithinAt.add, HasDerivWithinAt.const_mul, hasDerivWithinAt_id
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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_1 : ℝ
hx : x_1 ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
bound₁ : x ∈ Ico a b → f x = B x + r * (x - a) → B' x < B' x + r * 1
⊢ x ∈ Ico a b → f x = B x + r * (x - a) → B' x < B' x + r * 1

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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_1 : ℝ
hx : x_1 ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
h : x ∈ Ico a b
bound₁ : f x = B x + r * (x - a) → B' x < B' x + r * 1
⊢ f x = B x + r * (x - a) → B' x < B' x + r * 1

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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_1 : ℝ
hx : x_1 ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
h : x ∈ Ico a b
h_1 : f x = B x + r * (x - a)
bound₁ : B' x < B' x + r
⊢ B' x < B' x + r * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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_1 : ℝ
hx : x_1 ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
h : x ∈ Ico a b
h_1 : f x = B x + r * (x - a)
⊢ B' x < B' x + r

Tactic:
(lt_add_iff_pos_right _).2 hr

Premises used: Iff.mpr, lt_add_iff_pos_right
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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_1 : ℝ
hx : x_1 ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
h : x ∈ Ico a b
h_1 : f x = B x + r * (x - a)
⊢ B' x < B' x + r

Tactic:
exact (lt_add_iff_pos_right _).2 hr

Premises used: Iff.mpr, lt_add_iff_pos_right
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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:
hx
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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 ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)

Tactic:
have Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a) := fun x hx r hr => by
    apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound
    · rwa [sub_self, mul_zero, add_zero]
    · exact hB.add (continuousOn_const.mul (continuousOn_id.sub continuousOn_const))
    · intro x hx
      exact (hB' x hx).add (((hasDerivWithinAt_id x (Ici x)).sub_const a).const_mul r)
    · intro x _ _
      rw [mul_one]
      exact (lt_add_iff_pos_right _).2 hr
    exact hx
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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
⊢ ContinuousWithinAt (Y := ℝ) (fun (r : ℝ) ↦ B x + r * (x - a)) (Ioi 0) 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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
⊢ ContinuousWithinAt (Y := ℝ) (fun (r : ℝ) ↦ B x + r * (x - a)) (Ioi 0) 0

Tactic:
have : ContinuousWithinAt (fun r => B x + r * (x - a)) (Ioi 0) 0 := by fun_prop
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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 (Y := ℝ) (fun (r : ℝ) ↦ B x + r * (x - a)) (Ioi 0) 0
⊢ f x ≤ B x + 0 * (x - a)

Tactic:
continuousWithinAt_const.closure_le _ this (Hr x hx)

Premises used: ContinuousWithinAt.closure_le, continuousWithinAt_const
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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 (Y := ℝ) (fun (r : ℝ) ↦ B x + r * (x - a)) (Ioi 0) 0
h : B x = B x + 0 * (x - a)
convert! : Membership.mem (γ := Set ℝ) (closure (Ioi 0)) 0
⊢ f x ≤ B x

Tactic:
convert! continuousWithinAt_const.closure_le _ this (Hr x hx) using 1

Premises used: ContinuousWithinAt.closure_le, continuousWithinAt_const
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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 (Y := ℝ) (fun (r : ℝ) ↦ B x + r * (x - a)) (Ioi 0) 0
⊢ B x = B x + 0 * (x - a)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
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 (Y := ℝ) (fun (r : ℝ) ↦ B x + r * (x - a)) (Ioi 0) 0
⊢ Membership.mem (γ := Set ℝ) (closure (Ioi 0)) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
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, f x = B x → f' x < B' x
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → f x ≤ B x

Tactic:
image_le_of_liminf_slope_right_lt_deriv_boundary' hf
    (fun x hx _ hr => (hf' x hx).liminf_right_slope_le hr) ha hB hB' bound

Premises used: HasDerivWithinAt.liminf_right_slope_le, image_le_of_liminf_slope_right_lt_deriv_boundary'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ∀ (x : ℝ), HasDerivAt B (B' x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → f x ≤ B x

Tactic:
image_le_of_deriv_right_lt_deriv_boundary' hf hf' ha
    (fun x _ => (hB x).continuousAt.continuousWithinAt) (fun x _ => (hB x).hasDerivWithinAt) bound

Premises used: HasDerivAt.hasDerivWithinAt, ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, image_le_of_deriv_right_lt_deriv_boundary'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
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, f' x ≤ B' x
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → f x ≤ B x

Tactic:
image_le_of_liminf_slope_right_le_deriv_boundary hf ha hB hB' fun x hx _ hr =>
    (hf' x hx).liminf_right_slope_le (lt_of_le_of_lt (bound x hx) hr)

Premises used: HasDerivWithinAt.liminf_right_slope_le, lt_of_le_of_lt, image_le_of_liminf_slope_right_le_deriv_boundary
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
a b : ℝ
E : Type u_3
inst : NormedAddCommGroup E
f : ℝ → E
f' : ℝ → ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope (norm ∘ f) x z < r
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, ‖f x‖ = B x → f' x < B' x
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → ‖f x‖ ≤ B x

Tactic:
image_le_of_liminf_slope_right_lt_deriv_boundary' (continuous_norm.comp_continuousOn hf) hf' ha hB
    hB' bound

Premises used: Continuous.comp_continuousOn, image_le_of_liminf_slope_right_lt_deriv_boundary', continuous_norm
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
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, ‖f x‖ = B x → ‖f' x‖ < B' x
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → ‖f x‖ ≤ B x

Tactic:
image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary hf
    (fun x hx _ hr => (hf' x hx).liminf_right_slope_norm_le hr) ha hB hB' bound

Premises used: HasDerivWithinAt.liminf_right_slope_norm_le, image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
B B' : ℝ → ℝ
ha : ‖f a‖ ≤ B a
hB : ∀ (x : ℝ), HasDerivAt B (B' x) x
bound : ∀ x ∈ Ico a b, ‖f x‖ = B x → ‖f' x‖ < B' x
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → ‖f x‖ ≤ B x

Tactic:
image_norm_le_of_norm_deriv_right_lt_deriv_boundary' hf hf' ha
    (fun x _ => (hB x).continuousAt.continuousWithinAt) (fun x _ => (hB x).hasDerivWithinAt) bound

Premises used: HasDerivAt.hasDerivWithinAt, image_norm_le_of_norm_deriv_right_lt_deriv_boundary', ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
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, ‖f' x‖ ≤ B' x
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → ‖f x‖ ≤ B x

Tactic:
image_le_of_liminf_slope_right_le_deriv_boundary (continuous_norm.comp_continuousOn hf) ha hB hB'
    fun x hx _ hr => (hf' x hx).liminf_right_slope_norm_le ((bound x hx).trans_lt hr)

Premises used: HasDerivWithinAt.liminf_right_slope_norm_le, Continuous.comp_continuousOn, LE.le.trans_lt, continuous_norm, image_le_of_liminf_slope_right_le_deriv_boundary
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
B B' : ℝ → ℝ
ha : ‖f a‖ ≤ B a
hB : ∀ (x : ℝ), HasDerivAt B (B' x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ B' x
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → ‖f x‖ ≤ B x

Tactic:
image_norm_le_of_norm_deriv_right_le_deriv_boundary' hf hf' ha
    (fun x _ => (hB x).continuousAt.continuousWithinAt) (fun x _ => (hB x).hasDerivWithinAt) bound

Premises used: HasDerivAt.hasDerivWithinAt, image_norm_le_of_norm_deriv_right_le_deriv_boundary', ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : (x : ℝ) → E := fun (x : ℝ) ↦ f x - f a
⊢ ContinuousOn g (Icc a b)

Tactic:
have hg : ContinuousOn g (Icc a b) := hf.sub continuousOn_const
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : (x : ℝ) → E := fun (x : ℝ) ↦ f x - f a
hg : ContinuousOn g (Icc a b)
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt g (f' x) (Ici x) x

Tactic:
simp [g, hf' x hx]
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : (x : ℝ) → E := fun (x : ℝ) ↦ f x - f a
hg : ContinuousOn g (Icc a b)
⊢ ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x

Tactic:
have hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x := by
    intro x hx
    simp [g, hf' x hx]
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : (x : ℝ) → E := fun (x : ℝ) ↦ f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
B : (x : ℝ) → ℝ := fun (x : ℝ) ↦ C * (x - a)
x : ℝ
⊢ HasDerivAt B C x

Tactic:
simpa using (hasDerivAt_const x C).mul ((hasDerivAt_id x).sub (hasDerivAt_const x a))

Premises used: HasDerivAt.sub, hasDerivAt_const, hasDerivAt_id, HasDerivAt.mul
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : (x : ℝ) → E := fun (x : ℝ) ↦ f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
B : (x : ℝ) → ℝ := fun (x : ℝ) ↦ C * (x - a)
⊢ ∀ (x : ℝ), HasDerivAt B C x

Tactic:
have hB : ∀ x, HasDerivAt B C x := by
    intro x
    simpa using (hasDerivAt_const x C).mul ((hasDerivAt_id x).sub (hasDerivAt_const x a))
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : (x : ℝ) → E := fun (x : ℝ) ↦ f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
B : (x : ℝ) → ℝ := fun (x : ℝ) ↦ C * (x - a)
hB : ∀ (x : ℝ), HasDerivAt B C x
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → ‖g x‖ ≤ B x

Tactic:
image_norm_le_of_norm_deriv_right_le_deriv_boundary hg hg' _ hB bound

Premises used: image_norm_le_of_norm_deriv_right_le_deriv_boundary
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : (x : ℝ) → E := fun (x : ℝ) ↦ f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
B : (x : ℝ) → ℝ := fun (x : ℝ) ↦ C * (x - a)
hB : ∀ (x : ℝ), HasDerivAt B C x
convert! : ‖g a‖ ≤ B a
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Tactic:
convert! image_norm_le_of_norm_deriv_right_le_deriv_boundary hg hg' _ hB bound

Premises used: image_norm_le_of_norm_deriv_right_le_deriv_boundary
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : (x : ℝ) → E := fun (x : ℝ) ↦ f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
B : (x : ℝ) → ℝ := fun (x : ℝ) ↦ C * (x - a)
hB : ∀ (x : ℝ), HasDerivAt B C x
simp : ‖f a - f a‖ ≤ C * (a - a)
⊢ ‖g a‖ ≤ B a

Tactic:
simp only [g, B]
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : (x : ℝ) → E := fun (x : ℝ) ↦ f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
B : (x : ℝ) → ℝ := fun (x : ℝ) ↦ C * (x - a)
hB : ∀ (x : ℝ), HasDerivAt B C x
rw : norm.{u_1} (E := E) 0 ≤ C * (a - a)
rw₁ : 0 ≤ C * (a - a)
rw₂ : 0 ≤ C * 0
rw₃ rw₄ : LE.le (α := ℝ) 0 0
⊢ ‖f a - f a‖ ≤ C * (a - a)

Tactic:
rw [sub_self, norm_zero, sub_self, mul_zero]

Premises used: sub_self, norm_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Tactic:
norm_image_sub_le_of_norm_deriv_right_le_segment (fun x hx => (hf x hx).continuousWithinAt)
      (fun x hx => ?_) bound

Premises used: norm_image_sub_le_of_norm_deriv_right_le_segment, HasDerivWithinAt.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
norm_image_sub_le_of_norm_deriv_right_le_segment : ∀ (x : ℝ) (hx : x ∈ Ico a b), HasDerivWithinAt f (f' x) (Ici x) x
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Tactic:
refine
    norm_image_sub_le_of_norm_deriv_right_le_segment (fun x hx => (hf x hx).continuousWithinAt)
      (fun x hx => ?_) bound

Premises used: norm_image_sub_le_of_norm_deriv_right_le_segment, HasDerivWithinAt.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt f (f' x) (Ici x) x

Tactic:
(hf x <| Ico_subset_Icc_self hx).mono_of_mem_nhdsWithin (Icc_mem_nhdsGE_of_mem hx)

Premises used: Set.Ico_subset_Icc_self, Icc_mem_nhdsGE_of_mem, HasDerivWithinAt.mono_of_mem_nhdsWithin