awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
M : ℕ
hM :
  ∀ b ≥ M,
    ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
key₂ :
  Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
room₂ :
  ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near :
  ∀ᶠ (a : ι) in L,
    ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs a) : Measure Ω) ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near' :
  ∀ᶠ (x : ι) in L,
    ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
inr :
  limsup (fun (x : ι) ↦ ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
apply (Filter.limsup_le_limsup ev_near').trans

Premises used: Filter.limsup_le_limsup, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
M : ℕ
hM :
  ∀ b ≥ M,
    ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
key₂ :
  Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
room₂ :
  ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near :
  ∀ᶠ (a : ι) in L,
    ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs a) : Measure Ω) ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near' :
  ∀ᶠ (x : ι) in L,
    ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
inr :
  ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2 ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ limsup (fun (x : ι) ↦ ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
rw [limsup_const]

Premises used: Filter.limsup_const
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
M : ℕ
hM :
  ∀ b ≥ M,
    ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
key₂ :
  Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
room₂ :
  ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near :
  ∀ᶠ (a : ι) in L,
    ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs a) : Measure Ω) ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near' :
  ∀ᶠ (x : ι) in L,
    ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
inr :
  HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2) + (↑ε : ℝ≥0∞) / 2 ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2 ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
apply le_trans (add_le_add (hM M rfl.le).le (le_refl (ε / 2 : ℝ≥0∞)))

Premises used: le_refl, ENNReal.ofNNReal, add_le_add, HDiv.hDiv, LT.lt.le, Eq.le, OfNat.ofNat, rfl, le_trans
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
M : ℕ
hM :
  ∀ b ≥ M,
    ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
key₂ :
  Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
room₂ :
  ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near :
  ∀ᶠ (a : ι) in L,
    ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs a) : Measure Ω) ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near' :
  ∀ᶠ (x : ι) in L,
    ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
⊢ HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2) + (↑ε : ℝ≥0∞) / 2 ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
simp only [add_assoc, ENNReal.add_halves, le_refl]

Premises used: le_refl, add_assoc, ENNReal.add_halves
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)

Tactic:
apply FiniteMeasure.limsup_measure_closed_le_of_tendsto
    ((tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds L).mp μs_lim) F_closed

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds, MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
G : Set Ω
G_open : IsOpen[inst_1] G
⊢ LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)

Tactic:
haveI h_closeds : ∀ F, IsClosed F → (L.limsup fun i ↦ (μs i : Measure Ω) F) ≤ (μ : Measure Ω) F :=
    fun _ F_closed ↦ limsup_measure_closed_le_of_tendsto μs_lim F_closed
  le_measure_liminf_of_limsup_measure_compl_le G_open.measurableSet
    (h_closeds _ (isClosed_compl_iff.mpr G_open))

Premises used: Iff.mpr, Compl.compl, IsOpen.measurableSet, MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto, MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le, isClosed_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (frontier E) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)

Tactic:
haveI h_opens : ∀ G, IsOpen G → (μ : Measure Ω) G ≤ L.liminf fun i ↦ (μs i : Measure Ω) G :=
    fun _ G_open ↦ le_liminf_measure_open_of_tendsto μs_lim G_open
  tendsto_measure_of_null_frontier h_opens E_nullbdry

Premises used: MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto, MeasureTheory.tendsto_measure_of_null_frontier
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) (frontier E) : ℝ≥0) (0 : ℝ≥0)
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (frontier E) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa using E_nullbdry
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) (frontier E) : ℝ≥0) (0 : ℝ≥0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)

Tactic:
have key := tendsto_measure_of_null_frontier_of_tendsto' μs_lim (by simpa using E_nullbdry)
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) (frontier E) : ℝ≥0) (0 : ℝ≥0)
key :
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0) E : ℝ≥0)) L (𝓝 ((μ : (a : Set Ω) → ℝ≥0) E) : Filter ℝ≥0)

Tactic:
(ENNReal.tendsto_toNNReal (measure_ne_top (↑μ) E)).comp key

Premises used: MeasureTheory.measure_ne_top, ENNReal.tendsto_toNNReal, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) (frontier E) : ℝ≥0) (0 : ℝ≥0)
key :
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0) E : ℝ≥0)) L (𝓝 ((μ : (a : Set Ω) → ℝ≥0) E) : Filter ℝ≥0)

Tactic:
exact (ENNReal.tendsto_toNNReal (measure_ne_top (↑μ) E)).comp key

Premises used: MeasureTheory.measure_ne_top, ENNReal.tendsto_toNNReal, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
hE : IsClopen E
⊢ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) (frontier E) : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp [hE]
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
⊢ ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))

Tactic:
have mbles : ∀ r : ℝ, MeasurableSet (frontier (Metric.thickening r s)) :=
    fun r ↦ isClosed_frontier.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
⊢ Pairwise (α := ℝ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set Ω) Disjoint fun (r : ℝ) ↦ frontier (Metric.thickening r s))

Tactic:
have disjs := Metric.frontier_thickening_disjoint s
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs :
  Pairwise (α := ℝ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set Ω) Disjoint fun (r : ℝ) ↦ frontier (Metric.thickening r s))
⊢ Set.Countable (α := ℝ)
    {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}

Tactic:
have key := Measure.countable_meas_pos_of_disjoint_iUnion (μ := μ) mbles disjs
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs :
  Pairwise (α := ℝ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set Ω) Disjoint fun (r : ℝ) ↦ frontier (Metric.thickening r s))
key :
  Set.Countable (α := ℝ)
    {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}
⊢ Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (Ioo a b \
          {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}) :
      ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞)

Tactic:
have aux := measure_diff_null (s := Ioo a b) (Set.Countable.measure_zero key volume)
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs :
  Pairwise (α := ℝ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set Ω) Disjoint fun (r : ℝ) ↦ frontier (Metric.thickening r s))
key :
  Set.Countable (α := ℝ)
    {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}
aux :
  Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (Ioo a b \
          {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}) :
      ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞)
⊢ 0 < ENNReal.ofReal (b - a)

Tactic:
simp only [hab, ENNReal.ofReal_pos, sub_pos]

Premises used: sub_pos, ENNReal.ofReal_pos
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs :
  Pairwise (α := ℝ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set Ω) Disjoint fun (r : ℝ) ↦ frontier (Metric.thickening r s))
key :
  Set.Countable (α := ℝ)
    {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}
aux :
  Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (Ioo a b \
          {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}) :
      ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞)
⊢ 0 < ENNReal.ofReal (b - a)

Tactic:
have len_pos : 0 < ENNReal.ofReal (b - a) := by simp only [hab, ENNReal.ofReal_pos, sub_pos]
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs :
  Pairwise (α := ℝ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set Ω) Disjoint fun (r : ℝ) ↦ frontier (Metric.thickening r s))
key :
  Set.Countable (α := ℝ)
    {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}
aux :
  Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (Ioo a b \
          {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}) :
      ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞)
len_pos : 0 < ENNReal.ofReal (b - a)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (Ioo a b \
          {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}) :
      ℝ≥0∞)

Tactic:
rw [← Real.volume_Ioo, ← aux] at len_pos

Premises used: Real.volume_Ioo
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs :
  Pairwise (α := ℝ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set Ω) Disjoint fun (r : ℝ) ↦ frontier (Metric.thickening r s))
key :
  Set.Countable (α := ℝ)
    {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}
aux :
  Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (Ioo a b \
          {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}) :
      ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞)
len_pos :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (Ioo a b \
          {i : ℝ | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening i s)) : ℝ≥0∞)}) :
      ℝ≥0∞)
⊢ ∃ r ∈ Ioo a b, Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [Set.Nonempty] using nonempty_of_measure_ne_zero len_pos.ne'

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, LT.lt.ne', Set.Nonempty
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
rcases :
  ∀ (Rs : ℕ → ℝ),
    StrictAnti Rs →
      ∀ (Rs_pos : ∀ (n : ℕ), 0 < Rs n) (Rs_lim : Tendsto Rs atTop (𝓝 0)),
        ∃ (rs : ℕ → ℝ),
          Tendsto rs atTop (𝓝 0) ∧
            ∀ (n : ℕ),
              0 < rs n ∧
                Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) s)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) s)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases exists_seq_strictAnti_tendsto (0 : ℝ) with ⟨Rs, ⟨_, ⟨Rs_pos, Rs_lim⟩⟩⟩

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
Rs : ℕ → ℝ
left : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
⊢ ∀ (n : ℕ),
    ∃ r ∈ Ioo 0 (Rs n), Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have obs := fun n : ℕ => exists_null_frontier_thickening μ s (Rs_pos n)
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
Rs : ℕ → ℝ
left : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
obs :
  ∀ (n : ℕ),
    ∃ r ∈ Ioo 0 (Rs n), Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) s)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨fun n : ℕ => (obs n).choose, ⟨?_, ?_⟩⟩

Premises used: And.intro, Exists.intro, Exists.choose