awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
E₀_ae_eq_E : E₀ =ᶠ[ae μ] E
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)

Tactic:
measure_congr E₀_ae_eq_E.symm

Premises used: MeasureTheory.measure_congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
E₀_ae_eq_E : E₀ =ᶠ[ae μ] E
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)

Tactic:
h_E₀
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
E₀_ae_eq_E : E₀ =ᶠ[ae μ] E
⊢ LE.le (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L)

Tactic:
liminf_le_liminf (.of_forall fun _ ↦ measure_mono E₀_subset)

Premises used: Filter.Eventually.of_forall, MeasureTheory.measure_mono, Filter.liminf_le_liminf
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
E₀_ae_eq_E : E₀ =ᶠ[ae μ] E
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)

Tactic:
calc
      μ E = μ E₀ := measure_congr E₀_ae_eq_E.symm
      _ ≤ L.liminf fun i ↦ μs i E₀ := h_E₀
      _ ≤ L.liminf fun i ↦ μs i E :=
        liminf_le_liminf (.of_forall fun _ ↦ measure_mono E₀_subset)

Premises used: MeasureTheory.measure_congr, Filter.liminf, Filter.Eventually.of_forall, MeasureTheory.measure_mono, Filter.liminf_le_liminf, DFunLike.coe, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
⊢ E =ᶠ[ae μ] E₁

Tactic:
have E_ae_eq_E₁ : E =ᵐ[μ] E₁ :=
      EventuallyLE.antisymm subset_E₁.eventuallyLE
        ((ae_le_set.mpr nulldiff).trans E₀_subset.eventuallyLE)
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
E_ae_eq_E₁ : E =ᶠ[ae μ] E₁
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L)
    (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L)

Tactic:
limsup_le_limsup (.of_forall fun _ ↦ measure_mono subset_E₁)

Premises used: Filter.Eventually.of_forall, MeasureTheory.measure_mono, Filter.limsup_le_limsup
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
E_ae_eq_E₁ : E =ᶠ[ae μ] E₁
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)

Tactic:
h_E₁
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
E_ae_eq_E₁ : E =ᶠ[ae μ] E₁
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
measure_congr E_ae_eq_E₁.symm

Premises used: MeasureTheory.measure_congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
E_ae_eq_E₁ : E =ᶠ[ae μ] E₁
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
calc
      (L.limsup fun i ↦ μs i E) ≤ L.limsup fun i ↦ μs i E₁ :=
        limsup_le_limsup (.of_forall fun _ ↦ measure_mono subset_E₁)
      _ ≤ μ E₁ := h_E₁
      _ = μ E := measure_congr E_ae_eq_E₁.symm

Premises used: MeasureTheory.measure_congr, Filter.Eventually.of_forall, Filter.limsup, MeasureTheory.measure_mono, Filter.limsup_le_limsup, DFunLike.coe, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)
E : Set Ω
E_nullbdry : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier E) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)

Tactic:
haveI h_closeds : ∀ F, IsClosed F → (L.limsup fun i ↦ μs i F) ≤ μ F :=
    limsup_measure_closed_le_iff_liminf_measure_open_ge.mpr h_opens
  tendsto_measure_of_le_liminf_measure_of_limsup_measure_le interior_subset subset_closure
    E_nullbdry (h_opens _ isOpen_interior) (h_closeds _ isClosed_closure)

Premises used: Iff.mpr, interior_subset, subset_closure, isOpen_interior, MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge, closure, interior, MeasureTheory.tendsto_measure_of_le_liminf_measure_of_limsup_measure_le, isClosed_closure
-- 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
inl :
  ∀ (μs_lim : Tendsto μs ⊥ (𝓝 μ)),
    LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) ⊥ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
inr :
  ∀ (hne : L.NeBot),
    LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)

Tactic:
rcases L.eq_or_neBot with rfl | hne

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

Tactic:
simp only [limsup_bot, bot_le]

Premises used: Filter.limsup_bot, bot_le
-- 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
inr :
  ∀ (ε : ℝ≥0),
    0 < ε →
      LT.lt (α := ℝ≥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∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)

Tactic:
apply ENNReal.le_of_forall_pos_le_add

Premises used: ENNReal.le_of_forall_pos_le_add
-- 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 < ε
inr :
  LT.lt (α := ℝ≥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∞)
⊢ LT.lt (α := ℝ≥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:
_
-- 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∞)
⊢ (↑ε : ℝ≥0∞) / 2 ≠ 0

Tactic:
have ε_pos' := (ENNReal.half_pos (ENNReal.coe_ne_zero.mpr ε_pos.ne.symm)).ne.symm
-- 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)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)

Tactic:
have key₁ : Tendsto (fun n ↦ ∫⁻ ω, (fs n ω : ℝ≥0∞) ∂μ) atTop (𝓝 ((μ : Measure Ω) F)) :=
    HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed (μ : Measure Ω)
-- 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∞)
⊢ ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)

Tactic:
have room₁ : (μ : Measure Ω) F < (μ : Measure Ω) F + ε / 2 :=
    ENNReal.lt_add_right (measure_lt_top (μ : Measure Ω) F).ne ε_pos'
-- 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)
inr :
  ∀ (M : ℕ)
    (hM :
      ∀ b ≥ M,
        ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
          HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)),
    limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) 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:
obtain ⟨M, hM⟩ := eventually_atTop.mp <| key₁.eventually_lt_const room₁

Premises used: Filter.Tendsto.eventually_lt_const, Iff.mp, Filter.eventually_atTop
-- 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)
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))

Tactic:
have key₂ := FiniteMeasure.tendsto_iff_forall_lintegral_tendsto.mp μs_lim (fs M)
-- 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 Ω)))
⊢ ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2

Tactic:
have room₂ :
    (lintegral (μ : Measure Ω) fun a ↦ fs M a) <
      (lintegral (μ : Measure Ω) fun a ↦ fs M a) + ε / 2 :=
    ENNReal.lt_add_right (ne_of_lt ((fs M).lintegral_lt_top_of_nnreal _)) ε_pos'
-- 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
⊢ ∀ᶠ (a : ι) in L,
    ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs a) : Measure Ω) ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2

Tactic:
have ev_near := key₂.eventually_le_const room₂
-- 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
⊢ ∀ᶠ (x : ι) in L,
    ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2

Tactic:
have ev_near' := ev_near.mono
    (fun n ↦ le_trans (HasOuterApproxClosed.measure_le_lintegral F_closed (μs n) M))