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)
apply : Tendsto (fun (y : ℝ) ↦ y + 1 * HPow.hPow (β := ℕ) (y - x) 2) (𝓝[<] x) (𝓝[<] x)
⊢ 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:
apply tendsto_apply_add_mul_sq_div_sub (nhdsLT_le_nhdsNE x) L2

Premises used: nhdsLT_le_nhdsNE, tendsto_apply_add_mul_sq_div_sub
-- 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)
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 ∈ Iio 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 : 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)
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 : 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 + 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 : 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)
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 : 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 < x

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

Tactic:
filter_upwards [Ioo_mem_nhdsLT <| show x - 1 < x by simp]

Premises used: Ioo_mem_nhdsLT
-- 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)
y : ℝ
hy : x - 1 < y
h'y : y < x
nlinarith :
  x ≤ y + 1 * HPow.hPow (β := ℕ) (y - x) 2 →
    x - (y + 1 * HPow.hPow (β := ℕ) (y - x) 2) + (0 - (x - 1 - y) * (y - x)) = 0
⊢ y + 1 * HPow.hPow (β := ℕ) (y - x) 2 < x

Tactic:
nlinarith
-- 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)
⊢ 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
-- 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)
hgf :
  ∀ᶠ (b : ℝ) in 𝓝[<] x,
    (leftLim (↑f : ℝ → ℝ) (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) ≤ (leftLim (↑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)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' L3 L2

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le'
-- 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)
h :
  ∀ a ∈ Iio x,
    (leftLim (↑f : ℝ → ℝ) (a + 1 * HPow.hPow (β := ℕ) (a - x) 2) - (↑f : ℝ → ℝ) x) / (a - x) ≤
      ((↑f : ℝ → ℝ) a - (↑f : ℝ → ℝ) x) / (a - x)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x,
    (leftLim (↑f : ℝ → ℝ) (b + 1 * HPow.hPow (β := ℕ) (b - x) 2) - (↑f : ℝ → ℝ) x) / (b - x) ≤
      ((↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x)

Tactic:
filter_upwards [self_mem_nhdsWithin]

Premises used: self_mem_nhdsWithin
-- 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)
y : ℝ
hy : y < x
linarith : 0 < y - x → y - x + (0 - (y - x)) = 0
⊢ y - x ≤ 0

Tactic:
linarith
-- 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)
y : ℝ
hy : y < x
h : (↑f : ℝ → ℝ) y ≤ leftLim (↑f : ℝ → ℝ) (y + 1 * HPow.hPow (β := ℕ) (y - x) 2)
⊢ (leftLim (↑f : ℝ → ℝ) (y + 1 * HPow.hPow (β := ℕ) (y - x) 2) - (↑f : ℝ → ℝ) x) / (y - x) ≤
    ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)

Tactic:
refine div_le_div_of_nonpos_of_le (by linarith) ((sub_le_sub_iff_right _).2 ?_)

Premises used: div_le_div_of_nonpos_of_le, Iff.mpr, sub_le_sub_iff_right
-- 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)
y : ℝ
hy : y < x
h : y < y + 1 * HPow.hPow (β := ℕ) (y - x) 2
⊢ (↑f : ℝ → ℝ) y ≤ leftLim (↑f : ℝ → ℝ) (y + 1 * HPow.hPow (β := ℕ) (y - x) 2)

Tactic:
apply f.mono.le_leftLim

Premises used: StieltjesFunction.mono, Monotone.le_leftLim
-- 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)
y : ℝ
hy : y < x
⊢ 0 < HPow.hPow (β := ℕ) (x - y) 2

Tactic:
have : ↑0 < (x - y) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
-- 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)
y : ℝ
hy : y < x
this : 0 < HPow.hPow (β := ℕ) (x - y) 2
linarith :
  y + 1 * HPow.hPow (β := ℕ) (y - x) 2 ≤ y →
    0 - HPow.hPow (β := ℕ) (x - y) 2 + (y + 1 * HPow.hPow (β := ℕ) (y - x) 2 - y) = 0
⊢ y < y + 1 * HPow.hPow (β := ℕ) (y - x) 2

Tactic:
linarith
-- 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)
h : ∀ a ∈ Iio x, ((↑f : ℝ → ℝ) a - (↑f : ℝ → ℝ) x) / (a - x) ≤ (leftLim (↑f : ℝ → ℝ) a - (↑f : ℝ → ℝ) x) / (a - x)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x,
    ((↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x) ≤ (leftLim (↑f : ℝ → ℝ) b - (↑f : ℝ → ℝ) x) / (b - x)

Tactic:
filter_upwards [self_mem_nhdsWithin]

Premises used: self_mem_nhdsWithin
-- 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)
y : ℝ
hy : y < x
h : leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x ≤ (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x
⊢ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x) ≤ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)

Tactic:
refine div_le_div_of_nonpos_of_le (by linarith) ?_

Premises used: div_le_div_of_nonpos_of_le
-- 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)
y : ℝ
hy : y < x
⊢ leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x ≤ (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x

Tactic:
simpa only [sub_le_sub_iff_right] using f.mono.leftLim_le (le_refl y)

Premises used: le_refl, sub_le_sub_iff_right, StieltjesFunction.mono, Monotone.leftLim_le