awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
⊢ ∀ (i : ℕ),
    ∃ (p : R × R),
      Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
have : ∀ i, ∃ p : R × R, Icc a' b ∩ s i ⊆ Iotop 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_eq]
    simp only [iInf_lt_iff, exists_prop] at hl
    rcases hl with ⟨p, q', spq, hq'⟩
    have A : Icc a' b ∩ s i ⊆ Ioc p q' := by
      rintro x ⟨hx, h'x⟩
      apply spq
      simp [h'x, notMem_botSet_of_lt (aa'.trans_le hx.1)]
    by_cases htq' : IsTop q'
    · refine ⟨(p, q'), ?_, hq'⟩
      rintro x hx
      simp only [Iotop, htq', ↓reduceIte, mem_Ioc]
      exact ⟨(A hx).1, htq' _⟩
    have : (𝓝[>] q').NeBot := by simp [Filter.neBot_iff, nhdsGT_eq_bot_iff, htq', not_covBy]
    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⟩, A.trans ((Ioc_subset_Ioo_right q'q).trans Ioo_subset_Iotop), hq⟩
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this_1 : Nonempty R
this :
  ∀ (i : ℕ),
    ∃ (p : R × R),
      Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
choose :
  ∀ (g : (i : ℕ) → R × R)
    (hg :
      ∀ (i : ℕ),
        Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧
          ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)),
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)

Tactic:
choose g hg using this
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
g : (i : ℕ) → R × R
hg :
  ∀ (i : ℕ),
    Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧
      ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ Icc a' b ∩ Ioc a b ⊆ Icc a' b ∩ ⋃ (i : ℕ), s i

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
g : (i : ℕ) → R × R
hg :
  ∀ (i : ℕ),
    Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧
      ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ Icc a' b ⊆ ⋃ (i : ℕ), Iotop (g i).1 (g i).2

Tactic:
have I_subset : Icc a' b ⊆ ⋃ i, Iotop (g i).1 (g i).2 :=
    calc
      Icc a' b ⊆ Icc a' b ∩ Ioc a b := fun x hx => ⟨hx, aa'.trans_le hx.1, hx.2⟩
      _ ⊆ Icc a' b ∩ ⋃ i, s i := by gcongr
      _ = ⋃ i, Icc a' b ∩ s i := inter_iUnion (Icc a' b) s
      _ ⊆ ⋃ i, Iotop (g i).1 (g i).2 := iUnion_mono fun i => (hg i).1
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
g : (i : ℕ) → R × R
hg :
  ∀ (i : ℕ),
    Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧
      ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Iotop (g i).1 (g i).2
rw rw₁ : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) =
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a' + ((↑f : R → ℝ) a' - (↑f : R → ℝ) a))

Tactic:
rw [sub_add_sub_cancel]

Premises used: sub_add_sub_cancel
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
g : (i : ℕ) → R × R
hg :
  ∀ (i : ℕ),
    Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧
      ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Iotop (g i).1 (g i).2
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a' + ((↑f : R → ℝ) a' - (↑f : R → ℝ) a)) ≤
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a') + ofReal ((↑f : R → ℝ) a' - (↑f : R → ℝ) a)

Tactic:
ENNReal.ofReal_add_le

Premises used: ENNReal.ofReal_add_le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
g : (i : ℕ) → R × R
hg :
  ∀ (i : ℕ),
    Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧
      ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Iotop (g i).1 (g i).2
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a') + ofReal ((↑f : R → ℝ) a' - (↑f : R → ℝ) a) ≤
    ∑' (i : ℕ), ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) + ofReal (↑δ : ℝ)

Tactic:
(add_le_add (f.length_subadditive_Icc_Ioo I_subset) (ENNReal.ofReal_le_ofReal ha'.le))

Premises used: add_le_add, ENNReal.ofReal_le_ofReal, StieltjesFunction.length_subadditive_Icc_Ioo, LT.lt.le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
g : (i : ℕ) → R × R
hg :
  ∀ (i : ℕ),
    Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧
      ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Iotop (g i).1 (g i).2
⊢ ofReal (↑δ : ℝ) ≤ (↑δ : ℝ≥0∞)

Tactic:
simp only [ENNReal.ofReal_coe_nnreal, le_rfl]

Premises used: le_rfl, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
g : (i : ℕ) → R × R
hg :
  ∀ (i : ℕ),
    Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧
      ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Iotop (g i).1 (g i).2
rw rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), f.length (s a)) (∑' (a : ℕ), (↑(ε' a) : ℝ≥0∞)) + (↑δ : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞)) + (↑δ : ℝ≥0∞)
⊢ ∑' (i : ℕ), (f.length (s i) + (↑(ε' i) : ℝ≥0∞)) + (↑δ : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞)) + (↑δ : ℝ≥0∞)

Tactic:
rw [ENNReal.tsum_add]

Premises used: ENNReal.tsum_add
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
g : (i : ℕ) → R × R
hg :
  ∀ (i : ℕ),
    Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧
      ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Iotop (g i).1 (g i).2
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞)) + (↑δ : ℝ≥0∞) ≤
    ∑' (i : ℕ), f.length (s i) + (↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)

Tactic:
add_le_add (add_le_add le_rfl hε.le) le_rfl

Premises used: le_rfl, add_le_add, LT.lt.le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
g : (i : ℕ) → R × R
hg :
  ∀ (i : ℕ),
    Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧
      ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Iotop (g i).1 (g i).2
⊢ ∑' (i : ℕ), f.length (s i) + (↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞) = ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)

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

Premises used: add_assoc, ENNReal.add_halves
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
g : (i : ℕ) → R × R
hg :
  ∀ (i : ℕ),
    Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧
      ENNReal.ofReal ((↑f : R → ℝ) (g i).2 - (↑f : R → ℝ) (g i).1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Iotop (g i).1 (g i).2
ofReal :
  ENNReal.ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) =
    ENNReal.ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a' + ((↑f : R → ℝ) a' - (↑f : R → ℝ) a))
ofReal₁ :
  ∑' (i : ℕ), (f.length (s i) + (↑(ε' i) : ℝ≥0∞)) + (↑δ : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞)) + (↑δ : ℝ≥0∞)
ofReal₂ : ∑' (i : ℕ), f.length (s i) + (↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞) = ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
⊢ ENNReal.ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)

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]

Premises used: ENNReal.tsum_le_tsum, le_rfl, ENNReal.ofReal, add_le_add, HSub.hSub, ENNReal.ofReal_add_le, ENNReal.ofReal_le_ofReal, StieltjesFunction.toFun, StieltjesFunction.length_subadditive_Icc_Ioo, LT.lt.le, And.right, HAdd.hAdd, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
⊢ MeasurableSet (Ioi c)

Tactic:
OuterMeasure.ofFunction_caratheodory fun t => ?_

Premises used: StieltjesFunction.outer, MeasureTheory.OuterMeasure.ofFunction_caratheodory
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
refine : ∀ (t : Set R), f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ f.length t
⊢ MeasurableSet (Ioi c)

Tactic:
refine OuterMeasure.ofFunction_caratheodory fun t => ?_

Premises used: MeasureTheory.OuterMeasure.ofFunction_caratheodory
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
⊢ Nonempty R

Tactic:
have : Nonempty R := ⟨c⟩
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
simp :
  HAdd.hAdd (α := ℝ≥0∞)
      (⨅ (a : R), ⨅ (b : R), ⨅ (_ : (t ∩ Ioi c) \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))
      (⨅ (a : R), ⨅ (b : R), ⨅ (_ : (t \ Ioi c) \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)) ≤
    ⨅ (a : R), ⨅ (b : R), ⨅ (_ : t \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ f.length t

Tactic:
simp only [length_eq]

Premises used: StieltjesFunction.length_eq
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (⨅ (a : R), ⨅ (b : R), ⨅ (_ : (t ∩ Ioi c) \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))
      (⨅ (a : R), ⨅ (b : R), ⨅ (_ : (t \ Ioi c) \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)) ≤
    ⨅ (a : R), ⨅ (b : R), ⨅ (_ : t \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
le_iInf fun a => le_iInf fun b => le_iInf fun h => ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
refine :
  ∀ (a b : R) (h : t \ botSet ⊆ Ioc a b),
    HAdd.hAdd (α := ℝ≥0∞)
        (⨅ (a : R), ⨅ (b : R), ⨅ (_ : (t ∩ Ioi c) \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))
        (⨅ (a : R), ⨅ (b : R), ⨅ (_ : (t \ Ioi c) \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)) ≤
      ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (⨅ (a : R), ⨅ (b : R), ⨅ (_ : (t ∩ Ioi c) \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))
      (⨅ (a : R), ⨅ (b : R), ⨅ (_ : (t \ Ioi c) \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)) ≤
    ⨅ (a : R), ⨅ (b : R), ⨅ (_ : t \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
refine le_iInf fun a => le_iInf fun b => le_iInf fun h => ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
simp : f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (⨅ (a : R), ⨅ (b : R), ⨅ (_ : (t ∩ Ioi c) \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))
      (⨅ (a : R), ⨅ (b : R), ⨅ (_ : (t \ Ioi c) \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)) ≤
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
simp only [← length_eq]

Premises used: StieltjesFunction.length_eq
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
rw : f.length (t \ botSet ∩ Ioi c) + f.length ((t \ botSet) \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
rw [← length_diff_botSet, inter_diff_right_comm, ← length_diff_botSet (s := t \ Ioi c),
    diff_diff_comm]

Premises used: Set.inter_diff_right_comm, StieltjesFunction.length_diff_botSet, Set.diff_diff_comm
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
⊢ f.length (t \ botSet ∩ Ioi c) + f.length ((t \ botSet) \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
le_trans
      (add_le_add (f.length_mono <| inter_subset_inter_left _ h)
        (f.length_mono <| diff_subset_diff_left h)) ?_

Premises used: add_le_add, Set.diff_subset_diff_left, Set.inter_subset_inter_left, StieltjesFunction.length_mono, le_trans
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
inter_subset_inter_left :
  f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ f.length (t \ botSet ∩ Ioi c) + f.length ((t \ botSet) \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
refine
    le_trans
      (add_le_add (f.length_mono <| inter_subset_inter_left _ h)
        (f.length_mono <| diff_subset_diff_left h)) ?_

Premises used: add_le_add, Set.diff_subset_diff_left, Set.inter_subset_inter_left, StieltjesFunction.length_mono, le_trans
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
inl :
  ∀ (hac : a ≤ c), f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
inr :
  ∀ (hac : c ≤ a), f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
rcases le_total a c with hac | hac

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
hac : a ≤ c
inl :
  ∀ (hbc : b ≤ c), f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
inl₁ :
  ∀ (hbc : c ≤ b), f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
rcases le_total b c with hbc | hbc

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
hac : c ≤ a
inr :
  ∀ (hbc : b ≤ c), f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
inr₁ :
  ∀ (hbc : c ≤ b), f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
rcases le_total b c with hbc | hbc

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
hac : a ≤ c
hbc : b ≤ c
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
simp only [Ioc_inter_Ioi, f.length_Ioc, hac, hbc, le_refl, Ioc_eq_empty,
      max_eq_right, min_eq_left, Ioc_diff_Ioi, f.length_empty, zero_add, not_lt]

Premises used: le_refl, zero_add, Set.Ioc_eq_empty, max_eq_right, StieltjesFunction.length_empty, Set.Ioc_diff_Ioi, min_eq_left, not_lt, Set.Ioc_inter_Ioi, StieltjesFunction.length_Ioc
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
hac : a ≤ c
hbc : c ≤ b
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
simp only [hac, hbc, Ioc_inter_Ioi, Ioc_diff_Ioi, f.length_Ioc, min_eq_right,
      ← ENNReal.ofReal_add, f.mono hac, f.mono hbc, sub_nonneg,
      sub_add_sub_cancel, le_refl,
      max_eq_right]

Premises used: le_refl, sub_add_sub_cancel, StieltjesFunction.mono, min_eq_right, max_eq_right, Set.Ioc_diff_Ioi, ENNReal.ofReal_add, Set.Ioc_inter_Ioi, StieltjesFunction.length_Ioc, sub_nonneg