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 : 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 : (a : Set Ω) → ℝ≥0) E : ℝ≥0)) L (𝓝 ((μ : (a : Set Ω) → ℝ≥0) E) : Filter ℝ≥0)
have key : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
⊢ ∃ r ∈ Ioo a b, Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)
have mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
Tactic: have mbles : ∀ r : ℝ, MeasurableSet (frontier (Metric.thickening r s)) :=
    fun r ↦ isClosed_frontier.measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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))
⊢ ∃ r ∈ Ioo a b, Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)
have disjs : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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))
⊢ ∃ r ∈ Ioo a b, Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)
have key : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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∞)}
⊢ ∃ r ∈ Ioo a b, Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: have aux := measure_diff_null (s := Ioo a b) (Set.Countable.measure_zero key volume)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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∞)
⊢ ∃ r ∈ Ioo a b, Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)
have len_pos : 0 < ENNReal.ofReal (b - a)
Tactic: have len_pos : 0 < ENNReal.ofReal (b - a) := by simp only [hab, ENNReal.ofReal_pos, sub_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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)
⊢ ∃ r ∈ Ioo a b, Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: rw [← Real.volume_Ioo, ← aux] at len_pos
Cleared hypotheses: len_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : SFinite μ
s : Set Ω
⊢ ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) s)) : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: rcases exists_seq_strictAnti_tendsto (0 : ℝ) with ⟨Rs, ⟨_, ⟨Rs_pos, Rs_lim⟩⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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)
⊢ ∃ (rs : ℕ → ℝ),
    Tendsto rs atTop (𝓝 0) ∧
      ∀ (n : ℕ),
        0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) s)) : ℝ≥0∞) (0 : ℝ≥0∞)
have obs : ∀ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
have refine_1 : Tendsto (β := ℝ)
  (fun (n : ℕ) ↦
    sorry.choose (p := fun (r : ℝ) ↦
      r ∈ Ioo 0 (Rs n) ∧
        Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)))
  atTop (𝓝 0)
Tactic: refine ⟨fun n : ℕ => (obs n).choose, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
refine_1 :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      ⋯.choose (p := fun (r : ℝ) ↦
        r ∈ Ioo 0 (Rs n) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)))
    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∞)
have refine_2 : ∀ (n : ℕ),
  LT.lt (α := ℝ) 0
      ((fun (n : ℕ) ↦
          sorry.choose (p := fun (r : ℝ) ↦
            r ∈ Ioo 0 (Rs n) ∧
              Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)))
        n) ∧
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞)
          (frontier
            (Metric.thickening
              ((fun (n : ℕ) ↦
                  sorry.choose (p := fun (r : ℝ) ↦
                    r ∈ Ioo 0 (Rs n) ∧
                      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening r s)) : ℝ≥0∞) (0 : ℝ≥0∞)))
                n)
              s)) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
Tactic: refine ⟨fun n : ℕ => (obs n).choose, ⟨?_, ?_⟩⟩
-- 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 Ω
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have inl : ∀
  (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∞)) ⊥
            (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) ⊥ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
Tactic: rcases L.eq_or_neBot with rfl | _
Cleared hypotheses: L, h
-- 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 Ω
inl :
  ∀
    (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∞)) ⊥
              (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) ⊥ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have inr : L.NeBot →
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
Tactic: rcases L.eq_or_neBot with rfl | _
-- 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
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have ex : ∃ (rs : ℕ → ℝ),
  Tendsto rs atTop (𝓝 0) ∧
    ∀ (n : ℕ),
      0 < rs n ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have ex := exists_null_frontiers_thickening μ F
-- 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
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have rs_lim : Tendsto rs atTop (𝓝 0)
Tactic: have rs_lim : Tendsto rs atTop (𝓝 0) := (Classical.choose_spec ex).1
-- 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)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have rs_pos : ∀ (n : ℕ), 0 < rs n
Tactic: have rs_pos : ∀ n, 0 < rs n := fun n ↦ ((Classical.choose_spec ex).2 n).1
-- 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
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have rs_null : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (frontier (Metric.thickening (rs n) F)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have rs_null : ∀ n, μ (frontier (Metric.thickening (rs n) F)) = 0 :=
    fun n ↦ ((Classical.choose_spec ex).2 n).2
-- 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∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have Fthicks_open : ∀ (n : ℕ), IsOpen[inst_1] (Metric.thickening (rs n) F)
Tactic: have Fthicks_open : ∀ n, IsOpen (Metric.thickening (rs n) F) :=
    fun n ↦ Metric.isOpen_thickening
-- 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)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have 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∞)
Tactic: have key := fun (n : ℕ) ↦ h (Fthicks_open n).measurableSet (rs_null n)
-- 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_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∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have inr : ∀ (ε : ℝ≥0),
  0 < ε →
    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∞)
Tactic: apply ENNReal.le_of_forall_pos_le_add