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 : 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∞) (⨅ (_ : MeasurableSet (iUnion g)), (f.outer : (a : Set R) → ℝ≥0∞) (iUnion g))
    (∑' (a : ℕ), (f.length (t a) + (↑(ε' a) : ℝ≥0∞)))
have apply : LE.le (α := ℝ≥0∞) ((f.outer : (a : Set R) → ℝ≥0∞) (iUnion g) : ℝ≥0∞)
  (∑' (a : ℕ), (f.length (t a) + (↑(ε' a) : ℝ≥0∞)) : ℝ≥0∞)
Tactic: apply iInf_le_of_le (MeasurableSet.iUnion fun i => (hg i).2.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 : SecondCountableTopology R
⊢ borel R ≤ f.outer.caratheodory
have rw : MeasurableSpace.generateFrom (range Ioi) ≤ f.outer.caratheodory
Tactic: rw [borel_eq_generateFrom_Ioi]
-- 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 : SecondCountableTopology R
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ f.outer.caratheodory
have refine : ∀ (t : Set R), Membership.mem (γ := Set (Set R)) (range Ioi) t → MeasurableSet t
Tactic: refine MeasurableSpace.generateFrom_le ?_
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
_s : ℕ → Set R
hs : ∀ (i : ℕ), MeasurableSet (_s i)
i : ℕ
⊢ MeasurableSet (_s i)
have inst : BorelSpace R
Tactic: borelize R
Cleared hypotheses: inst_4, inst_5, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
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
⊢ MeasurableSet (_s i)
have hs₁ : ∀ (i : ℕ), MeasurableSet (_s i)
Tactic: borelize R
Cleared hypotheses: inst_5, inst_6, hs
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc a b) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have rw : (let __OuterMeasure := f.outer;
      ({ toOuterMeasure := __OuterMeasure, m_iUnion := sorry, trim_le := sorry } : Measure R) :
      (a : Set R) → ℝ≥0∞)
    (Ioc a b) =
  ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
Tactic: rw [StieltjesFunction.measure]
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
have pos : ∀ (ha : IsBot a), ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
Tactic: by_cases ha : IsBot a
-- 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 : 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)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
have neg : ∀ (ha : ¬IsBot a), ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
Tactic: by_cases ha : IsBot a
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
⊢ leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
have h : 𝓝[<] a = ⊥
Tactic: apply leftLim_eq_of_eq_bot
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
have this : 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]
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
have pos : Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [this, sub_self, ofReal_zero]
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
have pos : LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} : ℝ≥0∞) (⊥ : ℝ≥0∞)
Tactic: apply eq_bot_iff.2
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
⊢ LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} : ℝ≥0∞) (⊥ : ℝ≥0∞)
have pos : LE.le (α := ℝ≥0∞)
  ((let __OuterMeasure := f.outer;
        ({ toOuterMeasure := __OuterMeasure, m_iUnion := sorry, trim_le := sorry } : Measure R) :
        (a : Set R) → ℝ≥0∞)
      {a} :
    ℝ≥0∞)
  (⊥ : ℝ≥0∞)
Tactic: rw [StieltjesFunction.measure]
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
⊢ LE.le (α := ℝ≥0∞)
    ((let __OuterMeasure := f.outer;
          ({ toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ } : Measure R) :
          (a : Set R) → ℝ≥0∞)
        {a} :
      ℝ≥0∞)
    (⊥ : ℝ≥0∞)
have pos : f.length {a} ≤ ⊥
Tactic: apply (outer_le_length _ _).trans
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f : R → ℝ) a = (↑f : R → ℝ) a
⊢ f.length {a} ≤ ⊥
have pos : f.length ({a} \ botSet) ≤ ⊥
Tactic: rw [← length_diff_botSet]
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
have neg : ∀ (b : R) (hb : b < 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
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
have neg : ∀ (u : ℕ → R) (u_mono : StrictMono u) (u_lt_a : ∀ (n : ℕ), u n ∈ Ioo b a) (u_lim : Tendsto u atTop (𝓝 a)),
  ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
Tactic: obtain ⟨u, u_mono, u_lt_a, u_lim⟩ :
    ∃ u : ℕ → R, StrictMono u ∧ (∀ n : ℕ, u n ∈ Ioo b a) ∧ Tendsto u atTop (𝓝 a) :=
    exists_seq_strictMono_tendsto' hb
-- 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 : 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
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n ∈ Ioo b a
u_lim : Tendsto u atTop (𝓝 a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
have u_lt_a₁ : ∀ (n : ℕ), u n < a
Tactic: replace u_lt_a n : u n < a := (u_lt_a n).2
Cleared hypotheses: u_lt_a
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
⊢ Eq (α := Set R) {a} (⋂ (n : ℕ), Ioc (u n) a)
have refine : ∀ (x : R) (hx : Membership.mem (γ := Set R) (⋂ (n : ℕ), Ioc (u n) a) x), Membership.mem (γ := Set R) {a} x
Tactic: refine Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => ?_
-- 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 : 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
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : R
hx : Membership.mem (γ := Set R) (⋂ (n : ℕ), Ioc (u n) a) x
⊢ Membership.mem (γ := Set R) {a} x
have hx₁ : ∀ (i : ℕ), u i < x ∧ x ≤ a
Tactic: replace hx : ∀ (i : ℕ), u i < x ∧ x ≤ a := by simpa using hx
Cleared hypotheses: hx
-- 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 : 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
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : R
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
⊢ Membership.mem (γ := Set R) {a} x
have this : a ≤ x
Tactic: have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le
-- 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 : 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
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
have A : Eq (α := Set R) {a} (⋂ (n : ℕ), Ioc (u n) a)
Tactic: have A : {a} = ⋂ n, Ioc (u n) a := by
    refine Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => ?_
    replace hx : ∀ (i : ℕ), u i < x ∧ x ≤ a := by simpa using hx
    have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le
    simp [le_antisymm this (hx 0).2]
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set R) {a} (⋂ (n : ℕ), Ioc (u n) a)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u n) a) : ℝ≥0∞)) atTop
    (𝓝 (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a}) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u n) a) : ℝ≥0∞)) atTop
  (𝓝 (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (⋂ (n : ℕ), Ioc (u n) a)) : Filter ℝ≥0∞)
Tactic: rw [A]
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set R) {a} (⋂ (n : ℕ), Ioc (u n) a)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u n) a) : ℝ≥0∞)) atTop
    (𝓝 (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (⋂ (n : ℕ), Ioc (u n) a)) : Filter ℝ≥0∞)
have refine_1 : ∀ (m n : ℕ) (hmn : m ≤ n), Ioc (u n) a ≤ Ioc (u m) a
Tactic: refine tendsto_measure_iInter_atTop (fun n => nullMeasurableSet_Ioc)
      (fun m n hmn => ?_) ?_
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set R) {a} (⋂ (n : ℕ), Ioc (u n) a)
refine_1 : ∀ (m n : ℕ) (hmn : m ≤ n), Ioc (u n) a ≤ Ioc (u m) a
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u n) a) : ℝ≥0∞)) atTop
    (𝓝 (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (⋂ (n : ℕ), Ioc (u n) a)) : Filter ℝ≥0∞)
have refine_2 : ∃ (i : ℕ), Ne (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u i) a) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine tendsto_measure_iInter_atTop (fun n => nullMeasurableSet_Ioc)
      (fun m n hmn => ?_) ?_
-- 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 : 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
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set R) {a} (⋂ (n : ℕ), Ioc (u n) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
have L1 : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u n) a) : ℝ≥0∞)) atTop
  (𝓝 (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a}) : Filter ℝ≥0∞)
Tactic: have L1 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a})) := by
    rw [A]
    refine tendsto_measure_iInter_atTop (fun n => nullMeasurableSet_Ioc)
      (fun m n hmn => ?_) ?_
    · exact Ioc_subset_Ioc_left (u_mono.monotone hmn)
    · exact ⟨0, by simpa only [measure_Ioc] using ENNReal.ofReal_ne_top⟩
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set R) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u n) a) : ℝ≥0∞)) atTop
    (𝓝 (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a}) : Filter ℝ≥0∞)
⊢ Tendsto (fun (n : ℕ) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u n) a)) atTop
    (𝓝 (ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)))
have simp : Tendsto (fun (n : ℕ) ↦ ofReal ((↑f : R → ℝ) a - (↑f : R → ℝ) (u n))) atTop
  (𝓝 (ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)))
Tactic: simp only [measure_Ioc]
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set R) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u n) a) : ℝ≥0∞)) atTop
    (𝓝 (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a}) : Filter ℝ≥0∞)
⊢ Tendsto (fun (n : ℕ) ↦ (↑f : R → ℝ) (u n)) atTop (𝓝 (leftLim (↑f : R → ℝ) a))
have apply : Tendsto u atTop (𝓝[<] a)
Tactic: apply (f.mono.tendsto_leftLim a).comp
-- 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 : 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
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set R) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u n) a) : ℝ≥0∞)) atTop
    (𝓝 (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a}) : Filter ℝ≥0∞)
⊢ Tendsto (fun (n : ℕ) ↦ ofReal ((↑f : R → ℝ) a - (↑f : R → ℝ) (u n))) atTop
    (𝓝 (ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)))
have this : Tendsto (fun (n : ℕ) ↦ (↑f : R → ℝ) (u n)) atTop (𝓝 (leftLim (↑f : R → ℝ) a))
Tactic: have : Tendsto (fun n => f (u n)) atTop (𝓝 (leftLim f a)) := by
      apply (f.mono.tendsto_leftLim a).comp
      exact
        tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim
          (Eventually.of_forall fun n => u_lt_a n)
-- 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 : 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
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set R) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u n) a) : ℝ≥0∞)) atTop
    (𝓝 (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a}) : Filter ℝ≥0∞)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)
have L2 : Tendsto (fun (n : ℕ) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u n) a)) atTop
  (𝓝 (ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)))
Tactic: have L2 :
      Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (ofReal (f a - leftLim f a))) := by
    simp only [measure_Ioc]
    have : Tendsto (fun n => f (u n)) atTop (𝓝 (leftLim f a)) := by
      apply (f.mono.tendsto_leftLim a).comp
      exact
        tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim
          (Eventually.of_forall fun n => u_lt_a n)
    exact ENNReal.continuous_ofReal.continuousAt.tendsto.comp (tendsto_const_nhds.sub this)
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have inl : ∀ (hab : a ≤ b),
  ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
Tactic: rcases le_or_gt a b with (hab | hab)
-- 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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
inl :
  ∀ (hab : a ≤ b),
    ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have inr : ∀ (hab : b < a),
  ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
Tactic: rcases le_or_gt a b with (hab | hab)