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 : PseudoMetrizableSpace Ω
inst_3 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
μs : ι → Measure Ω
h :
  ∀ {E : Set Ω},
    MeasurableSet E →
      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∞)
F : Set Ω
F_closed : IsClosed[inst_1] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h_1 : L.NeBot
ex :
  ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
rs : ℕ → ℝ :=
  Classical.choose (p := fun (x : ℕ → ℝ) ↦
    Tendsto x atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < x n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (x n) F)) : ℝ≥0∞) (0 : ℝ≥0∞))
    ex
rs_lim : Tendsto rs atTop (𝓝 0)
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
Fthicks_open : ∀ (n : ℕ), IsOpen[inst_1] (Metric.thickening (rs n) F)
key :
  ∀ (n : ℕ),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F) : ℝ≥0∞)) L
      (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F)) : Filter ℝ≥0∞)
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
keyB :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening r F) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
nhds :
  Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
    (Iio (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)))
⊢ (fun (r : ℝ) ↦ (μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening r F)) ⁻¹'
      Iio (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)) ∈
    map rs atTop

Tactic:
specialize rs_lim (keyB nhds)
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : PseudoMetrizableSpace Ω
inst_3 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
μs : ι → Measure Ω
h :
  ∀ {E : Set Ω},
    MeasurableSet E →
      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∞)
F : Set Ω
F_closed : IsClosed[inst_1] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h_1 : L.NeBot
ex :
  ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
rs : ℕ → ℝ :=
  Classical.choose (p := fun (x : ℕ → ℝ) ↦
    Tendsto x atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < x n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (x n) F)) : ℝ≥0∞) (0 : ℝ≥0∞))
    ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
Fthicks_open : ∀ (n : ℕ), IsOpen[inst_1] (Metric.thickening (rs n) F)
key :
  ∀ (n : ℕ),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F) : ℝ≥0∞)) L
      (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F)) : Filter ℝ≥0∞)
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
keyB :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening r F) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
nhds :
  Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
    (Iio (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)))
rs_lim :
  (fun (r : ℝ) ↦ (μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening r F)) ⁻¹'
      Iio (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)) ∈
    map rs atTop
⊢ ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b →
        (μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening (rs b) F) <
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
simp only [mem_map, mem_atTop_sets, ge_iff_le, mem_preimage, mem_Iio] at rs_lim

Premises used: Set.mem_Iio, ge_iff_le, Filter.mem_atTop_sets, Filter.mem_map, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : PseudoMetrizableSpace Ω
inst_3 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
μs : ι → Measure Ω
h :
  ∀ {E : Set Ω},
    MeasurableSet E →
      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∞)
F : Set Ω
F_closed : IsClosed[inst_1] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h_1 : L.NeBot
ex :
  ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
rs : ℕ → ℝ :=
  Classical.choose (p := fun (x : ℕ → ℝ) ↦
    Tendsto x atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < x n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (x n) F)) : ℝ≥0∞) (0 : ℝ≥0∞))
    ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
Fthicks_open : ∀ (n : ℕ), IsOpen[inst_1] (Metric.thickening (rs n) F)
key :
  ∀ (n : ℕ),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F) : ℝ≥0∞)) L
      (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F)) : Filter ℝ≥0∞)
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
keyB :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening r F) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
nhds :
  Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
    (Iio (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)))
rs_lim :
  ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b →
        (μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening (rs b) F) <
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
inr :
  ∀ (m : ℕ)
    (hm :
      ∀ (b : ℕ),
        m ≤ b →
          (μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening (rs b) F) <
            HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)),
    limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨m, hm⟩ := rs_lim
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : PseudoMetrizableSpace Ω
inst_3 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
μs : ι → Measure Ω
h :
  ∀ {E : Set Ω},
    MeasurableSet E →
      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∞)
F : Set Ω
F_closed : IsClosed[inst_1] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h_1 : L.NeBot
ex :
  ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
rs : ℕ → ℝ :=
  Classical.choose (p := fun (x : ℕ → ℝ) ↦
    Tendsto x atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < x n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (x n) F)) : ℝ≥0∞) (0 : ℝ≥0∞))
    ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
Fthicks_open : ∀ (n : ℕ), IsOpen[inst_1] (Metric.thickening (rs n) F)
key :
  ∀ (n : ℕ),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F) : ℝ≥0∞)) L
      (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F)) : Filter ℝ≥0∞)
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
keyB :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening r F) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
nhds :
  Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
    (Iio (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)))
m : ℕ
hm :
  ∀ (b : ℕ),
    m ≤ b →
      (μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening (rs b) F) <
        HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ L.EventuallyLE (β := ℝ≥0∞) (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) fun (i : ι) ↦
    (μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs m) F)

Tactic:
have aux : (fun i ↦ (μs i F)) ≤ᶠ[L] (fun i ↦ μs i (Metric.thickening (rs m) F)) :=
    .of_forall <| fun i ↦ measure_mono (Metric.self_subset_thickening (rs_pos m) F)
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : PseudoMetrizableSpace Ω
inst_3 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
μs : ι → Measure Ω
h :
  ∀ {E : Set Ω},
    MeasurableSet E →
      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∞)
F : Set Ω
F_closed : IsClosed[inst_1] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h_1 : L.NeBot
ex :
  ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
rs : ℕ → ℝ :=
  Classical.choose (p := fun (x : ℕ → ℝ) ↦
    Tendsto x atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < x n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (x n) F)) : ℝ≥0∞) (0 : ℝ≥0∞))
    ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
Fthicks_open : ∀ (n : ℕ), IsOpen[inst_1] (Metric.thickening (rs n) F)
key :
  ∀ (n : ℕ),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F) : ℝ≥0∞)) L
      (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F)) : Filter ℝ≥0∞)
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
keyB :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening r F) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
nhds :
  Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
    (Iio (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)))
m : ℕ
hm :
  ∀ (b : ℕ),
    m ≤ b →
      (μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening (rs b) F) <
        HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
aux :
  L.EventuallyLE (β := ℝ≥0∞) (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) fun (i : ι) ↦
    (μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs m) F)
⊢ limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
(limsup_le_limsup aux).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 : PseudoMetrizableSpace Ω
inst_3 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
μs : ι → Measure Ω
h :
  ∀ {E : Set Ω},
    MeasurableSet E →
      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∞)
F : Set Ω
F_closed : IsClosed[inst_1] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h_1 : L.NeBot
ex :
  ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
rs : ℕ → ℝ :=
  Classical.choose (p := fun (x : ℕ → ℝ) ↦
    Tendsto x atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < x n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (x n) F)) : ℝ≥0∞) (0 : ℝ≥0∞))
    ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
Fthicks_open : ∀ (n : ℕ), IsOpen[inst_1] (Metric.thickening (rs n) F)
key :
  ∀ (n : ℕ),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F) : ℝ≥0∞)) L
      (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F)) : Filter ℝ≥0∞)
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
keyB :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening r F) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
nhds :
  Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
    (Iio (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)))
m : ℕ
hm :
  ∀ (b : ℕ),
    m ≤ b →
      (μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening (rs b) F) <
        HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
aux :
  L.EventuallyLE (β := ℝ≥0∞) (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) fun (i : ι) ↦
    (μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs m) F)
inr :
  limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs m) F)) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
refine (limsup_le_limsup aux).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 : PseudoMetrizableSpace Ω
inst_3 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
μs : ι → Measure Ω
h :
  ∀ {E : Set Ω},
    MeasurableSet E →
      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∞)
F : Set Ω
F_closed : IsClosed[inst_1] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h_1 : L.NeBot
ex :
  ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
rs : ℕ → ℝ :=
  Classical.choose (p := fun (x : ℕ → ℝ) ↦
    Tendsto x atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < x n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (x n) F)) : ℝ≥0∞) (0 : ℝ≥0∞))
    ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
Fthicks_open : ∀ (n : ℕ), IsOpen[inst_1] (Metric.thickening (rs n) F)
key :
  ∀ (n : ℕ),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F) : ℝ≥0∞)) L
      (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F)) : Filter ℝ≥0∞)
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
keyB :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening r F) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
nhds :
  Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
    (Iio (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)))
m : ℕ
hm :
  ∀ (b : ℕ),
    m ≤ b →
      (μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening (rs b) F) <
        HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
aux :
  L.EventuallyLE (β := ℝ≥0∞) (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) fun (i : ι) ↦
    (μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs m) F)
inr :
  (μ : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs m) F) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs m) F)) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
rw [Tendsto.limsup_eq (key m)]

Premises used: Filter.Tendsto.limsup_eq
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : PseudoMetrizableSpace Ω
inst_3 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
μs : ι → Measure Ω
h :
  ∀ {E : Set Ω},
    MeasurableSet E →
      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∞)
F : Set Ω
F_closed : IsClosed[inst_1] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h_1 : L.NeBot
ex :
  ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
rs : ℕ → ℝ :=
  Classical.choose (p := fun (x : ℕ → ℝ) ↦
    Tendsto x atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < x n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (x n) F)) : ℝ≥0∞) (0 : ℝ≥0∞))
    ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
Fthicks_open : ∀ (n : ℕ), IsOpen[inst_1] (Metric.thickening (rs n) F)
key :
  ∀ (n : ℕ),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F) : ℝ≥0∞)) L
      (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs n) F)) : Filter ℝ≥0∞)
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
keyB :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening r F) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
nhds :
  Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
    (Iio (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)))
m : ℕ
hm :
  ∀ (b : ℕ),
    m ≤ b →
      (μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening (rs b) F) <
        HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
aux :
  L.EventuallyLE (β := ℝ≥0∞) (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) fun (i : ι) ↦
    (μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs m) F)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs m) F) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
apply (measure_mono (Metric.thickening_subset_cthickening (rs m) F)).trans (hm m rfl.le).le

Premises used: Metric.thickening_subset_cthickening, LT.lt.le, Eq.le, MeasureTheory.measure_mono, LE.le.trans, rfl
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : PseudoMetrizableSpace Ω
inst_3 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_4 : IsProbabilityMeasure μ
μs : ι → Measure Ω
inst_5 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ {E : Set Ω},
    MeasurableSet E →
      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∞)
G : Set Ω
G_open : IsOpen[inst_1] G
apply :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Gᶜ) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Gᶜ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)

Tactic:
apply le_measure_liminf_of_limsup_measure_compl_le G_open.measurableSet

Premises used: IsOpen.measurableSet, MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : PseudoMetrizableSpace Ω
inst_3 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_4 : IsProbabilityMeasure μ
μs : ι → Measure Ω
inst_5 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ {E : Set Ω},
    MeasurableSet E →
      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∞)
G : Set Ω
G_open : IsOpen[inst_1] G
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Gᶜ) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Gᶜ : ℝ≥0∞)

Tactic:
limsup_measure_closed_le_of_forall_tendsto_measure h _ (isClosed_compl_iff.mpr G_open)

Premises used: Iff.mpr, MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure, isClosed_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : PseudoMetrizableSpace Ω
inst_3 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_4 : IsProbabilityMeasure μ
μs : ι → Measure Ω
inst_5 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ {E : Set Ω},
    MeasurableSet E →
      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∞)
G : Set Ω
G_open : IsOpen[inst_1] G
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Gᶜ) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Gᶜ : ℝ≥0∞)

Tactic:
exact limsup_measure_closed_le_of_forall_tendsto_measure h _ (isClosed_compl_iff.mpr G_open)

Premises used: Iff.mpr, MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure, isClosed_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst_1, _] f
f_nn : 0 ≤ f
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) atTop : ℝ≥0∞)
simp_rw :
  ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a} ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (t : ℝ) in Ioi 0, (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop
⊢ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop

Tactic:
simp_rw [lintegral_eq_lintegral_meas_lt _ (Eventually.of_forall f_nn) f_cont.aemeasurable]

Premises used: Filter.Eventually.of_forall, Continuous.aemeasurable, MeasureTheory.lintegral_eq_lintegral_meas_lt