f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
⊢ ∀ (s : Finset ℕ) (b : ℝ),
    (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
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))
suffices
  ∀ (s : Finset ℕ) (b), Icc a b ⊆ (⋃ i ∈ (s : Set ℕ), Ioo (c i) (d i)) →
    (ofReal (f b - f a) : ℝ≥0∞) ≤ ∑ i in 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 [ext_iff, exists_prop, Finset.set_biUnion_coe, mem_iUnion, forall_const,
      iff_self_iff, Finite.mem_toFinset]
  rw [ENNReal.tsum_eq_iSup_sum]
  refine' le_trans _ (le_iSup _ hf.toFinset)
  exact this hf.toFinset _ (by simpa only [e] )
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
⊢ ∀ (s : Finset ℕ) (b : ℝ),
    (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
⊢ ∀ (s : Finset ℕ) (b : ℝ),
    (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
clear ss b
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
⊢ ∀ (s : Finset ℕ) (b : ℝ),
    (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
refine' fun s => Finset.strongInductionOn s fun s IH b cv => _
case inl
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : b ≤ a
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))

case inr
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : a ≤ b
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
cases' le_total b a with ab ab
case inr
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : a ≤ b
this : b ∈ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
case inr
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : a ≤ b
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
have := cv ⟨ab, le_rfl⟩
case inr
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : 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 in s, ofReal (↑f (d i) - ↑f (c i))
case inr
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : a ≤ b
this : b ∈ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
simp only [Finset.mem_coe, gt_iff_lt, not_lt, ge_iff_le, mem_iUnion, mem_Ioo, exists_and_left,
  exists_prop] at this
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : a ≤ b
i : ℕ
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
case inr
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : 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 in s, ofReal (↑f (d i) - ↑f (c i))
rcases this with ⟨i, cb, is, bd⟩
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ ⋃ (i_1 : ℕ) (_ : i_1 ∈ ↑(insert i (Finset.erase s i))), Ioo (c i_1) (d i_1)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in insert i (Finset.erase s i), ofReal (↑f (d i) - ↑f (c i))
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : a ≤ b
i : ℕ
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
rw [← Finset.insert_erase is] at cv ⊢
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in insert i (Finset.erase s i), ofReal (↑f (d i) - ↑f (c i))
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ ⋃ (i_1 : ℕ) (_ : i_1 ∈ ↑(insert i (Finset.erase s i))), Ioo (c i_1) (d i_1)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in insert i (Finset.erase s i), ofReal (↑f (d i) - ↑f (c i))
rw [Finset.coe_insert, biUnion_insert] at cv
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s 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 in Finset.erase s i, ofReal (↑f (d x) - ↑f (c x))
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in insert i (Finset.erase s i), ofReal (↑f (d i) - ↑f (c i))
rw [Finset.sum_insert (Finset.not_mem_erase _ _)]
case inr.intro.intro.intro.refine'_1
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s 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 : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ Icc a (c i) ⊆ ⋃ (i_1 : ℕ) (_ : i_1 ∈ ↑(Finset.erase s i)), Ioo (c i_1) (d i_1)
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s 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 in Finset.erase s i, ofReal (↑f (d x) - ↑f (c x))
refine' le_trans _ (add_le_add_left (IH _ (Finset.erase_ssubset is) (c i) _) _)
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 : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc ?m.230535 ?m.230536 ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))
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⟩
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 : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
e : (⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i)) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))
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 : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc ?m.230535 ?m.230536 ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))
have e : (⋃ i ∈ (hf.toFinset : Set ℕ), Ioo (c i) (d i)) = ⋃ i ∈ s, Ioo (c i) (d i) := by
  simp only [ext_iff, exists_prop, Finset.set_biUnion_coe, mem_iUnion, forall_const,
    iff_self_iff, Finite.mem_toFinset]
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 : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
e : (⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i)) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ⨆ (s : Finset ℕ), ∑ a in s, ofReal (↑f (d a) - ↑f (c a))
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 : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
e : (⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i)) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))
rw [ENNReal.tsum_eq_iSup_sum]
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 : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
e : (⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i)) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ a in Finite.toFinset hf, ofReal (↑f (d a) - ↑f (c a))
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 : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
e : (⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i)) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ⨆ (s : Finset ℕ), ∑ a in s, ofReal (↑f (d a) - ↑f (c a))
refine' le_trans _ (le_iSup _ hf.toFinset)
no goals
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 : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
e : (⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i)) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ a in Finite.toFinset hf, ofReal (↑f (d a) - ↑f (c a))
exact this hf.toFinset _ (by simpa only [e] )
no goals
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
⊢ Icc ?m.230535 ?m.230536 ⊆ ⋃ (i : ℕ) (_ : i ∈ univ), Ioo (c i) (d i)
simpa using ss
no goals
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ (⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i)) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
simp only [ext_iff, exists_prop, Finset.set_biUnion_coe, mem_iUnion, forall_const,
  iff_self_iff, Finite.mem_toFinset]
no goals
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
e : (⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i)) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i)
simpa only [e]
case inl
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : b ≤ a
⊢ 0 ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
case inl
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : b ≤ a
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
rw [ENNReal.ofReal_eq_zero.2 (sub_nonpos.2 (f.mono ab))]
no goals
case inl
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : b ≤ a
⊢ 0 ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
exact zero_le _
case inr.intro.intro.intro.refine'_1
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s 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 (c i) + (↑f (c i) - ↑f a)
case inr.intro.intro.intro.refine'_1
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s 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)
refine' le_trans (ENNReal.ofReal_le_ofReal _) ENNReal.ofReal_add_le
case inr.intro.intro.intro.refine'_1
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s 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
case inr.intro.intro.intro.refine'_1
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s 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 (c i) + (↑f (c i) - ↑f a)
rw [sub_add_sub_cancel]
no goals
case inr.intro.intro.intro.refine'_1
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s 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
exact sub_le_sub_right (f.mono bd.le) _
case inr.intro.intro.intro.refine'_2.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
x : ℝ
h₁ : a ≤ x
h₂ : x ≤ c i
⊢ x ∈ ⋃ (i_1 : ℕ) (_ : i_1 ∈ ↑(Finset.erase s i)), Ioo (c i_1) (d i_1)
case inr.intro.intro.intro.refine'_2
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ Icc a (c i) ⊆ ⋃ (i_1 : ℕ) (_ : i_1 ∈ ↑(Finset.erase s i)), Ioo (c i_1) (d i_1)
rintro x ⟨h₁, h₂⟩
no goals
case inr.intro.intro.intro.refine'_2.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        (Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i)) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
x : ℝ
h₁ : a ≤ x
h₂ : x ≤ c i
⊢ x ∈ ⋃ (i_1 : ℕ) (_ : i_1 ∈ ↑(Finset.erase s i)), Ioo (c i_1) (d i_1)
refine' (cv ⟨h₁, le_trans h₂ (le_of_lt cb)⟩).resolve_left (mt And.left (not_lt_of_le h₂))