case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
f : StieltjesFunction
a : ℝ
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
obtain ⟨u, u_mono, u_lt_a, u_lim⟩ :
  ∃ u : ℕ → ℝ, StrictMono u ∧ (∀ n : ℕ, u n < a) ∧ Tendsto u atTop (𝓝 a) :=
  exists_seq_strictMono_tendsto a
case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
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 => _
  simp at hx
  have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le
  simp [le_antisymm this (hx 0).2]
case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
L2 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
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)
no goals
case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
L2 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
exact tendsto_nhds_unique L1 L2
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : x ∈ ⋂ (n : ℕ), Ioc (u n) a
⊢ x ∈ {a}
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
⊢ {a} = ⋂ (n : ℕ), Ioc (u n) a
refine' Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => _
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
⊢ x ∈ {a}
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : x ∈ ⋂ (n : ℕ), Ioc (u n) a
⊢ x ∈ {a}
simp at hx
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
this : a ≤ x
⊢ x ∈ {a}
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
⊢ x ∈ {a}
have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le
no goals
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
this : a ≤ x
⊢ x ∈ {a}
simp [le_antisymm this (hx 0).2]
no goals
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : x ∈ {a}
⊢ x ∈ ⋂ (n : ℕ), Ioc (u n) a
simp [mem_singleton_iff.1 hx, u_lt_a]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop
    (𝓝 (↑↑(StieltjesFunction.measure f) (⋂ (n : ℕ), Ioc (u n) a)))
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
rw [A]
case refine'_1
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
m n : ℕ
hmn : m ≤ n
⊢ Ioc (u n) a ≤ Ioc (u m) a

case refine'_2
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ ∃ i, ↑↑(StieltjesFunction.measure f) (Ioc (u i) a) ≠ ⊤
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop
    (𝓝 (↑↑(StieltjesFunction.measure f) (⋂ (n : ℕ), Ioc (u n) a)))
refine' tendsto_measure_iInter (fun n => measurableSet_Ioc) (fun m n hmn => _) _
no goals
case refine'_1
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
m n : ℕ
hmn : m ≤ n
⊢ Ioc (u n) a ≤ Ioc (u m) a
exact Ioc_subset_Ioc (u_mono.monotone hmn) le_rfl
no goals
case refine'_2
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ ∃ i, ↑↑(StieltjesFunction.measure f) (Ioc (u i) a) ≠ ⊤
exact ⟨0, by simpa only [measure_Ioc] using ENNReal.ofReal_ne_top⟩
no goals
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ ↑↑(StieltjesFunction.measure f) (Ioc (u 0) a) ≠ ⊤
simpa only [measure_Ioc] using ENNReal.ofReal_ne_top
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ Tendsto (fun n => ofReal (↑f a - ↑f (u n))) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
simp only [measure_Ioc]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
this : Tendsto (fun n => ↑f (u n)) atTop (𝓝 (leftLim (↑f) a))
⊢ Tendsto (fun n => ofReal (↑f a - ↑f (u n))) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ Tendsto (fun n => ofReal (↑f a - ↑f (u n))) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
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)
no goals
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
this : Tendsto (fun n => ↑f (u n)) atTop (𝓝 (leftLim (↑f) a))
⊢ Tendsto (fun n => ofReal (↑f a - ↑f (u n))) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
exact ENNReal.continuous_ofReal.continuousAt.tendsto.comp (tendsto_const_nhds.sub this)
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ Tendsto (fun n => u n) atTop (𝓝[Iio a] a)
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ Tendsto (fun n => ↑f (u n)) atTop (𝓝 (leftLim (↑f) a))
apply (f.mono.tendsto_leftLim a).comp
no goals
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ Tendsto (fun n => u n) atTop (𝓝[Iio a] a)
exact
  tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim
    (eventually_of_forall fun n => u_lt_a n)