awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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∞)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
have 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∞)
Tactic: choose g hg using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
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∞)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
have I_subset : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 → ℝ) b - (↑f : R → ℝ) a' + ((↑f : R → ℝ) a' - (↑f : R → ℝ) a))
have rw : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
Tactic: rw [sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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) + (↑(ε' i) : ℝ≥0∞)) + (↑δ : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞)) + (↑δ : ℝ≥0∞)
have 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∞)
Tactic: rw [ENNReal.tsum_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
have ofReal : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) =
  ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a' + ((↑f : R → ℝ) a' - (↑f : R → ℝ) a))
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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))
⊢ ENNReal.ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
have ofReal₁ : ∑' (i : ℕ), (f.length (s i) + (↑(ε' i) : ℝ≥0∞)) + (↑δ : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞)) + (↑δ : ℝ≥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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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∞)
⊢ ENNReal.ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
have ofReal₂ : ∑' (i : ℕ), f.length (s i) + (↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞) = ∑' (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
⊢ MeasurableSet (Ioi c)
have refine : ∀ (t : Set R), f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ f.length t
Tactic: refine OuterMeasure.ofFunction_caratheodory fun t => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
⊢ f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ f.length t
have this : Nonempty R
Tactic: have : Nonempty R := ⟨c⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
⊢ f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ f.length t
have 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)
Tactic: simp only [length_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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)
have 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)
Tactic: refine le_iInf fun a => le_iInf fun b => le_iInf fun h => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ 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)
have simp : f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
Tactic: simp only [← length_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 ∩ Ioi c) + f.length (t \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have rw : f.length (t \ botSet ∩ Ioi c) + f.length ((t \ botSet) \ 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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)
have 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)
Tactic: refine
    le_trans
      (add_le_add (f.length_mono <| inter_subset_inter_left _ h)
        (f.length_mono <| diff_subset_diff_left h)) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have 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)
Tactic: rcases le_total a c with hac | hac
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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)
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have 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)
Tactic: rcases le_total a c with hac | hac
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have 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)
Tactic: rcases le_total b c with hbc | hbc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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)
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have 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)
Tactic: rcases le_total b c with hbc | hbc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have 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)
Tactic: rcases le_total b c with hbc | hbc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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)
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have 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)
Tactic: rcases le_total b c with hbc | hbc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
have refine : ∀ (s : Set R),
  LE.le (α := ℝ≥0∞) ((f.outer.trim : (a : Set R) → ℝ≥0∞) s : ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine le_antisymm (fun s => ?_) (OuterMeasure.le_trim _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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∞) ((f.outer.trim : (a : Set R) → ℝ≥0∞) s : ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: rw [OuterMeasure.trim_eq_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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∞)
have 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∞)
Tactic: refine le_iInf fun t => le_iInf fun ht => ENNReal.le_of_forall_pos_le_add fun ε ε0 h => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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)) ∞
⊢ ⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t ≤
    ∑' (i : ℕ), f.length (t i) + (↑ε : ℝ≥0∞)
have 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∞)
Tactic: rcases ENNReal.exists_pos_sum_of_countable (ENNReal.coe_pos.2 ε0).ne' ℕ with ⟨ε', ε'0, hε⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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∞)
⊢ ⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t ≤
    ∑' (i : ℕ), f.length (t i) + (↑ε : ℝ≥0∞)
have 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∞))
Tactic: grw [← hε]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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∞)
⊢ ⨅ (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∞))
have 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∞)))
Tactic: rw [← ENNReal.tsum_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 : ℕ
⊢ ∃ (s : Set R), t i ⊆ s ∧ MeasurableSet s ∧ (f.outer : (a : Set R) → ℝ≥0∞) s ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)
have 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) : ℝ)
Tactic: rcases isEmpty_or_nonempty R with hR | hR