-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem outer_Ioc (a b : ℝ) : f.outer (Ioc a b) = ofReal (f b - f a)

Proof state:
case intro.intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε

Tactic:
have : ∀ i, ∃ p : ℝ × ℝ, s i ⊆ Ioo p.1 p.2 ∧
    (ofReal (f p.2 - f p.1) : ℝ≥0∞) < f.length (s i) + ε' i := by
  intro i
  have hl :=
    ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_ne_zero.2 (ε'0 i).ne')
  conv at hl =>
    lhs
    rw [length]
  simp only [iInf_lt_iff, exists_prop] at hl
  rcases hl with ⟨p, q', spq, hq'⟩
  have : ContinuousWithinAt (fun r => ofReal (f r - f p)) (Ioi q') q' := by
    apply ENNReal.continuous_ofReal.continuousAt.comp_continuousWithinAt
    refine ContinuousWithinAt.sub ?_ continuousWithinAt_const
    exact (f.right_continuous q').mono Ioi_subset_Ici_self
  rcases (((tendsto_order.1 this).2 _ hq').and self_mem_nhdsWithin).exists with ⟨q, hq, q'q⟩
  exact ⟨⟨p, q⟩, spq.trans (Ioc_subset_Ioo_right q'q), hq⟩

Result:
case intro.intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : ∀ (i : ℕ), ∃ p, s i ⊆ Ioo p.1 p.2 ∧ ofReal (↑f p.2 - ↑f p.1) < f.length (s i) + ↑(ε' i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε

Proof state:
case intro.intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
g : ℕ → ℝ × ℝ
hg : ∀ (i : ℕ), s i ⊆ Ioo (g i).1 (g i).2 ∧ ofReal (↑f (g i).2 - ↑f (g i).1) < f.length (s i) + ↑(ε' i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε

Tactic:
have I_subset : Icc a' b ⊆ ⋃ i, Ioo (g i).1 (g i).2 :=
  calc
    Icc a' b ⊆ Ioc a b := fun x hx => ⟨aa'.trans_le hx.1, hx.2⟩
    _ ⊆ ⋃ i, s i := hs
    _ ⊆ ⋃ i, Ioo (g i).1 (g i).2 := iUnion_mono fun i => (hg i).1

Result:
case intro.intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
g : ℕ → ℝ × ℝ
hg : ∀ (i : ℕ), s i ⊆ Ioo (g i).1 (g i).2 ∧ ofReal (↑f (g i).2 - ↑f (g i).1) < f.length (s i) + ↑(ε' i)
I_subset : Icc a' b ⊆ ⋃ i, Ioo (g i).1 (g i).2
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε

Proof state:
case intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
p q' : ℝ
spq : s i ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
this : ContinuousWithinAt (fun r => ofReal (↑f r - ↑f p)) (Ioi q') q'
⊢ ∃ p, s i ⊆ Ioo p.1 p.2 ∧ ofReal (↑f p.2 - ↑f p.1) < f.length (s i) + ↑(ε' i)

Tactic:
rcases (((tendsto_order.1 this).2 _ hq').and self_mem_nhdsWithin).exists with ⟨q, hq, q'q⟩

Result:
case intro.intro.intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
p q' : ℝ
spq : s i ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
this : ContinuousWithinAt (fun r => ofReal (↑f r - ↑f p)) (Ioi q') q'
q : ℝ
hq : ofReal (↑f q - ↑f p) < f.length (s i) + ↑(ε' i)
q'q : q' < q
⊢ ∃ p, s i ⊆ Ioo p.1 p.2 ∧ ofReal (↑f p.2 - ↑f p.1) < f.length (s i) + ↑(ε' i)

Proof state:
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
g : ℕ → ℝ × ℝ
hg : ∀ (i : ℕ), s i ⊆ Ioo (g i).1 (g i).2 ∧ ofReal (↑f (g i).2 - ↑f (g i).1) < f.length (s i) + ↑(ε' i)
I_subset : Icc a' b ⊆ ⋃ i, Ioo (g i).1 (g i).2
⊢ ∑' (i : ℕ), f.length (s i) + ↑δ + ↑δ = ∑' (i : ℕ), f.length (s i) + ↑ε

Tactic:
simp [δ, add_assoc, ENNReal.add_halves]

Result:
no goals

Proof state:
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
A : ContinuousWithinAt (fun r => ↑f r - ↑f a) (Ioi a) a
⊢ ↑f a - ↑f a < ↑δ

Tactic:
rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]

Result:
no goals

Proof state:
f : StieltjesFunction
a b : ℝ
⊢ f.outer (Ioc a b) = ofReal (↑f b - ↑f a)

Tactic:
refine
  le_antisymm
    (by
      rw [← f.length_Ioc]
      apply outer_le_length)
    (le_iInf₂ fun s hs => ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_)

Result:
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε

Proof state:
case intro.intro.intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
p q' : ℝ
spq : s i ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
this : ContinuousWithinAt (fun r => ofReal (↑f r - ↑f p)) (Ioi q') q'
q : ℝ
hq : ofReal (↑f q - ↑f p) < f.length (s i) + ↑(ε' i)
q'q : q' < q
⊢ ∃ p, s i ⊆ Ioo p.1 p.2 ∧ ofReal (↑f p.2 - ↑f p.1) < f.length (s i) + ↑(ε' i)

Tactic:
exact ⟨⟨p, q⟩, spq.trans (Ioc_subset_Ioo_right q'q), hq⟩

Result:
no goals

Proof state:
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
p q' : ℝ
spq : s i ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
⊢ ContinuousWithinAt (fun r => ↑f r - ↑f p) (Ioi q') q'

Tactic:
refine ContinuousWithinAt.sub ?_ continuousWithinAt_const

Result:
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
p q' : ℝ
spq : s i ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
⊢ ContinuousWithinAt (↑f) (Ioi q') q'