-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem measure_singleton (a : ℝ) : f.measure {a} = ofReal (f a - leftLim f a)

Proof state:
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

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

Result:
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}

Proof state:
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 => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))

Tactic:
rw [A]

Result:
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 => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure (⋂ n, Ioc (u n) a)))

Proof state:
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 => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {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)))

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

Result:
no goals

Proof state:
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 => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))
⊢ Tendsto (fun n => ↑f (u n)) atTop (𝓝 (leftLim (↑f) a))

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

Result:
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 => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))
⊢ Tendsto u atTop (𝓝[<] a)

Proof state:
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)
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) 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 => ?_
  simp? at hx says simp only [mem_iInter, mem_Ioc] at hx
  have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le
  simp [le_antisymm this (hx 0).2]

Result:
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
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)

Proof state:
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

Tactic:
simp [mem_singleton_iff.1 hx, u_lt_a]

Result:
no goals

Proof state:
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 => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))
L2 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)

Tactic:
exact tendsto_nhds_unique L1 L2

Result:
no goals

Proof state:
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 => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure (⋂ n, Ioc (u n) a)))

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

Result:
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, f.measure (Ioc (u i) a) ≠ ⊤

Proof state:
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
⊢ f.measure (Ioc (u 0) a) ≠ ⊤

Tactic:
simpa only [measure_Ioc] using ENNReal.ofReal_ne_top

Result:
no goals

Proof state:
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, f.measure (Ioc (u i) a) ≠ ⊤

Tactic:
exact ⟨0, by simpa only [measure_Ioc] using ENNReal.ofReal_ne_top⟩

Result:
no goals

Proof state:
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

Tactic:
exact Ioc_subset_Ioc_left (u_mono.monotone hmn)

Result:
no goals

Proof state:
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}

Tactic:
simp? at hx says simp only [mem_iInter, mem_Ioc] at hx

Result:
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}

Proof state:
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}

Tactic:
simp only [mem_iInter, mem_Ioc] at hx

Result:
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}

Proof state:
f : StieltjesFunction
a : ℝ
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)

Tactic:
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

Result:
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)
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)

Proof state:
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 => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))
⊢ Tendsto (fun n => ofReal (↑f a - ↑f (u n))) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) 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)

Result:
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 => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {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)))

Proof state:
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}

Tactic:
have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le

Result:
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}