awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (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)
have h : ∀ a ∈ Ioi x,
  (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)
      a =
    ((↑f : ℝ → ℝ) a - (↑f : ℝ → ℝ) x) / (a - x)
Tactic: filter_upwards [self_mem_nhdsWithin]
-- 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
y : ℝ
hxy : x < y
⊢ (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)
      y =
    ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
have h : (ENNReal.ofReal ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / ENNReal.ofReal (y - x)).toReal =
  ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
Tactic: simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc, Classical.not_not.1 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
y : ℝ
hxy : x < y
⊢ (ENNReal.ofReal ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / ENNReal.ofReal (y - x)).toReal =
    ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
have h : 0 ≤ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
Tactic: rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
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
⊢ HasDerivAt (↑f : ℝ → ℝ) (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal x
have L1 : Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
  (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
Tactic: have L1 :
    Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (rnDeriv f.measure volume x).toReal) := by
    apply Tendsto.congr' _
      ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_right x)))
    filter_upwards [self_mem_nhdsWithin]
    rintro y (hxy : x < y)
    simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc, Classical.not_not.1 h''x]
    rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal]
    exact div_nonneg (sub_nonneg.2 (f.mono hxy.le)) (sub_pos.2 hxy).le
-- 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ (leftLim (↑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 y x) =ᶠ[𝓝[<] x]
  fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
Tactic: apply Tendsto.congr' _
      ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_left 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
⊢ (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 y x) =ᶠ[𝓝[<] x]
    fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
have h : ∀ a ∈ Iio x,
  (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 y x)
      a =
    (leftLim (↑f : ℝ → ℝ) a - (↑f : ℝ → ℝ) x) / (a - x)
Tactic: filter_upwards [self_mem_nhdsWithin]
-- 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
y : ℝ
hxy : y < x
⊢ (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 y x)
      y =
    (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
have h : (ENNReal.ofReal ((↑f : ℝ → ℝ) x - leftLim (↑f : ℝ → ℝ) y) / ENNReal.ofReal (x - y)).toReal =
  (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
Tactic: simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc]
-- 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
y : ℝ
hxy : y < x
⊢ (ENNReal.ofReal ((↑f : ℝ → ℝ) x - leftLim (↑f : ℝ → ℝ) y) / ENNReal.ofReal (x - y)).toReal =
    (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
have h : 0 ≤ ((↑f : ℝ → ℝ) x - leftLim (↑f : ℝ → ℝ) y) / (x - y)
Tactic: rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal, ← neg_neg (y - x),
      div_neg, neg_div', neg_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
⊢ HasDerivAt (↑f : ℝ → ℝ) (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal x
have L2 : Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
  (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
Tactic: have L2 : Tendsto (fun y => (leftLim f y - f x) / (y - x)) (𝓝[<] x)
      (𝓝 (rnDeriv f.measure volume x).toReal) := by
    apply Tendsto.congr' _
      ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_left x)))
    filter_upwards [self_mem_nhdsWithin]
    rintro y (hxy : y < x)
    simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc]
    rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal, ← neg_neg (y - x),
      div_neg, neg_div', neg_sub, neg_sub]
    exact div_nonneg (sub_nonneg.2 (f.mono.leftLim_le hxy.le)) (sub_pos.2 hxy).le
-- 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L2 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) (y + 1 * HPow.hPow (β := ℕ) (y - x) 2) - (↑f : ℝ → ℝ) x) / (y - x))
    (𝓝[<] x) (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
have apply : Tendsto (fun (y : ℝ) ↦ y + 1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝[<] x)
Tactic: apply tendsto_apply_add_mul_sq_div_sub (nhdsLT_le_nhdsNE x) L2
-- 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L2 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ y + 1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝[<] x)
have h1 : Tendsto (fun (y : ℝ) ↦ y + 1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝 x)
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L2 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
h1 : Tendsto (fun (y : ℝ) ↦ y + 1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝 x)
⊢ Tendsto (fun (y : ℝ) ↦ y + 1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝[<] x)
have h2 : ∀ᶠ (x_1 : ℝ) in 𝓝[<] x, x_1 + 1 * HPow.hPow (β := ℕ) (x_1 - x) 2 ∈ Iio x
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L2 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ y + 1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝 x)
have apply : Tendsto (fun (y : ℝ) ↦ y + 1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝 x) (𝓝 x)
Tactic: apply Tendsto.mono_left _ nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L2 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ y + 1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝 x) (𝓝 x)
have this : Tendsto (fun (y : ℝ) ↦ y + 1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝 x) (𝓝 (x + 1 * HPow.hPow (β := ℕ) (x - x) 2))
Tactic: have : Tendsto (fun y : ℝ => y + ↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + ↑1 * (x - x) ^ 2)) :=
        tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul ↑1)
-- 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L2 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[<] x, x_1 + 1 * HPow.hPow (β := ℕ) (x_1 - x) 2 ∈ Iio x
have h : ∀ a ∈ Ioo (x - 1) x, a + 1 * HPow.hPow (β := ℕ) (a - x) 2 ∈ Iio x
Tactic: filter_upwards [Ioo_mem_nhdsLT <| show x - 1 < x by simp]
-- 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L2 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
y : ℝ
hy : x - 1 < y
h'y : y < x
⊢ y + 1 * HPow.hPow (β := ℕ) (y - x) 2 < x
have nlinarith : x ≤ y + 1 * HPow.hPow (β := ℕ) (y - x) 2 → x - (y + 1 * HPow.hPow (β := ℕ) (y - x) 2) + (0 - (x - 1 - y) * (y - x)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L2 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
⊢ HasDerivAt (↑f : ℝ → ℝ) (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal x
have L3 : Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) (y + 1 * HPow.hPow (β := ℕ) (y - x) 2) - (↑f : ℝ → ℝ) x) / (y - x))
  (𝓝[<] x) (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
Tactic: have L3 : Tendsto (fun y => (leftLim f (y + 1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
      (𝓝 (rnDeriv f.measure volume x).toReal) := by
    apply tendsto_apply_add_mul_sq_div_sub (nhdsLT_le_nhdsNE x) L2
    apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
    · apply Tendsto.mono_left _ nhdsWithin_le_nhds
      have : Tendsto (fun y : ℝ => y + ↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + ↑1 * (x - x) ^ 2)) :=
        tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul ↑1)
      simpa using this
    · filter_upwards [Ioo_mem_nhdsLT <| show x - 1 < x by simp]
      rintro y ⟨hy : x - 1 < y, h'y : y < x⟩
      rw [mem_Iio]
      nlinarith
-- 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L2 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L3 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) (y + 1 * HPow.hPow (β := ℕ) (y - x) 2) - (↑f : ℝ → ℝ) x) / (y - x))
    (𝓝[<] x) (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
⊢ Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
have hgf : ∀ᶠ (b : ℝ) in 𝓝[<] x,
  (leftLim (↑f : ℝ → ℝ) (b + 1 * HPow.hPow (β := ℕ) (b - x) 2) - (↑f : ℝ → ℝ) x) / (b - x) ≤
    ((↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le' L3 L2
-- 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
L1 :
  Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L2 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
L3 :
  Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) (y + 1 * HPow.hPow (β := ℕ) (y - x) 2) - (↑f : ℝ → ℝ) x) / (y - x))
    (𝓝[<] x) (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
hgf :
  ∀ᶠ (b : ℝ) in 𝓝[<] x,
    (leftLim (↑f : ℝ → ℝ) (b + 1 * HPow.hPow (β := ℕ) (b - x) 2) - (↑f : ℝ → ℝ) x) / (b - x) ≤
      ((↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x)
⊢ Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
have hfh : ∀ᶠ (b : ℝ) in 𝓝[<] x, ((↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x) ≤ (leftLim (↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le' L3 L2