awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Monotone
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)

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)
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
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)
⊢ HasDerivAt (↑f : ℝ → ℝ) (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal x

Tactic:
rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, ← nhdsLT_sup_nhdsGT, tendsto_sup]

Premises used: Filter.tendsto_sup, slope_fun_def_field, hasDerivAt_iff_tendsto_slope, nhdsLT_sup_nhdsGT
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
⊢ 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:
⟨L4, L1⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
⊢ 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:
exact ⟨L4, L1⟩
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
hf : Monotone f
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
⊢ ∀ᵐ (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

Premises used: Monotone.stieltjesFunction, Set.Countable.ae_notMem, Monotone.countable_not_continuousAt, MeasureTheory.MeasureSpace.volume, StieltjesFunction.ae_hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Monotone
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
⊢ leftLim f x = rightLim f x

Tactic:
rw [Classical.not_not, hf.continuousAt_iff_leftLim_eq_rightLim] at h'x

Premises used: Monotone.continuousAt_iff_leftLim_eq_rightLim, Classical.not_not
-- Module: Mathlib.Analysis.Calculus.Monotone
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
apply : rightLim f x ≤ f x
⊢ (↑hf.stieltjesFunction : ℝ → ℝ) x = f x

Tactic:
apply le_antisymm _ (hf.le_rightLim (le_refl _))

Premises used: le_refl, le_antisymm, Monotone.le_rightLim
-- Module: Mathlib.Analysis.Calculus.Monotone
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
rw : leftLim f x ≤ f x
⊢ rightLim f x ≤ f x

Tactic:
rw [← h'x]
-- Module: Mathlib.Analysis.Calculus.Monotone
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
⊢ leftLim f x ≤ f x

Tactic:
hf.leftLim_le (le_refl _)

Premises used: le_refl, Monotone.leftLim_le
-- Module: Mathlib.Analysis.Calculus.Monotone
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
⊢ leftLim f x ≤ f x

Tactic:
exact hf.leftLim_le (le_refl _)

Premises used: le_refl, Monotone.leftLim_le
-- Module: Mathlib.Analysis.Calculus.Monotone
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

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 _)
-- Module: Mathlib.Analysis.Calculus.Monotone
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
⊢ 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

Premises used: Filter.tendsto_sup, slope_fun_def_field, Eq.symm, hasDerivAt_iff_tendsto_slope, nhdsLT_sup_nhdsGT
-- Module: Mathlib.Analysis.Calculus.Monotone
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
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)
⊢ ¬¬ContinuousAt f x

Tactic:
rw [hasDerivAt_iff_tendsto_slope, (nhdsLT_sup_nhdsGT x).symm, tendsto_sup,
    slope_fun_def_field, A] at hx

Premises used: Filter.tendsto_sup, slope_fun_def_field, Eq.symm, hasDerivAt_iff_tendsto_slope, nhdsLT_sup_nhdsGT
-- Module: Mathlib.Analysis.Calculus.Monotone
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
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
⊢ (↑hf.stieltjesFunction : ℝ → ℝ) x = f x

Tactic:
rw [hasDerivAt_iff_tendsto_slope, (nhdsLT_sup_nhdsGT x).symm, tendsto_sup,
    slope_fun_def_field, A] at hx

Premises used: Filter.tendsto_sup, slope_fun_def_field, Eq.symm, hasDerivAt_iff_tendsto_slope, nhdsLT_sup_nhdsGT
-- Module: Mathlib.Analysis.Calculus.Monotone
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
apply : Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[>] x) (𝓝[>] 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)

Tactic:
apply tendsto_apply_add_mul_sq_div_sub (nhdsGT_le_nhdsNE x) hx.2

Premises used: nhdsGT_le_nhdsNE, And.right, tendsto_apply_add_mul_sq_div_sub
-- Module: Mathlib.Analysis.Calculus.Monotone
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)
h2 : ∀ᶠ (x_1 : ℝ) in 𝓝[>] x, x_1 + -1 * HPow.hPow (β := ℕ) (x_1 - x) 2 ∈ Ioi x
⊢ Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[>] x) (𝓝[>] x)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within

Premises used: tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Module: Mathlib.Analysis.Calculus.Monotone
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
apply : Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝 x) (𝓝 x)
⊢ Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[>] x) (𝓝 x)

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.Calculus.Monotone
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 + -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))
-- Module: Mathlib.Analysis.Calculus.Monotone
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
this : Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝 x) (𝓝 (x + -1 * HPow.hPow (β := ℕ) (x - x) 2))
⊢ Tendsto (fun (y : ℝ) ↦ y + -1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝 x) (𝓝 x)

Tactic:
simpa using this
-- Module: Mathlib.Analysis.Calculus.Monotone
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 < x + 1

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Monotone
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
h : ∀ a ∈ Ioo x (x + 1), a + -1 * HPow.hPow (β := ℕ) (a - x) 2 ∈ Ioi x
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] x, x_1 + -1 * HPow.hPow (β := ℕ) (x_1 - x) 2 ∈ Ioi x

Tactic:
filter_upwards [Ioo_mem_nhdsGT <| show x < x + 1 by simp]

Premises used: Ioo_mem_nhdsGT
-- Module: Mathlib.Analysis.Calculus.Monotone
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
nlinarith :
  y + -1 * HPow.hPow (β := ℕ) (y - x) 2 ≤ x →
    y + -1 * HPow.hPow (β := ℕ) (y - x) 2 - x + (0 - (x - y) * (y - (x + 1))) = 0
⊢ x < y + -1 * HPow.hPow (β := ℕ) (y - x) 2

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Calculus.Monotone
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)

Tactic:
have : Tendsto (fun y => (hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
        (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by
      apply tendsto_apply_add_mul_sq_div_sub (nhdsGT_le_nhdsNE x) hx.2
      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_nhdsGT <| show x < x + 1 by simp]
        rintro y ⟨hy : x < y, h'y : y < x + 1⟩
        rw [mem_Ioi]
        nlinarith
-- Module: Mathlib.Analysis.Calculus.Monotone
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
this :
  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)
hgf :
  ∀ᶠ (b : ℝ) in 𝓝[>] x,
    ((↑hf.stieltjesFunction : ℝ → ℝ) (b + -1 * HPow.hPow (β := ℕ) (b - x) 2) - f x) / (b - x) ≤ (f b - f x) / (b - x)
hfh : ∀ᶠ (b : ℝ) in 𝓝[>] x, (f b - f x) / (b - x) ≤ ((↑hf.stieltjesFunction : ℝ → ℝ) b - f x) / (b - x)
⊢ Tendsto (fun (y : ℝ) ↦ (f y - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) (StieltjesFunction.measure hf.stieltjesFunction) volume x).toReal)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' this hx.2

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le', And.right
-- Module: Mathlib.Analysis.Calculus.Monotone
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
this :
  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)
h :
  ∀ (y : ℝ) (hy : y ∈ Ioi x),
    ((↑hf.stieltjesFunction : ℝ → ℝ) (y + -1 * HPow.hPow (β := ℕ) (y - x) 2) - f x) / (y - x) ≤ (f y - f x) / (y - x)
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] x,
    ((↑hf.stieltjesFunction : ℝ → ℝ) (b + -1 * HPow.hPow (β := ℕ) (b - x) 2) - f x) / (b - x) ≤ (f b - f x) / (b - x)

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

Premises used: self_mem_nhdsWithin