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
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)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x,
    (leftLim (↑f : ℝ → ℝ) (b + 1 * HPow.hPow (β := ℕ) (b - x) 2) - (↑f : ℝ → ℝ) x) / (b - x) ≤
      ((↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x)
have h : ∀ a ∈ Iio x,
  (leftLim (↑f : ℝ → ℝ) (a + 1 * HPow.hPow (β := ℕ) (a - x) 2) - (↑f : ℝ → ℝ) x) / (a - x) ≤
    ((↑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)
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)
y : ℝ
hy : y < x
⊢ y - x ≤ 0
have linarith : 0 < y - x → y - x + (0 - (y - x)) = 0
Tactic: linarith
-- 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)
y : ℝ
hy : y < x
⊢ (leftLim (↑f : ℝ → ℝ) (y + 1 * HPow.hPow (β := ℕ) (y - x) 2) - (↑f : ℝ → ℝ) x) / (y - x) ≤
    ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
have h : (↑f : ℝ → ℝ) y ≤ leftLim (↑f : ℝ → ℝ) (y + 1 * HPow.hPow (β := ℕ) (y - x) 2)
Tactic: refine div_le_div_of_nonpos_of_le (by linarith) ((sub_le_sub_iff_right _).2 ?_)
-- 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)
y : ℝ
hy : y < x
⊢ (↑f : ℝ → ℝ) y ≤ leftLim (↑f : ℝ → ℝ) (y + 1 * HPow.hPow (β := ℕ) (y - x) 2)
have h : y < y + 1 * HPow.hPow (β := ℕ) (y - x) 2
Tactic: apply f.mono.le_leftLim
-- 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)
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)
y : ℝ
hy : y < x
⊢ y < y + 1 * HPow.hPow (β := ℕ) (y - x) 2
have this : 0 < HPow.hPow (β := ℕ) (x - y) 2
Tactic: have : ↑0 < (x - y) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
-- 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)
y : ℝ
hy : y < x
this : 0 < HPow.hPow (β := ℕ) (x - y) 2
⊢ y < y + 1 * HPow.hPow (β := ℕ) (y - x) 2
have linarith : y + 1 * HPow.hPow (β := ℕ) (y - x) 2 ≤ y →
  0 - HPow.hPow (β := ℕ) (x - y) 2 + (y + 1 * HPow.hPow (β := ℕ) (y - x) 2 - y) = 0
Tactic: linarith
-- 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)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x,
    ((↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x) ≤ (leftLim (↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x)
have h : ∀ a ∈ Iio x, ((↑f : ℝ → ℝ) a - (↑f : ℝ → ℝ) x) / (a - x) ≤ (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)
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)
y : ℝ
hy : y < x
⊢ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x) ≤ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
have h : leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x ≤ (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x
Tactic: refine div_le_div_of_nonpos_of_le (by linarith) ?_
-- 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)
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)
⊢ HasDerivAt (↑f : ℝ → ℝ) (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal x
have L4 : Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
  (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
Tactic: have L4 :
    Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[<] x) (𝓝 (rnDeriv f.measure volume x).toReal) := by
    apply tendsto_of_tendsto_of_tendsto_of_le_of_le' L3 L2
    · filter_upwards [self_mem_nhdsWithin]
      rintro y (hy : y < x)
      refine div_le_div_of_nonpos_of_le (by linarith) ((sub_le_sub_iff_right _).2 ?_)
      apply f.mono.le_leftLim
      have : ↑0 < (x - y) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
      linarith
    · filter_upwards [self_mem_nhdsWithin]
      rintro y (hy : y < x)
      refine div_le_div_of_nonpos_of_le (by linarith) ?_
      simpa only [sub_le_sub_iff_right] using f.mono.leftLim_le (le_refl y)
-- 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)
L4 :
  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 h : Tendsto (fun (b : ℝ) ↦ ((↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal) ∧
  Tendsto (fun (b : ℝ) ↦ ((↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)
Tactic: rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, ← nhdsLT_sup_nhdsGT, tendsto_sup]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
⊢ ∀ᵐ (x : ℝ),
    HasDerivAt f (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal
      x
have h : ∀ (x : ℝ)
  (hx :
    HasDerivAt (↑hf.stieltjesFunction : ℝ → ℝ)
      (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x)
  (h'x : ¬¬ContinuousAt f x),
  HasDerivAt f (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x
Tactic: filter_upwards [hf.stieltjesFunction.ae_hasDerivAt,
    hf.countable_not_continuousAt.ae_notMem volume] with x hx h'x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt (↑hf.stieltjesFunction : ℝ → ℝ)
    (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x
h'x : ¬¬ContinuousAt f x
⊢ (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
have h'x₁ : leftLim f x = rightLim f x
Tactic: rw [Classical.not_not, hf.continuousAt_iff_leftLim_eq_rightLim] at h'x
Cleared hypotheses: h'x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt (↑hf.stieltjesFunction : ℝ → ℝ)
    (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x
h'x : leftLim f x = rightLim f x
⊢ (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
have apply : rightLim f x ≤ f x
Tactic: apply le_antisymm _ (hf.le_rightLim (le_refl _))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt (↑hf.stieltjesFunction : ℝ → ℝ)
    (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x
h'x : leftLim f x = rightLim f x
⊢ rightLim f x ≤ f x
have rw : leftLim f x ≤ f x
Tactic: rw [← h'x]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt (↑hf.stieltjesFunction : ℝ → ℝ)
    (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x
h'x : ¬¬ContinuousAt f x
⊢ HasDerivAt f (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x
have A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
Tactic: have A : hf.stieltjesFunction x = f x := by
    rw [Classical.not_not, hf.continuousAt_iff_leftLim_eq_rightLim] at h'x
    apply le_antisymm _ (hf.le_rightLim (le_refl _))
    rw [← h'x]
    exact hf.leftLim_le (le_refl _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (hypothesis)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt (↑hf.stieltjesFunction : ℝ → ℝ)
    (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
⊢ HasDerivAt f (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal x
have hx₁ : Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
Tactic: rw [hasDerivAt_iff_tendsto_slope, (nhdsLT_sup_nhdsGT x).symm, tendsto_sup,
    slope_fun_def_field, A] at hx
Cleared hypotheses: hx, h'x, A
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
⊢ Tendsto (fun (y : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x))
    (𝓝[>] x) (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) 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 (nhdsGT_le_nhdsNE x) hx.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
⊢ 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 : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
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 ∈ Ioi x
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
⊢ 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 : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
⊢ 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 : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] x, x_1 + -1 * HPow.hPow (β := ℕ) (x_1 - x) 2 ∈ Ioi x
have h : ∀ a ∈ Ioo x (x + 1), a + -1 * HPow.hPow (β := ℕ) (a - x) 2 ∈ Ioi x
Tactic: filter_upwards [Ioo_mem_nhdsGT <| show x < x + 1 by simp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Monotone (goal)
Goal:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal) ∧
    Tendsto (fun (b : ℝ) ↦ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : (↑hf.stieltjesFunction : ℝ → ℝ) x = f x
y : ℝ
hy : x < y
h'y : y < x + 1
⊢ x < y + -1 * HPow.hPow (β := ℕ) (y - x) 2
have nlinarith : y + -1 * HPow.hPow (β := ℕ) (y - x) 2 ≤ x →
  y + -1 * HPow.hPow (β := ℕ) (y - x) 2 - x + (0 - (x - y) * (y - (x + 1))) = 0
Tactic: nlinarith