-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem length_subadditive_Icc_Ioo {a b : ℝ} {c d : ℕ → ℝ} (ss : Icc a b ⊆ ⋃ i, Ioo (c i) (d i)) :
    ofReal (f b - f a) ≤ ∑' i, ofReal (f (d i) - f (c i))

Proof state:
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ i, Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))

Tactic:
suffices
  ∀ (s : Finset ℕ) (b), Icc a b ⊆ (⋃ i ∈ (s : Set ℕ), Ioo (c i) (d i)) →
    (ofReal (f b - f a) : ℝ≥0∞) ≤ ∑ i ∈ s, ofReal (f (d i) - f (c i)) by
  rcases isCompact_Icc.elim_finite_subcover_image
      (fun (i : ℕ) (_ : i ∈ univ) => @isOpen_Ioo _ _ _ _ (c i) (d i)) (by simpa using ss) with
    ⟨s, _, hf, hs⟩
  have e : ⋃ i ∈ (hf.toFinset : Set ℕ), Ioo (c i) (d i) = ⋃ i ∈ s, Ioo (c i) (d i) := by
    simp only [Set.ext_iff, exists_prop, Finset.set_biUnion_coe, mem_iUnion, forall_const,
      Finite.mem_toFinset]
  rw [ENNReal.tsum_eq_iSup_sum]
  refine le_trans ?_ (le_iSup _ hf.toFinset)
  exact this hf.toFinset _ (by simpa only [e] )

Result:
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ i, Ioo (c i) (d i)
⊢ ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))

Proof state:
case inr
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i)
ab : a ≤ b
this : b ∈ ⋃ i ∈ ↑s, Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))

Tactic:
simp only [Finset.mem_coe, gt_iff_lt, not_lt, mem_iUnion, mem_Ioo, exists_and_left,
  exists_prop] at this

Result:
case inr
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i)
ab : a ≤ b
this : ∃ i, c i < b ∧ i ∈ s ∧ b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))

Proof state:
case inl
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i)
ab : b ≤ a
⊢ 0 ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case intro.intro.intro
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ i, Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : s.Finite
hs : Icc a b ⊆ ⋃ i ∈ s, Ioo (c i) (d i)
e : ⋃ i ∈ ↑hf.toFinset, Ioo (c i) (d i) = ⋃ i ∈ s, Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ a ∈ hf.toFinset, ofReal (↑f (d a) - ↑f (c a))

Tactic:
exact this hf.toFinset _ (by simpa only [e] )

Result:
no goals

Proof state:
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i ∈ insert i (s.erase i), ofReal (↑f (d i) - ↑f (c i))

Tactic:
rw [Finset.sum_insert (Finset.not_mem_erase _ _)]

Result:
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i)) + ∑ x ∈ s.erase i, ofReal (↑f (d x) - ↑f (c x))

Proof state:
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i)) + ∑ x ∈ s.erase i, ofReal (↑f (d x) - ↑f (c x))

Tactic:
refine le_trans ?_ (add_le_add_left (IH _ (Finset.erase_ssubset is) (c i) ?_) _)

Result:
case inr.intro.intro.intro.refine_1
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i)) + ofReal (↑f (c i) - ↑f a)

case inr.intro.intro.intro.refine_2
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ Icc a (c i) ⊆ ⋃ i_1 ∈ ↑(s.erase i), Ioo (c i_1) (d i_1)

Proof state:
case intro.intro.intro
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ i, Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : s.Finite
hs : Icc a b ⊆ ⋃ i ∈ s, Ioo (c i) (d i)
e : ⋃ i ∈ ↑hf.toFinset, Ioo (c i) (d i) = ⋃ i ∈ s, Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))

Tactic:
rw [ENNReal.tsum_eq_iSup_sum]

Result:
case intro.intro.intro
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ i, Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : s.Finite
hs : Icc a b ⊆ ⋃ i ∈ s, Ioo (c i) (d i)
e : ⋃ i ∈ ↑hf.toFinset, Ioo (c i) (d i) = ⋃ i ∈ s, Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ⨆ s, ∑ a ∈ s, ofReal (↑f (d a) - ↑f (c a))

Proof state:
case inr.intro.intro.intro.refine_1
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ↑f b - ↑f a ≤ ↑f (d i) - ↑f a

Tactic:
exact sub_le_sub_right (f.mono bd.le) _

Result:
no goals

Proof state:
case inl
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i)
ab : b ≤ a
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))

Tactic:
rw [ENNReal.ofReal_eq_zero.2 (sub_nonpos.2 (f.mono ab))]

Result:
case inl
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i)
ab : b ≤ a
⊢ 0 ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))