-- 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'
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) + ↑ε

Tactic:
calc
  ofReal (f b - f a) = ofReal (f b - f a' + (f a' - f a)) := by rw [sub_add_sub_cancel]
  _ ≤ ofReal (f b - f a') + ofReal (f a' - f a) := ENNReal.ofReal_add_le
  _ ≤ ∑' i, ofReal (f (g i).2 - f (g i).1) + ofReal δ :=
    (add_le_add (f.length_subadditive_Icc_Ioo I_subset) (ENNReal.ofReal_le_ofReal ha'.le))
  _ ≤ ∑' i, (f.length (s i) + ε' i) + δ :=
    (add_le_add (ENNReal.tsum_le_tsum fun i => (hg i).2.le)
      (by simp only [ENNReal.ofReal_coe_nnreal, le_rfl]))
  _ = ∑' i, f.length (s i) + ∑' i, (ε' i : ℝ≥0∞) + δ := by rw [ENNReal.tsum_add]
  _ ≤ ∑' i, f.length (s i) + δ + δ := add_le_add (add_le_add le_rfl hε.le) le_rfl
  _ = ∑' i : ℕ, f.length (s i) + ε := by 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' : ℝ
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) = ofReal (↑f b - ↑f a' + (↑f a' - ↑f a))

Tactic:
rw [sub_add_sub_cancel]

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, s i ⊆ Ioo p.1 p.2 ∧ ofReal (↑f p.2 - ↑f p.1) < f.length (s i) + ↑(ε' i)

Tactic:
have hl :=
  ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_ne_zero.2 (ε'0 i).ne')

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 : ℕ
hl : f.length (s i) < f.length (s i) + ↑(ε' i)
⊢ ∃ 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 < ↑δ
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε

Tactic:
rcases ENNReal.exists_pos_sum_of_countable δpos.ne' ℕ with ⟨ε', ε'0, hε⟩

Result:
case 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) < ↑δ
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s 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
⊢ 0 < ↑δ

Tactic:
simpa [δ] using εpos.ne'

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
⊢ ∃ a', ↑f a' - ↑f a < ↑δ ∧ a < a'

Tactic:
have B : f a - f a < δ := by rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]

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 : ContinuousWithinAt (fun r => ↑f r - ↑f a) (Ioi a) a
B : ↑f a - ↑f a < ↑δ
⊢ ∃ a', ↑f a' - ↑f a < ↑δ ∧ a < a'