awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
f 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, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
have inr : Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
Tactic: refine ⟨z, ?_, hz⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
f 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, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
have this₁ : slope f x z ≤ slope B x z
Tactic: have := (hfz.trans hzB).le
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
f 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, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this_1 : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
this : slope f x z ≤ slope B x z
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
have inr : ∀ (this : (f z - f x) / (z - x) ≤ slope B x z), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
Tactic: rwa [slope_def_field, slope_def_field, div_le_div_iff_of_pos_right (sub_pos.2 hz.1), hxB,
      sub_le_sub_iff_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
f 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, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this_1 : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
this : slope f x z ≤ slope B x z
inr : ∀ (this : (f z - f x) / (z - x) ≤ slope B x z), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
have inr₁ : ∀ (this : (f z - f x) / (z - x) ≤ (B z - B x) / (z - x)), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
Tactic: rwa [slope_def_field, slope_def_field, div_le_div_iff_of_pos_right (sub_pos.2 hz.1), hxB,
      sub_le_sub_iff_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
f 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, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this_1 : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
this : slope f x z ≤ slope B x z
inr : ∀ (this : (f z - f x) / (z - x) ≤ slope B x z), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
inr₁ : ∀ (this : (f z - f x) / (z - x) ≤ (B z - B x) / (z - x)), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
have inr₂ : ∀ (this : f z - f x ≤ B z - B x), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
Tactic: rwa [slope_def_field, slope_def_field, div_le_div_iff_of_pos_right (sub_pos.2 hz.1), hxB,
      sub_le_sub_iff_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
f 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, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this_1 : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
this : slope f x z ≤ slope B x z
inr : ∀ (this : (f z - f x) / (z - x) ≤ slope B x z), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
inr₁ : ∀ (this : (f z - f x) / (z - x) ≤ (B z - B x) / (z - x)), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
inr₂ : ∀ (this : f z - f x ≤ B z - B x), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
have inr₃ : ∀ (this : f z - B x ≤ B z - B x), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
Tactic: rwa [slope_def_field, slope_def_field, div_le_div_iff_of_pos_right (sub_pos.2 hz.1), hxB,
      sub_le_sub_iff_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
f 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, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this_1 : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
this : slope f x z ≤ slope B x z
inr : ∀ (this : (f z - f x) / (z - x) ≤ slope B x z), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
inr₁ : ∀ (this : (f z - f x) / (z - x) ≤ (B z - B x) / (z - x)), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
inr₂ : ∀ (this : f z - f x ≤ B z - B x), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
inr₃ : ∀ (this : f z - B x ≤ B z - B x), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
have inr₄ : ∀ (this : f z ≤ B z), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
Tactic: rwa [slope_def_field, slope_def_field, div_le_div_iff_of_pos_right (sub_pos.2 hz.1), hxB,
      sub_le_sub_iff_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
⊢ f x ≤ B x + r * (x - a)
have ha₁ : f a ≤ B a + r * (a - a)
Tactic: apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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)
⊢ f x ≤ B x + r * (x - a)
have hB₁ : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ B x + r * (x - a)) (Icc a b)
Tactic: apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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)
⊢ f x ≤ B x + r * (x - a)
have hB'₁ : ∀ x ∈ Ico a b, HasDerivWithinAt (fun (x : ℝ) ↦ B x + r * (x - a)) (B' x + r * 1) (Ici x) x
Tactic: apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
⊢ f x ≤ B x + r * (x - a)
have bound₁ : ∀ x ∈ Ico a b, f x = B x + r * (x - a) → B' x < B' x + r * 1
Tactic: apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
⊢ f a ≤ B a + r * (a - a)
have ha₁ : f a ≤ B a + r * 0
Tactic: rwa [sub_self, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
⊢ f a ≤ B a + r * (a - a)
have ha₂ : f a ≤ B a + 0
Tactic: rwa [sub_self, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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 * 1
have bound₁ : B' x < B' x + r
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
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 : ℝ⦄, x ∈ Icc a b → f x ≤ B x
have Hr : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
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
⊢ f x ≤ B x
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
have h : B x = B x + 0 * (x - a)
Tactic: convert! continuousWithinAt_const.closure_le _ this (Hr x hx) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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)
⊢ f x ≤ B x
have convert! : Membership.mem (γ := Set ℝ) (closure (Ioi 0)) 0
Tactic: convert! continuousWithinAt_const.closure_le _ this (Hr x hx) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
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
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
have hg : ContinuousOn g (Icc a b)
Tactic: have hg : ContinuousOn g (Icc a b) := hf.sub continuousOn_const
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
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 ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
have hg' : ∀ 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
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 ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
have hB : ∀ (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))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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 ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
have convert! : ‖g a‖ ≤ B a
Tactic: convert! image_norm_le_of_norm_deriv_right_le_deriv_boundary hg hg' _ hB bound
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
⊢ ‖f a - f a‖ ≤ C * (a - a)
have rw : norm.{u_1} (E := E) 0 ≤ C * (a - a)
Tactic: rw [sub_self, norm_zero, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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)
⊢ ‖f a - f a‖ ≤ C * (a - a)
have rw₁ : 0 ≤ C * (a - a)
Tactic: rw [sub_self, norm_zero, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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)
⊢ ‖f a - f a‖ ≤ C * (a - a)
have rw₂ : 0 ≤ C * 0
Tactic: rw [sub_self, norm_zero, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
⊢ ‖f a - f a‖ ≤ C * (a - a)
have rw₃ : LE.le (α := ℝ) 0 0
Tactic: rw [sub_self, norm_zero, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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)
have norm_image_sub_le_of_norm_deriv_right_le_segment : ∀ (x : ℝ) (hx : x ∈ Ico a b), HasDerivWithinAt f (f' x) (Ici x) x
Tactic: refine
    norm_image_sub_le_of_norm_deriv_right_le_segment (fun x hx => (hf x hx).continuousWithinAt)
      (fun x hx => ?_) bound
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
have refine : ∀ x ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) x) (Icc a b) x
Tactic: refine norm_image_sub_le_of_norm_deriv_le_segment' ?_ bound
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x
⊢ ∀ x ∈ Icc a b, f x = f a
have this : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a)
Tactic: have : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a) := fun x hx =>
    norm_image_sub_le_of_norm_deriv_right_le_segment hcont hderiv (fun _ _ => norm_zero.le) x hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0
⊢ ∀ x ∈ Icc a b, f x = f a
have H : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0
Tactic: have H : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0 := by
    simpa only [norm_le_zero_iff] using fun x hx => hderiv x hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a = g a
⊢ ∀ y ∈ Icc a b, f y = g y
have simp : ∀ (hi : f a - g a = 0), ∀ y ∈ Icc a b, f y - g y = 0
Tactic: simp only [← @sub_eq_zero _ _ (f _)] at hi ⊢
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
⊢ ∀ y ∈ Icc a b, f y = g y
have A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
Tactic: have A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y := fun y hy =>
    (fdiff y (mem_Icc_of_Ico hy)).hasDerivWithinAt.mono_of_mem_nhdsWithin
    (Icc_mem_nhdsGE_of_mem hy)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
⊢ ∀ y ∈ Icc a b, f y = g y
have B : ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y
Tactic: have B : ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y := fun y hy =>
    (gdiff y (mem_Icc_of_Ico hy)).hasDerivWithinAt.mono_of_mem_nhdsWithin
    (Icc_mem_nhdsGE_of_mem hy)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
g : (a : ℝ) → E := (⇑(AffineMap.lineMap x y) : (a : ℝ) → E)
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖
have segm : MapsTo g (Icc 0 1) s
Tactic: have segm : MapsTo g (Icc 0 1 : Set ℝ) s := hs.mapsTo_lineMap xs ys