-- 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
L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x

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

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)
⊢ HasDerivAt (↑f) (f.measure.rnDeriv 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.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]

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
⊢ 0 ≤ (↑f y - ↑f x) / (y - x)

Proof state:
case h.intro
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)
y : ℝ
hy : x - 1 < y
h'y : y < x
⊢ y + 1 * (y - x) ^ 2 ∈ Iio x

Tactic:
rw [mem_Iio]

Result:
case h.intro
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)
y : ℝ
hy : x - 1 < y
h'y : y < x
⊢ y + 1 * (y - x) ^ 2 < 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)
⊢ ∀ a ∈ Iio x, (leftLim (↑f) (a + 1 * (a - x) ^ 2) - ↑f x) / (a - x) ≤ (↑f a - ↑f x) / (a - x)

Tactic:
rintro y (hy : y < 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
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
⊢ (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x) ≤ (↑f y - ↑f x) / (y - 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
⊢ (leftLim (↑f) (y + 1 * (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 ?_)

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)
y : ℝ
hy : y < x
⊢ ↑f y ≤ leftLim (↑f) (y + 1 * (y - x) ^ 2)

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
⊢ (↑f y - ↑f x) / (y - x) ≤ (leftLim (↑f) y - ↑f x) / (y - x)

Tactic:
refine div_le_div_of_nonpos_of_le (by linarith) ?_

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