-- Mathlib/Analysis/Calculus/Monotone.lean
theorem StieltjesFunction.ae_hasDerivAt (f : StieltjesFunction) :
    ∀ᵐ x, HasDerivAt f (rnDeriv f.measure volume x).toReal x

Proof state:
case h
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
y : ℝ
hxy : x < y
⊢ (ENNReal.toReal ∘ (fun a => f.measure a / volume a) ∘ 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]

Result:
case h
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
y : ℝ
hxy : x < y
⊢ (ENNReal.ofReal (↑f y - ↑f x) / ENNReal.ofReal (y - x)).toReal = (↑f y - ↑f x) / (y - x)

Proof state:
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ Tendsto (fun y => y + 1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)

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)

Result:
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
this : Tendsto (fun y => y + 1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + 1 * (x - x) ^ 2))
⊢ Tendsto (fun y => y + 1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)

Proof state:
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ Tendsto (fun y => (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)

Tactic:
apply tendsto_apply_add_mul_sq_div_sub (nhdsLT_le_nhdsNE x) L2

Result:
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ Tendsto (fun y => y + 1 * (y - x) ^ 2) (𝓝[<] x) (𝓝[<] x)

Proof state:
case hfh
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x, (↑f b - ↑f x) / (b - x) ≤ (leftLim (↑f) b - ↑f x) / (b - x)

Tactic:
filter_upwards [self_mem_nhdsWithin]

Result:
case h
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ ∀ a ∈ Iio x, (↑f a - ↑f x) / (a - x) ≤ (leftLim (↑f) a - ↑f x) / (a - x)

Proof state:
case h1
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ Tendsto (fun y => y + 1 * (y - x) ^ 2) (𝓝[<] x) (𝓝 x)

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Result:
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ Tendsto (fun y => y + 1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)

Proof state:
case h
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)
y : ℝ
hy : y < x
this : 0 < (x - y) ^ 2
⊢ y < y + 1 * (y - x) ^ 2

Tactic:
linarith

Result:
no goals

Proof state:
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
⊢ (ENNReal.toReal ∘ (fun a => f.measure a / volume a) ∘ fun y => Icc x y) =ᶠ[𝓝[>] x] fun y => (↑f y - ↑f x) / (y - x)

Tactic:
filter_upwards [self_mem_nhdsWithin]

Result:
case h
f : StieltjesFunction
x : ℝ
hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
⊢ ∀ a ∈ Ioi x, (ENNReal.toReal ∘ (fun a => f.measure a / volume a) ∘ fun y => Icc x y) a = (↑f a - ↑f x) / (a - x)