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 : 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∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) =
    (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)

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 : 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∞) (Ioc a b) < f.length (t i) + ofReal (↑(ε' i) : ℝ)

Tactic:
simpa using 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₂ : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + (↑(ε' i) : ℝ≥0∞)
calc :
  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∞)
calc₁ :
  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∞)
calc₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) =
    (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)
calc₃ : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) < f.length (t i) + ofReal (↑(ε' i) : ℝ)
⊢ (f.outer : (a : Set R) → ℝ≥0∞) (botSet ∪ Ioc a b) < f.length (t i) + ofReal (↑(ε' i) : ℝ)

Tactic:
calc f.outer (botSet ∪ Ioc a b)
      _ ≤ f.outer botSet + f.outer (Ioc a b) := measure_union_le _ _
      _ ≤ f.length botSet + f.outer (Ioc a b) := by gcongr; apply outer_le_length
      _ = 0 + f.outer (Ioc a b) := by
        simp only [← length_diff_botSet, sdiff_self, bot_eq_empty, empty_diff, outer_Ioc, zero_add]
        simp [empty_diff]
      _ = f.outer (Ioc a b) := by simp
      _ < f.length (t i) + ofReal ↑(ε' i) := by simpa using h₂

Premises used: Set.Ioc, ENNReal.ofReal, StieltjesFunction.outer, StieltjesFunction.length, botSet, Union.union, DFunLike.coe, NNReal.toReal, 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∞)
choose :
  ∀ (g : (i : ℕ) → Set R)
    (hg :
      ∀ (i : ℕ),
        t i ⊆ g i ∧ MeasurableSet (g i) ∧ (f.outer : (a : Set R) → ℝ≥0∞) (g i) ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)),
    LE.le (α := ℝ≥0∞) (⨅ (t : Set R), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (f.outer : (a : Set R) → ℝ≥0∞) t)
      (∑' (a : ℕ), (f.length (t a) + (↑(ε' a) : ℝ≥0∞)))
⊢ 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:
choose g hg using
    show ∀ i, ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ f.outer s ≤ f.length (t i) + ofReal (ε' i) by
      intro i
      rcases isEmpty_or_nonempty R with hR | hR
      · refine ⟨∅, ?_, MeasurableSet.empty, by simp⟩
        simpa using eq_empty_of_isEmpty (t i)
      have hl :=
        ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_pos.2 (ε'0 i)).ne'
      conv at hl =>
        lhs
        rw [length_eq]
      simp only [iInf_lt_iff] at hl
      rcases hl with ⟨a, b, h₁, h₂⟩
      rw [← f.outer_Ioc] at h₂
      rw [diff_subset_iff] at h₁
      refine ⟨_, h₁, measurableSet_botSet.union measurableSet_Ioc, le_of_lt ?_⟩
      calc f.outer (botSet ∪ Ioc a b)
      _ ≤ f.outer botSet + f.outer (Ioc a b) := measure_union_le _ _
      _ ≤ f.length botSet + f.outer (Ioc a b) := by gcongr; apply outer_le_length
      _ = 0 + f.outer (Ioc a b) := by
        simp only [← length_diff_botSet, sdiff_self, bot_eq_empty, empty_diff, outer_Ioc, zero_add]
        simp [empty_diff]
      _ = f.outer (Ioc a b) := by simp
      _ < f.length (t i) + ofReal ↑(ε' i) := by simpa using 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∞)
g : (i : ℕ) → Set R
hg :
  ∀ (i : ℕ),
    t i ⊆ g i ∧ MeasurableSet (g i) ∧ (f.outer : (a : Set R) → ℝ≥0∞) (g i) ≤ f.length (t i) + ofReal (↑(ε' i) : ℝ)
⊢ ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ (f.outer : (a : Set R) → ℝ≥0∞) (g i) ≤ f.length (t i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
simp only [ofReal_coe_nnreal] at hg

Premises used: 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 : 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∞)
g : (i : ℕ) → Set R
hg :
  ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ (f.outer : (a : Set R) → ℝ≥0∞) (g i) ≤ f.length (t i) + (↑(ε' i) : ℝ≥0∞)
apply :
  LE.le (α := ℝ≥0∞) (⨅ (_ : s ⊆ iUnion g), ⨅ (_ : MeasurableSet (iUnion g)), (f.outer : (a : Set R) → ℝ≥0∞) (iUnion g))
    (∑' (a : ℕ), (f.length (t a) + (↑(ε' a) : ℝ≥0∞)))
⊢ 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:
apply iInf_le_of_le (iUnion g) _

Premises used: iInf_le_of_le, Set.iUnion
-- 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∞)
g : (i : ℕ) → Set R
hg :
  ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ (f.outer : (a : Set R) → ℝ≥0∞) (g i) ≤ f.length (t i) + (↑(ε' i) : ℝ≥0∞)
apply :
  LE.le (α := ℝ≥0∞) (⨅ (_ : MeasurableSet (iUnion g)), (f.outer : (a : Set R) → ℝ≥0∞) (iUnion g))
    (∑' (a : ℕ), (f.length (t a) + (↑(ε' a) : ℝ≥0∞)))
⊢ LE.le (α := ℝ≥0∞) (⨅ (_ : s ⊆ iUnion g), ⨅ (_ : MeasurableSet (iUnion g)), (f.outer : (a : Set R) → ℝ≥0∞) (iUnion g))
    (∑' (a : ℕ), (f.length (t a) + (↑(ε' a) : ℝ≥0∞)))

Tactic:
apply iInf_le_of_le (ht.trans <| iUnion_mono fun i => (hg i).1) _

Premises used: HasSubset.Subset.trans, And.left, Set.iUnion_mono, iInf_le_of_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∞)
g : (i : ℕ) → Set R
hg :
  ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ (f.outer : (a : Set R) → ℝ≥0∞) (g i) ≤ f.length (t i) + (↑(ε' i) : ℝ≥0∞)
apply :
  LE.le (α := ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) (iUnion g) : ℝ≥0∞)
    (∑' (a : ℕ), (f.length (t a) + (↑(ε' a) : ℝ≥0∞)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (⨅ (_ : MeasurableSet (iUnion g)), (f.outer : (a : Set R) → ℝ≥0∞) (iUnion g))
    (∑' (a : ℕ), (f.length (t a) + (↑(ε' a) : ℝ≥0∞)))

Tactic:
apply iInf_le_of_le (MeasurableSet.iUnion fun i => (hg i).2.1) _

Premises used: And.right, And.left, MeasurableSet.iUnion, iInf_le_of_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∞)
g : (i : ℕ) → Set R
hg :
  ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ (f.outer : (a : Set R) → ℝ≥0∞) (g i) ≤ f.length (t i) + (↑(ε' i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) (iUnion g) : ℝ≥0∞)
    (∑' (a : ℕ), (f.length (t a) + (↑(ε' a) : ℝ≥0∞)) : ℝ≥0∞)

Tactic:
le_trans (measure_iUnion_le _) (ENNReal.tsum_le_tsum fun i => (hg i).2.2)

Premises used: ENNReal.tsum_le_tsum, MeasureTheory.measure_iUnion_le, And.right, le_trans
-- 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∞)
g : (i : ℕ) → Set R
hg :
  ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ (f.outer : (a : Set R) → ℝ≥0∞) (g i) ≤ f.length (t i) + (↑(ε' i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) (iUnion g) : ℝ≥0∞)
    (∑' (a : ℕ), (f.length (t a) + (↑(ε' a) : ℝ≥0∞)) : ℝ≥0∞)

Tactic:
exact le_trans (measure_iUnion_le _) (ENNReal.tsum_le_tsum fun i => (hg i).2.2)

Premises used: ENNReal.tsum_le_tsum, MeasureTheory.measure_iUnion_le, And.right, le_trans
-- 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 : SecondCountableTopology R
rw : MeasurableSpace.generateFrom (range Ioi) ≤ f.outer.caratheodory
⊢ borel R ≤ f.outer.caratheodory

Tactic:
rw [borel_eq_generateFrom_Ioi]

Premises used: borel_eq_generateFrom_Ioi
-- 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 : SecondCountableTopology R
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ f.outer.caratheodory

Tactic:
MeasurableSpace.generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_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 : SecondCountableTopology R
refine : ∀ (t : Set R), Membership.mem (γ := Set (Set R)) (range Ioi) t → MeasurableSet t
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ f.outer.caratheodory

Tactic:
refine MeasurableSpace.generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_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 : SecondCountableTopology R
⊢ ∀ (t : Set R), Membership.mem (γ := Set (Set R)) (range Ioi) t → MeasurableSet t

Tactic:
simp +contextual [f.measurableSet_Ioi]

Premises used: StieltjesFunction.measurableSet_Ioi
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
_s : ℕ → Set R
hs : ∀ (i : ℕ), MeasurableSet (_s i)
i : ℕ
⊢ BorelSpace R

Tactic:
borelize R
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst_1 : LinearOrder R
inst_2 : TopologicalSpace R
f : StieltjesFunction R
inst_3 : OrderTopology R
inst_4 : CompactIccSpace R
inst_5 : MeasurableSpace R
inst_6 : BorelSpace R
inst_7 : SecondCountableTopology R
inst_8 : DenselyOrdered R
_s : ℕ → Set R
hs : ∀ (i : ℕ), MeasurableSet (_s i)
i : ℕ
inst : BorelSpace R
⊢ ∀ (i : ℕ), MeasurableSet (_s i)

Tactic:
borelize R
-- 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 : SecondCountableTopology R
inst_5 : DenselyOrdered R
_s : ℕ → Set R
i : ℕ
inst_6 : BorelSpace R
hs : ∀ (i : ℕ), MeasurableSet (_s i)
this : MeasurableSpace R := borel R
⊢ MeasurableSet (_s i)

Tactic:
hs i
-- 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 : SecondCountableTopology R
inst_5 : DenselyOrdered R
_s : ℕ → Set R
i : ℕ
inst_6 : BorelSpace R
hs : ∀ (i : ℕ), MeasurableSet (_s i)
this : MeasurableSpace R := borel R
⊢ MeasurableSet (_s i)

Tactic:
exact hs i
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
rw :
  (let __OuterMeasure := f.outer;
        ({ toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ } : Measure R) :
        (a : Set R) → ℝ≥0∞)
      (Ioc a b) =
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc a b) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
rw [StieltjesFunction.measure]

Premises used: StieltjesFunction.measure
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
⊢ (let __OuterMeasure := f.outer;
        ({ toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ } : Measure R) :
        (a : Set R) → ℝ≥0∞)
      (Ioc a b) =
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
f.outer_Ioc a b

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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
⊢ (let __OuterMeasure := f.outer;
        ({ toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ } : Measure R) :
        (a : Set R) → ℝ≥0∞)
      (Ioc a b) =
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
exact f.outer_Ioc a b

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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
pos :
  ∀ (ha : IsBot a),
    ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
neg :
  ∀ (ha : ¬IsBot a),
    ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)

Tactic:
by_cases ha : IsBot a

Premises used: IsBot
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
h : 𝓝[<] a = ⊥
⊢ leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a

Tactic:
apply leftLim_eq_of_eq_bot

Premises used: leftLim_eq_of_eq_bot
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
⊢ 𝓝[<] a = ⊥

Tactic:
simp [nhdsLT_eq_bot_iff, ha]

Premises used: nhdsLT_eq_bot_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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
⊢ leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a

Tactic:
have : leftLim f a = f a := by
      apply leftLim_eq_of_eq_bot
      simp [nhdsLT_eq_bot_iff, ha]
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
pos : Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)

Tactic:
simp only [this, sub_self, ofReal_zero]

Premises used: sub_self, ENNReal.ofReal_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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
pos : LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} : ℝ≥0∞) (⊥ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply eq_bot_iff.2

Premises used: Iff.mpr, eq_bot_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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
pos :
  LE.le (α := ℝ≥0∞)
    ((let __OuterMeasure := f.outer;
          ({ toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ } : Measure R) :
          (a : Set R) → ℝ≥0∞)
        {a} :
      ℝ≥0∞)
    (⊥ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} : ℝ≥0∞) (⊥ : ℝ≥0∞)

Tactic:
rw [StieltjesFunction.measure]

Premises used: StieltjesFunction.measure
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
pos : f.length {a} ≤ ⊥
⊢ LE.le (α := ℝ≥0∞)
    ((let __OuterMeasure := f.outer;
          ({ toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ } : Measure R) :
          (a : Set R) → ℝ≥0∞)
        {a} :
      ℝ≥0∞)
    (⊥ : ℝ≥0∞)

Tactic:
apply (outer_le_length _ _).trans

Premises used: StieltjesFunction.outer_le_length, LE.le.trans
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
pos : f.length ({a} \ botSet) ≤ ⊥
⊢ f.length {a} ≤ ⊥

Tactic:
rw [← length_diff_botSet]

Premises used: StieltjesFunction.length_diff_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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
⊢ f.length ({a} \ botSet) ≤ ⊥

Tactic:
simp [subsingleton_botSet.eq_singleton_of_mem ha]

Premises used: Set.Subsingleton.eq_singleton_of_mem, subsingleton_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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
⊢ ∃ (b : R), b < a

Tactic:
simpa only [IsBot, not_forall, not_le] using ha

Premises used: not_le, IsBot, Classical.not_forall
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
neg :
  ∀ (b : R) (hb : b < a),
    ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)

Tactic:
obtain ⟨b, hb⟩ : ∃ b, b < a := by simpa only [IsBot, not_forall, not_le] using ha
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
⊢ ∃ (u : ℕ → R), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo b a) ∧ Tendsto u atTop (𝓝 a)

Tactic:
exists_seq_strictMono_tendsto' hb

Premises used: exists_seq_strictMono_tendsto'