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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
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)
⊢ ((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

Premises used: exists_seq_strictMono_tendsto'
-- 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
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n ∈ Ioo b a
u_lim : Tendsto u atTop (𝓝 a)
⊢ ∀ (n : ℕ), u n < a

Tactic:
replace u_lt_a n : u n < a := (u_lt_a n).2
-- 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
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : R
hx : Membership.mem (γ := Set R) {a} x
⊢ Membership.mem (γ := Set R) (⋂ (n : ℕ), Ioc (u n) a) x

Tactic:
simp [mem_singleton_iff.1 hx, u_lt_a]

Premises used: Set.mem_singleton_iff, Iff.mp
-- 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
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
refine : ∀ (x : R) (hx : Membership.mem (γ := Set R) (⋂ (n : ℕ), Ioc (u n) a) x), Membership.mem (γ := Set R) {a} x
⊢ Eq (α := Set R) {a} (⋂ (n : ℕ), Ioc (u n) a)

Tactic:
refine Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => ?_

Premises used: Set.Subset.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 : 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
⊢ ∀ (i : ℕ), u i < x ∧ x ≤ a

Tactic:
simpa using hx
-- 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
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
⊢ ∀ (i : ℕ), u i < x ∧ x ≤ a

Tactic:
replace hx : ∀ (i : ℕ), u i < x ∧ x ≤ a := by simpa using hx
-- 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
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
⊢ a ≤ x

Tactic:
have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.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 : 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
this : a ≤ x
⊢ Membership.mem (γ := Set R) {a} x

Tactic:
simp [le_antisymm this (hx 0).2]

Premises used: le_antisymm, And.right, OfNat.ofNat
-- 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
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)

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]
-- 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
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)
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∞)
⊢ 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:
rw [A]
-- 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
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∞)

Tactic:
tendsto_measure_iInter_atTop (fun n => nullMeasurableSet_Ioc)
      (fun m n hmn => ?_) ?_

Premises used: nullMeasurableSet_Ioc, MeasureTheory.tendsto_measure_iInter_atTop
-- 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
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
refine_2 : ∃ (i : ℕ), Ne (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u i) a) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 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:
refine tendsto_measure_iInter_atTop (fun n => nullMeasurableSet_Ioc)
      (fun m n hmn => ?_) ?_

Premises used: nullMeasurableSet_Ioc, MeasureTheory.tendsto_measure_iInter_atTop
-- 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
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)
m n : ℕ
hmn : m ≤ n
⊢ Ioc (u n) a ≤ Ioc (u m) a

Tactic:
Ioc_subset_Ioc_left (u_mono.monotone hmn)

Premises used: StrictMono.monotone, Set.Ioc_subset_Ioc_left
-- 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
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)
m n : ℕ
hmn : m ≤ n
⊢ Ioc (u n) a ≤ Ioc (u m) a

Tactic:
exact Ioc_subset_Ioc_left (u_mono.monotone hmn)

Premises used: StrictMono.monotone, Set.Ioc_subset_Ioc_left
-- 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
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)
⊢ Ne (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u 0) a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa only [measure_Ioc] using ENNReal.ofReal_ne_top

Premises used: StieltjesFunction.measure_Ioc, ENNReal.ofReal_ne_top
-- 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
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)
⊢ ∃ (i : ℕ), Ne (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc (u i) a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨0, by simpa only [measure_Ioc] using ENNReal.ofReal_ne_top⟩
-- 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
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∞)

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⟩
-- 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
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∞)
simp :
  Tendsto (fun (n : ℕ) ↦ ofReal ((↑f : R → ℝ) a - (↑f : R → ℝ) (u n))) atTop
    (𝓝 (ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)))
⊢ 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:
simp only [measure_Ioc]

Premises used: StieltjesFunction.measure_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
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∞)
apply : Tendsto u atTop (𝓝[<] a)
⊢ Tendsto (fun (n : ℕ) ↦ (↑f : R → ℝ) (u n)) atTop (𝓝 (leftLim (↑f : R → ℝ) a))

Tactic:
apply (f.mono.tendsto_leftLim a).comp

Premises used: StieltjesFunction.mono, Filter.Tendsto.comp, Monotone.tendsto_leftLim
-- 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
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 u atTop (𝓝[<] a)

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim
          (Eventually.of_forall fun n => u_lt_a n)

Premises used: Filter.Eventually.of_forall, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- 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
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 u atTop (𝓝[<] a)

Tactic:
exact
        tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim
          (Eventually.of_forall fun n => u_lt_a n)

Premises used: Filter.Eventually.of_forall, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- 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
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))

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)
-- 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
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∞)
this : Tendsto (fun (n : ℕ) ↦ (↑f : R → ℝ) (u n)) atTop (𝓝 (leftLim (↑f : R → ℝ) a))
⊢ Tendsto (fun (n : ℕ) ↦ ofReal ((↑f : R → ℝ) a - (↑f : R → ℝ) (u n))) atTop
    (𝓝 (ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)))

Tactic:
ENNReal.continuous_ofReal.continuousAt.tendsto.comp (tendsto_const_nhds.sub this)

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, tendsto_const_nhds, ENNReal.continuous_ofReal, WithTop.some, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp, Filter.Tendsto.sub
-- 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
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∞)
this : Tendsto (fun (n : ℕ) ↦ (↑f : R → ℝ) (u n)) atTop (𝓝 (leftLim (↑f : R → ℝ) a))
⊢ Tendsto (fun (n : ℕ) ↦ ofReal ((↑f : R → ℝ) a - (↑f : R → ℝ) (u n))) atTop
    (𝓝 (ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)))

Tactic:
exact ENNReal.continuous_ofReal.continuousAt.tendsto.comp (tendsto_const_nhds.sub this)

Premises used: tendsto_const_nhds, ENNReal.continuous_ofReal, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp, Filter.Tendsto.sub
-- 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
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)))

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)
-- 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
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∞)
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)))
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)

Tactic:
tendsto_nhds_unique L1 L2

Premises used: tendsto_nhds_unique
-- 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
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∞)
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)))
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {a} = ofReal ((↑f : R → ℝ) a - leftLim (↑f : R → ℝ) a)

Tactic:
exact tendsto_nhds_unique L1 L2

Premises used: tendsto_nhds_unique
-- 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
inl :
  ∀ (hab : a ≤ b),
    ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
inr :
  ∀ (hab : b < a),
    ((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)

Tactic:
rcases le_or_gt a b with (hab | hab)

Premises used: le_or_gt
-- 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
hab : a ≤ b
⊢ Disjoint {a} (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 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a ≤ b
⊢ Disjoint {a} (Ioc a b)

Tactic:
have A : Disjoint {a} (Ioc a b) := by simp