awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h_segment : [x₀ -[ℝ] x] ⊆ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
h₁ : ‖f x - f x₀‖ = ‖f x - f x₀ - (f x₀ - f x₀)‖
⊢ ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
have h₂ : ∀ x_1 ∈ [x₀ -[ℝ] x], HasFDerivWithinAt (fun (x : E) ↦ f x - f x₀) (f' x_1) [x₀ -[ℝ] x] x_1
Tactic: convert!
    (convex_segment x₀ x).norm_image_sub_le_of_norm_hasFDerivWithin_le (f := fun x ↦ f x - f x₀)
      (y := x) (x := x₀) (s := segment ℝ x₀ x) ?_ h
      (left_mem_segment ℝ x₀ x)
      (right_mem_segment ℝ x₀ x) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h_segment : [x₀ -[ℝ] x] ⊆ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ∀ x_1 ∈ [x₀ -[ℝ] x], HasFDerivWithinAt (fun (x : E) ↦ f x - f x₀) (f' x_1) [x₀ -[ℝ] x] x_1
have h₁ : ∀ x_1 ∈ [x₀ -[ℝ] x], HasFDerivWithinAt f (f' x_1) [x₀ -[ℝ] x] x_1
Tactic: simp only [hasFDerivWithinAt_sub_const_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : IsLittleO (F := ℝ) (𝓝[s] x₀) f' fun (x : ℝ) ↦ (x - x₀) ^ n
⊢ IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
have refine_2 : ∀ (h : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ ‖x - x₀‖ ^ (n + 1)),
  IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
Tactic: have h := hs.isLittleO_pow_succ hx₀s hff' ?_ (n := n)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : IsLittleO (F := ℝ) (𝓝[s] x₀) f' fun (x : ℝ) ↦ (x - x₀) ^ n
refine_2 :
  ∀ (h : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ ‖x - x₀‖ ^ (n + 1)),
    IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
⊢ IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
have refine_1 : IsLittleO.{0, u_1, 0} (E := ℝ →L[ℝ] E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ toSpanSingleton ℝ (f' x)) fun (x : ℝ) ↦
  ‖x - x₀‖ ^ n
Tactic: have h := hs.isLittleO_pow_succ hx₀s hff' ?_ (n := n)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : IsLittleO (F := ℝ) (𝓝[s] x₀) f' fun (x : ℝ) ↦ (x - x₀) ^ n
h : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ ‖x - x₀‖ ^ (n + 1)
⊢ IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
have refine_2 : ∀ (h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖ ^ (n + 1)‖) ⦃c : ℝ⦄,
  0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖(x - x₀) ^ (n + 1)‖
Tactic: rw [Asymptotics.isLittleO_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : IsLittleO (F := ℝ) (𝓝[s] x₀) f' fun (x : ℝ) ↦ (x - x₀) ^ n
⊢ IsLittleO.{0, u_1, 0} (E := ℝ →L[ℝ] E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ toSpanSingleton ℝ (f' x)) fun (x : ℝ) ↦
    ‖x - x₀‖ ^ n
have refine_1 : ∀ (hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖) ⦃c : ℝ⦄,
  0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, norm (E := ℝ →L[ℝ] E) (toSpanSingleton ℝ (f' x)) ≤ c * ‖‖x - x₀‖ ^ n‖
Tactic: rw [Asymptotics.isLittleO_iff] at hf' ⊢
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, norm (E := ℝ →L[ℝ] E) (toSpanSingleton ℝ (f' x)) ≤ c * ‖‖x - x₀‖ ^ n‖
have h : ∀ (c : ℝ) (hc : 0 < c) (x : ℝ),
  norm (E := ℝ →L[ℝ] E) (toSpanSingleton ℝ (f' x)) ≤ c * ‖‖x - x₀‖ ^ n‖ ↔ ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖
Tactic: convert! hf' using 4 with c hc x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x : 𝕜
hx : x ∈ s
⊢ Eq (α := 𝕜 →L[𝕜] G) (fderiv 𝕜 f x) (0 x)
have h : Eq.{u_4 + 1} (α := G) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] G) : (a : 𝕜) → G) 1 : G) ((0 x : (a : 𝕜) → G) 1 : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x y : 𝕜
hx : x ∈ s
hy : y ∈ s
a : 𝕜
ha : a ∈ s
⊢ Eq (α := 𝕜 →L[𝕜] G) (fderiv 𝕜 f a) (0 a)
have h : Eq.{u_4 + 1} (α := G) (((fderiv 𝕜 f a : 𝕜 →L[𝕜] G) : (a : 𝕜) → G) 1 : G) ((0 a : (a : 𝕜) → G) 1 : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
⊢ HasStrictFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' x) x
have rw : ∀ ⦃c : ℝ⦄,
  0 < c →
    ∀ᶠ (x_1 : G × G) in 𝓝 (x, x),
      ‖HSub.hSub (β := H) (f x_1.1 - f x_1.2) ((f' x : (a : G) → H) (x_1.1 - x_1.2) : H)‖ ≤ c * ‖x_1.1 - x_1.2‖
Tactic: rw [hasStrictFDerivAt_iff_isLittleO, isLittleO_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
⊢ ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : G × G) in 𝓝 (x, x),
        ‖HSub.hSub (β := H) (f x_1.1 - f x_1.2) ((f' x : (a : G) → H) (x_1.1 - x_1.2) : H)‖ ≤ c * ‖x_1.1 - x_1.2‖
have refine : ∀ (c : ℝ) (hc : 0 < c),
  ∃ ε > 0,
    ∀ y ∈ ball (x, x) ε, ‖HSub.hSub (β := H) (f y.1 - f y.2) ((f' x : (a : G) → H) (y.1 - y.2) : H)‖ ≤ c * ‖y.1 - y.2‖
Tactic: refine fun c hc => Metric.eventually_nhds_iff_ball.mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
⊢ ∃ ε > 0,
    ∀ y ∈ ball (x, x) ε, ‖HSub.hSub (β := H) (f y.1 - f y.2) ((f' x : (a : G) → H) (y.1 - y.2) : H)‖ ≤ c * ‖y.1 - y.2‖
have rcases : ∀ (ε : ℝ) (ε0 : ε > 0)
  (hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c),
  ∃ ε > 0,
    ∀ y ∈ ball (x, x) ε, ‖HSub.hSub (β := H) (f y.1 - f y.2) ((f' x : (a : G) → H) (y.1 - y.2) : H)‖ ≤ c * ‖y.1 - y.2‖
Tactic: rcases Metric.mem_nhds_iff.mp (inter_mem hder (hcont <| ball_mem_nhds _ hc)) with ⟨ε, ε0, hε⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
⊢ ∃ ε > 0,
    ∀ y ∈ ball (x, x) ε, ‖HSub.hSub (β := H) (f y.1 - f y.2) ((f' x : (a : G) → H) (y.1 - y.2) : H)‖ ≤ c * ‖y.1 - y.2‖
have refine : ∀ y ∈ ball (x, x) ε, ‖HSub.hSub (β := H) (f y.1 - f y.2) ((f' x : (a : G) → H) (y.1 - y.2) : H)‖ ≤ c * ‖y.1 - y.2‖
Tactic: refine ⟨ε, ε0, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : (a, b) ∈ ball (x, x) ε
⊢ ‖HSub.hSub (β := H) (f (a, b).1 - f (a, b).2) ((f' x : (a : G) → H) ((a, b).1 - (a, b).2) : H)‖ ≤
    c * ‖(a, b).1 - (a, b).2‖
have h₁ : a ∈ ball x ε ∧ b ∈ ball x ε
Tactic: rw [← ball_prod_same, prodMk_mem_set_prod_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
x' : G
H' : x' ∈ ball x ε
⊢ ‖f' x' - f' x‖ ≤ c
have rw : dist (f' x') (f' x) ≤ c
Tactic: rw [← dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
⊢ ‖HSub.hSub (β := H) (f (a, b).1 - f (a, b).2) ((f' x : (a : G) → H) ((a, b).1 - (a, b).2) : H)‖ ≤
    c * ‖(a, b).1 - (a, b).2‖
have hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c
Tactic: have hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c := fun x' H' => by
    rw [← dist_eq_norm]
    exact le_of_lt (hε H').2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
⊢ ‖HSub.hSub (β := H) (f (a, b).1 - f (a, b).2) ((f' x : (a : G) → H) ((a, b).1 - (a, b).2) : H)‖ ≤
    c * ‖(a, b).1 - (a, b).2‖
have refine : ∀ x_1 ∈ ball x ε, HasFDerivWithinAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' x_1) (ball x ε) x_1
Tactic: refine (convex_ball _ _).norm_image_sub_le_of_norm_hasFDerivWithin_le' ?_ hf' h.2 h.1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
⊢ Tendsto (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 (1 + c * (x - x)))
have apply : Tendsto (fun (y : ℝ) ↦ 1 + c * (y - x)) (𝓝 x) (𝓝 (1 + c * (x - x)))
Tactic: apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
⊢ Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
have this : Tendsto (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 (1 + c * (x - x)))
Tactic: have : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x))) := by
      apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
      exact ((tendsto_id.sub_const x).const_mul c).const_add 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
this : Tendsto (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 (1 + c * (x - x)))
⊢ Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
have this₁ : Tendsto (β := ℝ) (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 1)
Tactic: simp only [_root_.sub_self, add_zero, mul_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
this : Tendsto (β := ℝ) (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
have apply : ∀ᶠ (x_1 : ℝ) in 𝓝[≠] x, 1 + c * (x_1 - x) = (x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)
Tactic: apply Tendsto.congr' (Eventually.filter_mono hl _) this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
this : Tendsto (β := ℝ) (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 1)
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[≠] x, 1 + c * (x_1 - x) = (x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)
have h : ∀ (y : ℝ) (hy : Membership.mem (γ := Set ℝ) {x}ᶜ y),
  1 + c * (y - x) = (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)
Tactic: filter_upwards [self_mem_nhdsWithin] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
⊢ Tendsto (fun (y : ℝ) ↦ (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)) l (𝓝 a)
have L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
Tactic: have L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1) := by
    have : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x))) := by
      apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
      exact ((tendsto_id.sub_const x).const_mul c).const_add 1
    simp only [_root_.sub_self, add_zero, mul_zero] at this
    apply Tendsto.congr' (Eventually.filter_mono hl _) this
    filter_upwards [self_mem_nhdsWithin] with y hy
    field [sub_ne_zero.2 hy]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
⊢ Tendsto (fun (y : ℝ) ↦ (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)) l (𝓝 a)
have Z : Tendsto
  (fun (x_1 : ℝ) ↦
    ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
      ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
  l (𝓝 (a * 1))
Tactic: have Z := (hf.comp h').mul L
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 (a * 1))
⊢ Tendsto (fun (y : ℝ) ↦ (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)) l (𝓝 a)
have Z₁ : Tendsto
  (fun (x_1 : ℝ) ↦
    ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
      ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
  l (𝓝 a)
Tactic: rw [mul_one] at Z
Cleared hypotheses: Z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ Tendsto (fun (y : ℝ) ↦ (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)) l (𝓝 a)
have apply : l.EventuallyEq (β := ℝ)
  (fun (x_1 : ℝ) ↦
    ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
      ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
  fun (y : ℝ) ↦ (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)
Tactic: apply Tendsto.congr' _ Z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ l.EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    fun (y : ℝ) ↦ (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)
have this : ∀ᶠ (y : ℝ) in l, y + c * HPow.hPow (β := ℕ) (y - x) 2 ≠ x
Tactic: have : ∀ᶠ y in l, y + c * (y - x) ^ 2 ≠ x := by apply Tendsto.mono_right h' hl self_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 a)
this : ∀ᶠ (y : ℝ) in l, y + c * HPow.hPow (β := ℕ) (y - x) 2 ≠ x
⊢ l.EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    fun (y : ℝ) ↦ (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)
have h : ∀ (y : ℝ) (hy : y + c * HPow.hPow (β := ℕ) (y - x) 2 ≠ x),
  ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) y *
      ((y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) =
    (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)
Tactic: filter_upwards [this] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : StieltjesFunction ℝ
⊢ ∀ᵐ (x : ℝ), HasDerivAt (↑f : ℝ → ℝ) (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal x
have h : ∀ (x : ℝ)
  (hx :
    Tendsto
      (fun (a : Set ℝ) ↦
        HDiv.hDiv (α := ENNReal) (β := ENNReal) ((f.measure : (a : Set ℝ) → ENNReal) a : ENNReal)
          ((volume : (a : Set ℝ) → ENNReal) a : ENNReal))
      (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
      (𝓝 (rnDeriv (m := MeasureSpace.toMeasurableSpace) f.measure volume x)))
  (h'x : rnDeriv (m := Real.measurableSpace) f.measure volume x < ⊤) (h''x : ¬leftLim (↑f : ℝ → ℝ) x ≠ (↑f : ℝ → ℝ) x),
  HasDerivAt (↑f : ℝ → ℝ) (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal x
Tactic: filter_upwards [VitaliFamily.ae_tendsto_rnDeriv (vitaliFamily (volume : Measure ℝ) 1) f.measure,
    rnDeriv_lt_top f.measure volume, f.countable_leftLim_ne.ae_notMem volume] with x hx h'x h''x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : StieltjesFunction ℝ
x : ℝ
hx :
  Tendsto
    (fun (a : Set ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal) ((f.measure : (a : Set ℝ) → ENNReal) a : ENNReal)
        ((volume : (a : Set ℝ) → ENNReal) a : ENNReal))
    (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (m := MeasureSpace.toMeasurableSpace) f.measure volume x))
h'x : rnDeriv (m := Real.measurableSpace) f.measure volume x < ⊤
h''x : ¬leftLim (↑f : ℝ → ℝ) x ≠ (↑f : ℝ → ℝ) x
⊢ Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
have apply : (ENNReal.toReal ∘
    (fun (a : Set ℝ) ↦
        HDiv.hDiv (α := ENNReal) (β := ENNReal) ((f.measure : (a : Set ℝ) → ENNReal) a : ENNReal)
          ((volume : (a : Set ℝ) → ENNReal) a : ENNReal)) ∘
      fun (y : ℝ) ↦ Icc x y) =ᶠ[𝓝[>] x]
  fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
Tactic: apply Tendsto.congr' _
      ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_right x)))