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
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
hac : c ≤ a
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 [hbc, le_refl, Ioc_eq_empty, Ioc_inter_Ioi, min_eq_left, Ioc_diff_Ioi, f.length_empty,
      zero_add, or_true, le_sup_iff, f.length_Ioc, not_lt]

Premises used: le_refl, zero_add, Set.Ioc_eq_empty, StieltjesFunction.length_empty, Set.Ioc_diff_Ioi, min_eq_left, not_lt, le_sup_iff, Set.Ioc_inter_Ioi, StieltjesFunction.length_Ioc, or_true
-- 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
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,
      le_refl, Ioc_eq_empty, add_zero, max_eq_left, f.length_empty, not_lt]

Premises used: le_refl, max_eq_left, Set.Ioc_eq_empty, min_eq_right, StieltjesFunction.length_empty, Set.Ioc_diff_Ioi, not_lt, Set.Ioc_inter_Ioi, StieltjesFunction.length_Ioc, add_zero
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
⊢ f.outer.trim = f.outer

Tactic:
le_antisymm (fun s => ?_) (OuterMeasure.le_trim _)

Premises used: MeasureTheory.OuterMeasure.le_trim, le_antisymm
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
refine :
  ∀ (s : Set R),
    LE.le (α := ℝ≥0∞) ((f.outer.trim : (a : Set R) → ℝ≥0∞) s : ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) s : ℝ≥0∞)
⊢ f.outer.trim = f.outer

Tactic:
refine le_antisymm (fun s => ?_) (OuterMeasure.le_trim _)

Premises used: MeasureTheory.OuterMeasure.le_trim, le_antisymm
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
rw :
  LE.le (α := ℝ≥0∞) (⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t : ℝ≥0∞)
    ((f.outer : (a : Set R) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((f.outer.trim : (a : Set R) → ℝ≥0∞) s : ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [OuterMeasure.trim_eq_iInf]

Premises used: MeasureTheory.OuterMeasure.trim_eq_iInf
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t : ℝ≥0∞)
    ((f.outer : (a : Set R) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_iInf fun t => le_iInf fun ht => ENNReal.le_of_forall_pos_le_add fun ε ε0 h => ?_

Premises used: iInf, le_iInf, ENNReal.le_of_forall_pos_le_add, ite
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
refine :
  ∀ (t : ℕ → Set R) (ht : s ⊆ ⋃ (i : ℕ), t i) (ε : ℝ≥0) (ε0 : 0 < ε)
    (h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞),
    ⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t ≤
      ∑' (i : ℕ), f.length (t i) + (↑ε : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t : ℝ≥0∞)
    ((f.outer : (a : Set R) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine le_iInf fun t => le_iInf fun ht => ENNReal.le_of_forall_pos_le_add fun ε ε0 h => ?_

Premises used: le_iInf, ENNReal.le_of_forall_pos_le_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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
rcases :
  ∀ (ε' : ℕ → ℝ≥0) (ε'0 : ∀ (i : ℕ), 0 < ε' i) (hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)),
    ⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t ≤
      ∑' (i : ℕ), f.length (t i) + (↑ε : ℝ≥0∞)
⊢ ⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t ≤
    ∑' (i : ℕ), f.length (t i) + (↑ε : ℝ≥0∞)

Tactic:
rcases ENNReal.exists_pos_sum_of_countable (ENNReal.coe_pos.2 ε0).ne' ℕ with ⟨ε', ε'0, hε⟩

Premises used: Iff.mpr, LT.lt.ne', ENNReal.coe_pos, ENNReal.exists_pos_sum_of_countable, Nat
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
grw :
  ⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞))
⊢ ⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t ≤
    ∑' (i : ℕ), f.length (t i) + (↑ε : ℝ≥0∞)

Tactic:
grw [← hε]
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
rw :
  LE.le (α := ℝ≥0∞) (⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t)
    (∑' (a : ℕ), (f.length (t a) + (↑(ε' a) : ℝ≥0∞)))
⊢ ⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
inl :
  ∀ (hR : IsEmpty R),
    ∃ (s : Set R), t i ⊆ s ∧ MeasurableSet s ∧ (f.outer : (a : Set R) → ℝ≥0∞) s ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)
inr :
  ∀ (hR : Nonempty R),
    ∃ (s : Set R), t i ⊆ s ∧ MeasurableSet s ∧ (f.outer : (a : Set R) → ℝ≥0∞) s ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)
⊢ ∃ (s : Set R), t i ⊆ s ∧ MeasurableSet s ∧ (f.outer : (a : Set R) → ℝ≥0∞) s ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)

Tactic:
rcases isEmpty_or_nonempty R with hR | hR

Premises used: isEmpty_or_nonempty
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : IsEmpty R
⊢ (f.outer : (a : Set R) → ℝ≥0∞) ∅ ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)

Tactic:
simp
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : IsEmpty R
inl : t i ⊆ ∅
⊢ ∃ (s : Set R), t i ⊆ s ∧ MeasurableSet s ∧ (f.outer : (a : Set R) → ℝ≥0∞) s ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)

Tactic:
refine ⟨∅, ?_, MeasurableSet.empty, by simp⟩
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : IsEmpty R
⊢ t i ⊆ ∅

Tactic:
simpa using eq_empty_of_isEmpty (t i)

Premises used: Set.eq_empty_of_isEmpty
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
⊢ f.length (t i) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
have hl :=
        ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_pos.2 (ε'0 i)).ne'
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
hl : f.length (t i) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
lhs : f.length (t i)
| f.length (t i) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
lhs
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
hl : f.length (t i) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
rw : ⨅ (a : R), ⨅ (b : R), ⨅ (_ : t i \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
| f.length (t i)

Tactic:
rw [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
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
hl : f.length (t i) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
rw : ⨅ (a : R), ⨅ (b : R), ⨅ (_ : t i \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
| f.length (t i) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
lhs
        rw [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
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
hl : f.length (t i) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
⊢ ⨅ (a : R), ⨅ (b : R), ⨅ (_ : t i \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) <
    f.length (t i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
conv at hl =>
        lhs
        rw [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
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
hl :
  ⨅ (a : R), ⨅ (b : R), ⨅ (_ : t i \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) <
    f.length (t i) + (↑(ε' i) : ℝ≥0∞)
⊢ ∃ (i_1 : R) (i_2 : R) (_ : t i \ botSet ⊆ Ioc i_1 i_2),
    ofReal ((↑f : R → ℝ) i_2 - (↑f : R → ℝ) i_1) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
simp only [iInf_lt_iff] at hl

Premises used: iInf_lt_iff
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
hl :
  ∃ (i_1 : R) (i_2 : R) (_ : t i \ botSet ⊆ Ioc i_1 i_2),
    ofReal ((↑f : R → ℝ) i_2 - (↑f : R → ℝ) i_1) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
inr :
  ∀ (a b : R) (h₁ : t i \ botSet ⊆ Ioc a b)
    (h₂ : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)),
    ∃ (s : Set R), t i ⊆ s ∧ MeasurableSet s ∧ (f.outer : (a : Set R) → ℝ≥0∞) s ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)
⊢ ∃ (s : Set R), t i ⊆ s ∧ MeasurableSet s ∧ (f.outer : (a : Set R) → ℝ≥0∞) s ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)

Tactic:
rcases hl with ⟨a, b, h₁, h₂⟩
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i \ botSet ⊆ Ioc a b
h₂ : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
⊢ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
rw [← f.outer_Ioc] at h₂

Premises used: StieltjesFunction.outer_Ioc
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i \ botSet ⊆ Ioc a b
h₂ : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
⊢ t i ⊆ botSet ∪ Ioc a b

Tactic:
rw [diff_subset_iff] at h₁

Premises used: Set.diff_subset_iff
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i \ botSet ⊆ Ioc a b
h₂ : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
h₃ : t i ⊆ botSet ∪ Ioc a b
⊢ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
rw [diff_subset_iff] at h₁

Premises used: Set.diff_subset_iff
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i ⊆ botSet ∪ Ioc a b
h₂ : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
⊢ ∃ (s : Set R), t i ⊆ s ∧ MeasurableSet s ∧ (f.outer : (a : Set R) → ℝ≥0∞) s ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)

Tactic:
⟨_, h₁, measurableSet_botSet.union measurableSet_Ioc, le_of_lt ?_⟩

Premises used: le_of_lt, And.intro, MeasurableSet.union, Exists.intro, measurableSet_Ioc, measurableSet_botSet
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i ⊆ botSet ∪ Ioc a b
h₂ : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
inr : (f.outer : (a : Set R) → ℝ≥0∞) (botSet ∪ Ioc a b) < f.length (t i) + ofReal (↑(ε' i) : ℝ)
⊢ ∃ (s : Set R), t i ⊆ s ∧ MeasurableSet s ∧ (f.outer : (a : Set R) → ℝ≥0∞) s ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)

Tactic:
refine ⟨_, h₁, measurableSet_botSet.union measurableSet_Ioc, le_of_lt ?_⟩
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i ⊆ botSet ∪ Ioc a b
h₂ : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
⊢ (f.outer : (a : Set R) → ℝ≥0∞) (botSet ∪ Ioc a b) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) botSet : ℝ≥0∞)
      ((f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)

Tactic:
measure_union_le _ _

Premises used: MeasureTheory.measure_union_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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i ⊆ botSet ∪ Ioc a b
h₂ : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
bc : (f.outer : (a : Set R) → ℝ≥0∞) botSet ≤ f.length botSet
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) botSet : ℝ≥0∞)
      ((f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) ≤
    HAdd.hAdd (β := ℝ≥0∞) (f.length botSet) ((f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)

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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i ⊆ botSet ∪ Ioc a b
h₂ : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
⊢ (f.outer : (a : Set R) → ℝ≥0∞) botSet ≤ f.length botSet

Tactic:
apply outer_le_length

Premises used: StieltjesFunction.outer_le_length
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i ⊆ botSet ∪ Ioc a b
h₂ : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
simp : f.length (∅ \ botSet) + ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ HAdd.hAdd (β := ℝ≥0∞) (f.length botSet) ((f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞)

Tactic:
simp only [← length_diff_botSet, sdiff_self, bot_eq_empty, empty_diff, outer_Ioc, zero_add]

Premises used: sdiff_self, StieltjesFunction.length_diff_botSet, Set.bot_eq_empty, zero_add, StieltjesFunction.outer_Ioc, Set.empty_diff
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (t i)) ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i ⊆ botSet ∪ Ioc a b
h₂ : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
⊢ f.length (∅ \ botSet) + ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
simp [empty_diff]

Premises used: Set.empty_diff