awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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∞)
⊢ limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have keyB : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0∞) (Metric.cthickening r F) : ℝ≥0∞)) (𝓝 0)
  (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
Tactic: have keyB := tendsto_measure_cthickening_of_isClosed (μ := μ) (s := F)
                ⟨1, ⟨by simp only [gt_iff_lt, zero_lt_one], measure_ne_top _ _⟩⟩ F_closed
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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∞)
⊢ limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have nhds : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
  (Iio (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)))
Tactic: have nhds : Iio (μ F + ε) ∈ 𝓝 (μ F) :=
    Iio_mem_nhds <| ENNReal.lt_add_right μF_finite.ne (ENNReal.coe_pos.mpr ε_pos).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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∞)))
⊢ limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have rs_lim₁ : (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)
Cleared hypotheses: rs_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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
⊢ limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have rs_lim₁ : ∃ (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
Cleared hypotheses: rs_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
⊢ limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have 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∞)
Tactic: obtain ⟨m, hm⟩ := rs_lim
Cleared hypotheses: rs_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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∞)
⊢ limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have aux : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
have inr : limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs m) F)) L ≤
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
Tactic: refine (limsup_le_limsup aux).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞) (Metric.thickening (rs m) F)) L ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have inr : (μ : (a : Set Ω) → ℝ≥0∞) (Metric.thickening (rs m) F) ≤
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
Tactic: rw [Tendsto.limsup_eq (key m)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Gᶜ) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Gᶜ : ℝ≥0∞)
Tactic: apply le_measure_liminf_of_limsup_measure_compl_le G_open.measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
⊢ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
have 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
Tactic: simp_rw [lintegral_eq_lintegral_meas_lt _ (Eventually.of_forall f_nn) f_cont.aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
⊢ ∫⁻ (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
have calc_1 : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a} ≤
  ∫⁻ (t : ℝ) in Ioi 0, liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop
Tactic: calc ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a}
      ≤ ∫⁻ (t : ℝ) in Set.Ioi 0, atTop.liminf (fun i ↦ (μs i) {a | t < f a}) := ?_ -- (i)
    _ ≤ atTop.liminf (fun i ↦ ∫⁻ (t : ℝ) in Set.Ioi 0, (μs i) {a | t < f a}) := ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
calc_1 :
  ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a} ≤
    ∫⁻ (t : ℝ) in Ioi 0, liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop
⊢ ∫⁻ (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
have calc_2 : ∫⁻ (t : ℝ) in Ioi 0, liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop ≤
  liminf (fun (i : ℕ) ↦ ∫⁻ (t : ℝ) in Ioi 0, (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop
Tactic: calc ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a}
      ≤ ∫⁻ (t : ℝ) in Set.Ioi 0, atTop.liminf (fun i ↦ (μs i) {a | t < f a}) := ?_ -- (i)
    _ ≤ atTop.liminf (fun i ↦ ∫⁻ (t : ℝ) in Set.Ioi 0, (μs i) {a | t < f a}) := ?_