awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
⊢ Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 (a * 1))

Tactic:
have Z := (hf.comp h').mul L
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 (a * 1))
⊢ Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 a)

Tactic:
rw [mul_one] at Z

Premises used: mul_one
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 a)
apply :
  l.EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    fun (y : ℝ) ↦ (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)
⊢ Tendsto (fun (y : ℝ) ↦ (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)) l (𝓝 a)

Tactic:
apply Tendsto.congr' _ Z

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ ∀ᶠ (y : ℝ) in l, y + c * HPow.hPow (β := ℕ) (y - x) 2 ≠ x

Tactic:
apply Tendsto.mono_right h' hl self_mem_nhdsWithin

Premises used: self_mem_nhdsWithin, Filter.Tendsto.mono_right
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ ∀ᶠ (y : ℝ) in l, y + c * HPow.hPow (β := ℕ) (y - x) 2 ≠ x

Tactic:
have : ∀ᶠ y in l, y + c * (y - x) ^ 2 ≠ x := by apply Tendsto.mono_right h' hl self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 a)
this : ∀ᶠ (y : ℝ) in l, y + c * HPow.hPow (β := ℕ) (y - x) 2 ≠ x
h :
  ∀ (y : ℝ) (hy : y + c * HPow.hPow (β := ℕ) (y - x) 2 ≠ x),
    ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) y *
        ((y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) =
      (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)
⊢ l.EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    fun (y : ℝ) ↦ (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)

Tactic:
filter_upwards [this] with y hy
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
L : Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun (x_1 : ℝ) ↦
      ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) x_1 *
        ((x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)))
    l (𝓝 a)
this : ∀ᶠ (y : ℝ) in l, y + c * HPow.hPow (β := ℕ) (y - x) 2 ≠ x
y : ℝ
hy : y + c * HPow.hPow (β := ℕ) (y - x) 2 ≠ x
⊢ ((fun (y : ℝ) ↦ (f y - d) / (y - x)) ∘ fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) y *
      ((y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) =
    (f (y + c * HPow.hPow (β := ℕ) (y - x) 2) - d) / (y - x)

Tactic:
simp [field, sub_ne_zero.2 hy]

Premises used: Iff.mpr, sub_ne_zero
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : StieltjesFunction ℝ
h :
  ∀ (x : ℝ)
    (hx :
      Tendsto
        (fun (a : Set ℝ) ↦
          HDiv.hDiv (α := ENNReal) (β := ENNReal) ((f.measure : (a : Set ℝ) → ENNReal) a : ENNReal)
            ((volume : (a : Set ℝ) → ENNReal) a : ENNReal))
        (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
        (𝓝 (rnDeriv (m := MeasureSpace.toMeasurableSpace) f.measure volume x)))
    (h'x : rnDeriv (m := Real.measurableSpace) f.measure volume x < ⊤)
    (h''x : ¬leftLim (↑f : ℝ → ℝ) x ≠ (↑f : ℝ → ℝ) x),
    HasDerivAt (↑f : ℝ → ℝ) (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal x
⊢ ∀ᵐ (x : ℝ), HasDerivAt (↑f : ℝ → ℝ) (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal x

Tactic:
filter_upwards [VitaliFamily.ae_tendsto_rnDeriv (vitaliFamily (volume : Measure ℝ) 1) f.measure,
    rnDeriv_lt_top f.measure volume, f.countable_leftLim_ne.ae_notMem volume] with x hx h'x h''x

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, Set.Countable.ae_notMem, IsUnifLocDoublingMeasure.vitaliFamily, StieltjesFunction.countable_leftLim_ne, StieltjesFunction.measure, MeasureTheory.MeasureSpace.volume, VitaliFamily.ae_tendsto_rnDeriv, OfNat.ofNat
-- 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
apply :
  (ENNReal.toReal ∘
      (fun (a : Set ℝ) ↦
          HDiv.hDiv (α := ENNReal) (β := ENNReal) ((f.measure : (a : Set ℝ) → ENNReal) a : ENNReal)
            ((volume : (a : Set ℝ) → ENNReal) a : ENNReal)) ∘
        fun (y : ℝ) ↦ Icc x y) =ᶠ[𝓝[>] x]
    fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
⊢ Tendsto (fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)

Tactic:
apply Tendsto.congr' _
      ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_right x)))

Premises used: ENNReal.tendsto_toReal, Filter.Tendsto.comp, Filter.Tendsto.congr', LT.lt.ne, Real.tendsto_Icc_vitaliFamily_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
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)
⊢ (ENNReal.toReal ∘
      (fun (a : Set ℝ) ↦
          HDiv.hDiv (α := ENNReal) (β := ENNReal) ((f.measure : (a : Set ℝ) → ENNReal) a : ENNReal)
            ((volume : (a : Set ℝ) → ENNReal) a : ENNReal)) ∘
        fun (y : ℝ) ↦ Icc x y) =ᶠ[𝓝[>] x]
    fun (y : ℝ) ↦ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)

Tactic:
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
y : ℝ
hxy : x < y
h :
  (ENNReal.ofReal ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / ENNReal.ofReal (y - x)).toReal =
    ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (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 x y)
      y =
    ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)

Tactic:
simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc, Classical.not_not.1 h''x]

Premises used: Classical.not_not, Real.volume_Icc, StieltjesFunction.measure_Icc, Iff.mp, Function.comp_apply
-- 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
y : ℝ
hxy : x < y
h : 0 ≤ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)
⊢ (ENNReal.ofReal ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / ENNReal.ofReal (y - x)).toReal =
    ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)

Tactic:
rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal]

Premises used: Iff.mpr, sub_pos, ENNReal.ofReal_div_of_pos, ENNReal.toReal_ofReal
-- 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
y : ℝ
hxy : x < y
⊢ 0 ≤ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)

Tactic:
div_nonneg (sub_nonneg.2 (f.mono hxy.le)) (sub_pos.2 hxy).le

Premises used: Iff.mpr, sub_pos, LT.lt.le, StieltjesFunction.mono, div_nonneg, sub_nonneg
-- 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
y : ℝ
hxy : x < y
⊢ 0 ≤ ((↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)

Tactic:
exact div_nonneg (sub_nonneg.2 (f.mono hxy.le)) (sub_pos.2 hxy).le

Premises used: Iff.mpr, sub_pos, LT.lt.le, StieltjesFunction.mono, div_nonneg, sub_nonneg
-- 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
⊢ 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
-- 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)
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)
⊢ Tendsto (fun (y : ℝ) ↦ (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv (m := Real.measurableSpace) f.measure volume x).toReal)

Tactic:
apply Tendsto.congr' _
      ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_left x)))

Premises used: ENNReal.tendsto_toReal, Real.tendsto_Icc_vitaliFamily_left, Filter.Tendsto.comp, Filter.Tendsto.congr', LT.lt.ne
-- 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)
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)
⊢ (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:
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)
y : ℝ
hxy : y < x
h :
  (ENNReal.ofReal ((↑f : ℝ → ℝ) x - leftLim (↑f : ℝ → ℝ) y) / ENNReal.ofReal (x - y)).toReal =
    (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (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)

Tactic:
simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc]

Premises used: Real.volume_Icc, StieltjesFunction.measure_Icc, Function.comp_apply
-- 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)
y : ℝ
hxy : y < x
h : 0 ≤ ((↑f : ℝ → ℝ) x - leftLim (↑f : ℝ → ℝ) y) / (x - y)
⊢ (ENNReal.ofReal ((↑f : ℝ → ℝ) x - leftLim (↑f : ℝ → ℝ) y) / ENNReal.ofReal (x - y)).toReal =
    (leftLim (↑f : ℝ → ℝ) y - (↑f : ℝ → ℝ) x) / (y - x)

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]

Premises used: neg_div', Iff.mpr, sub_pos, neg_sub, ENNReal.ofReal_div_of_pos, HSub.hSub, neg_neg, ENNReal.toReal_ofReal, div_neg
-- 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)
y : ℝ
hxy : y < x
⊢ 0 ≤ ((↑f : ℝ → ℝ) x - leftLim (↑f : ℝ → ℝ) y) / (x - y)

Tactic:
div_nonneg (sub_nonneg.2 (f.mono.leftLim_le hxy.le)) (sub_pos.2 hxy).le

Premises used: Iff.mpr, sub_pos, LT.lt.le, StieltjesFunction.mono, div_nonneg, Monotone.leftLim_le, sub_nonneg
-- 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)
y : ℝ
hxy : y < x
⊢ 0 ≤ ((↑f : ℝ → ℝ) x - leftLim (↑f : ℝ → ℝ) y) / (x - y)

Tactic:
exact div_nonneg (sub_nonneg.2 (f.mono.leftLim_le hxy.le)) (sub_pos.2 hxy).le

Premises used: Iff.mpr, sub_pos, LT.lt.le, StieltjesFunction.mono, div_nonneg, Monotone.leftLim_le, sub_nonneg
-- 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)
⊢ 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