awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[inst_1] G
h_opens :
  LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop : ℝ≥0)
refine_1 : ContinuousAt ENNReal.ofNNReal (liminf (fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) G) atTop)
refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) atTop fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) G
⊢ (↑(liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop) : ℝ≥0∞) =
    liminf (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop
have refine_3 : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) atTop fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) G
Tactic: refine Monotone.map_liminf_of_continuousAt (F := atTop) ENNReal.coe_mono (μs · G) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[inst_1] G
h_opens :
  LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop : ℝ≥0)
⊢ LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
    (liminf (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
have aux : (↑(liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop) : ℝ≥0∞) =
  liminf (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop
Tactic: have aux : ENNReal.ofNNReal (liminf (fun i ↦ μs i G) atTop) =
          liminf (ENNReal.ofNNReal ∘ fun i ↦ μs i G) atTop := by
    refine Monotone.map_liminf_of_continuousAt (F := atTop) ENNReal.coe_mono (μs · G) ?_ ?_ ?_
    · exact ENNReal.continuous_coe.continuousAt
    · exact IsBoundedUnder.isCoboundedUnder_ge ⟨1, by simp⟩
    · exact ⟨0, by simp⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[inst_1] G
h_opens :
  LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop : ℝ≥0)
aux :
  (↑(liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop) : ℝ≥0∞) =
    liminf (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop
⊢ LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
    (liminf (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
have obs : (↑((μ : (a : Set Ω) → ℝ≥0) G) : ℝ≥0∞) ≤ (↑(liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop) : ℝ≥0∞)
Tactic: have obs := ENNReal.coe_mono h_opens
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[inst_1] G
h_opens :
  LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop : ℝ≥0)
aux :
  (↑(liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop) : ℝ≥0∞) =
    liminf (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop
obs : (↑((μ : (a : Set Ω) → ℝ≥0) G) : ℝ≥0∞) ≤ (↑(liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
    (liminf (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
have obs₁ : ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G ≤
  liminf (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop
Tactic: simp only [ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, aux] at obs
Cleared hypotheses: obs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[inst_1] G
h_opens :
  LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop : ℝ≥0)
aux :
  (↑(liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop) : ℝ≥0∞) =
    liminf (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop
obs :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G ≤
    liminf (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop
⊢ LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
    (liminf (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
have h : ∀ (x : ℕ),
  ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G = (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) x
Tactic: convert! obs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_3 : L.IsCountablyGenerated
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)
⊢ Tendsto (fun (i : ι) ↦ μs i) L (𝓝 μ)
have apply : ∀ (u : ℕ → ι) (hu : Tendsto u atTop L), Tendsto ((fun (i : ι) ↦ μs i) ∘ u) atTop (𝓝 μ)
Tactic: apply Filter.tendsto_of_seq_tendsto fun u hu ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_3 : L.IsCountablyGenerated
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)
u : ℕ → ι
hu : Tendsto u atTop L
⊢ Tendsto ((fun (i : ι) ↦ μs i) ∘ u) atTop (𝓝 μ)
have apply : ∀ (G : Set Ω) (hG : IsOpen[inst_1] G),
  LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
    (liminf (fun (i : ℕ) ↦ (((↑(((fun (i : ι) ↦ μs i) ∘ u) i) : Measure Ω) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) atTop :
      ℝ≥0∞)
Tactic: apply tendsto_of_forall_isOpen_le_liminf_nat' fun G hG ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_3 : L.IsCountablyGenerated
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)
⊢ Tendsto (fun (i : ι) ↦ μs i) L (𝓝 μ)
have apply : ∀ (u : ℕ → ι) (hu : Tendsto u atTop L), Tendsto ((fun (i : ι) ↦ μs i) ∘ u) atTop (𝓝 μ)
Tactic: apply Filter.tendsto_of_seq_tendsto fun u hu ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_3 : L.IsCountablyGenerated
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)
u : ℕ → ι
hu : Tendsto u atTop L
⊢ Tendsto ((fun (i : ι) ↦ μs i) ∘ u) atTop (𝓝 μ)
have apply : ∀ (G : Set Ω) (hG : IsOpen[inst_1] G),
  LE.le (α := ℝ≥0) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) L)
    (liminf (fun (i : ℕ) ↦ ((((fun (i : ι) ↦ μs i) ∘ u) i : ProbabilityMeasure Ω) : (a : Set Ω) → ℝ≥0) G) atTop)
Tactic: apply tendsto_of_forall_isOpen_le_liminf_nat fun G hG ↦ (h_opens G hG).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_3 : L.IsCountablyGenerated
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)
u : ℕ → ι
hu : Tendsto u atTop L
G : Set Ω
hG : IsOpen[inst_1] G
⊢ LE.le (α := ℝ≥0) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) L)
    (liminf (fun (i : ℕ) ↦ ((((fun (i : ι) ↦ μs i) ∘ u) i : ProbabilityMeasure Ω) : (a : Set Ω) → ℝ≥0) G) atTop)
have change : LE.le (α := ℝ≥0) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) L)
  (liminf ((fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) ∘ u) atTop)
Tactic: change _ ≤ atTop.liminf ((fun i ↦ μs i G) ∘ u)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_3 : L.IsCountablyGenerated
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)
u : ℕ → ι
hu : Tendsto u atTop L
G : Set Ω
hG : IsOpen[inst_1] G
⊢ LE.le (α := ℝ≥0) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) L)
    (liminf ((fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) ∘ u) atTop)
have rw : LE.le (α := ℝ≥0) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) L)
  (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) (map u atTop))
Tactic: rw [liminf_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_3 : L.IsCountablyGenerated
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)
u : ℕ → ι
hu : Tendsto u atTop L
G : Set Ω
hG : IsOpen[inst_1] G
⊢ LE.le (α := ℝ≥0) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) L)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) (map u atTop))
have refine : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) (map u atTop) fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G
Tactic: refine liminf_le_liminf_of_le hu (by isBoundedDefault) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : TopologicalSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_2 : L.IsCountablyGenerated
h :
  ∀ (F : Set Ω),
    IsClosed[inst] F →
      LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
        (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
⊢ Tendsto μs L (𝓝 μ)
have refine : ∀ (G : Set Ω),
  IsOpen[inst] G →
    LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
      (liminf (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)
Tactic: refine tendsto_of_forall_isOpen_le_liminf' ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : TopologicalSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
h :
  ∀ (F : Set Ω),
    IsClosed[inst] F →
      LE.le (α := ℝ≥0) (limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop : ℝ≥0)
        ((μ : (a : Set Ω) → ℝ≥0) F : ℝ≥0)
⊢ Tendsto μs atTop (𝓝 μ)
have refine : ∀ (F : Set Ω) (hF_closed : IsClosed[inst] F),
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) atTop : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
Tactic: refine tendsto_of_forall_isClosed_limsup_le' fun F hF_closed ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : TopologicalSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
h :
  ∀ (F : Set Ω),
    IsClosed[inst] F →
      LE.le (α := ℝ≥0) (limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop : ℝ≥0)
        ((μ : (a : Set Ω) → ℝ≥0) F : ℝ≥0)
F : Set Ω
hF_closed : IsClosed[inst] F
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) atTop : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have h₁ : LE.le (α := ℝ≥0) (limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) F : ℝ≥0)
Tactic: specialize h F hF_closed
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : TopologicalSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
F : Set Ω
hF_closed : IsClosed[inst] F
h : LE.le (α := ℝ≥0) (limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) F : ℝ≥0)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) atTop : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have aux : (↑(limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop) : ℝ≥0∞) =
  limsup (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop
Tactic: have aux : ENNReal.ofNNReal (limsup (fun i ↦ μs i F) atTop) =
      limsup (ENNReal.ofNNReal ∘ fun i ↦ μs i F) atTop :=
    Monotone.map_limsup_of_continuousAt (F := atTop) ENNReal.coe_mono (μs · F) (by fun_prop)
      ⟨1, by simp⟩ ⟨0, by simp⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : TopologicalSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
F : Set Ω
hF_closed : IsClosed[inst] F
h : LE.le (α := ℝ≥0) (limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) F : ℝ≥0)
aux :
  (↑(limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop) : ℝ≥0∞) =
    limsup (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) atTop : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have obs : (↑(limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop) : ℝ≥0∞) ≤ (↑((μ : (a : Set Ω) → ℝ≥0) F) : ℝ≥0∞)
Tactic: have obs := ENNReal.coe_mono h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : TopologicalSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
F : Set Ω
hF_closed : IsClosed[inst] F
h : LE.le (α := ℝ≥0) (limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) F : ℝ≥0)
aux :
  (↑(limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop) : ℝ≥0∞) =
    limsup (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop
obs : (↑(limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop) : ℝ≥0∞) ≤ (↑((μ : (a : Set Ω) → ℝ≥0) F) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) atTop : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have obs₁ : limsup (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop ≤
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F
Tactic: simp only [ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, aux] at obs
Cleared hypotheses: obs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : TopologicalSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
F : Set Ω
hF_closed : IsClosed[inst] F
h : LE.le (α := ℝ≥0) (limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) F : ℝ≥0)
aux :
  (↑(limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop) : ℝ≥0∞) =
    limsup (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop
obs :
  limsup (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop ≤
    ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) atTop : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have h₁ : ∀ (x : ℕ),
  ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F = (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) x
Tactic: convert! obs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : TopologicalSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_2 : L.IsCountablyGenerated
h :
  ∀ (F : Set Ω),
    IsClosed[inst] F →
      LE.le (α := ℝ≥0) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) L : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) F : ℝ≥0)
⊢ Tendsto μs L (𝓝 μ)
have apply : ∀ (u : ℕ → ι) (hu : Tendsto u atTop L), Tendsto (μs ∘ u) atTop (𝓝 μ)
Tactic: apply Filter.tendsto_of_seq_tendsto fun u hu ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : TopologicalSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_2 : L.IsCountablyGenerated
h :
  ∀ (F : Set Ω),
    IsClosed[inst] F →
      LE.le (α := ℝ≥0) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) L : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) F : ℝ≥0)
u : ℕ → ι
hu : Tendsto u atTop L
⊢ Tendsto (μs ∘ u) atTop (𝓝 μ)
have apply : ∀ (F : Set Ω) (hF : IsClosed[inst] F),
  LE.le (α := ℝ≥0) (limsup (fun (i : ℕ) ↦ ((μs ∘ u) i : (a : Set Ω) → ℝ≥0) F) atTop)
    (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) L)
Tactic: apply tendsto_of_forall_isClosed_limsup_le_nat fun F hF ↦ le_trans ?_ (h F hF)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω → ℝ),
      (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
        (∃ (L : ℝ≥0), LipschitzWith L f) →
          Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F
            (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
have mp : Tendsto μs F (𝓝 μ) →
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
mp :
  Tendsto μs F (𝓝 μ) →
    ∀ (f : Ω → ℝ),
      (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
        (∃ (L : ℝ≥0), LipschitzWith L f) →
          Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F
            (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω → ℝ),
      (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
        (∃ (L : ℝ≥0), LipschitzWith L f) →
          Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F
            (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
have mpr : (∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F
          (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))) →
  Tendsto μs F (𝓝 μ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
h : Tendsto μs F (𝓝 μ)
f : Ω → ℝ
hf_bounded : ∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C
hf_lip : ∃ (L : ℝ≥0), LipschitzWith L f
⊢ Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
have h₁ : ∀ (f : Ω →ᵇ ℝ),
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑μ : Measure Ω)))
Tactic: simp_rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ (∀ (f : Ω → ℝ),
      (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
        (∃ (L : ℝ≥0), LipschitzWith L f) →
          Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F
            (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))) →
    Tendsto μs F (𝓝 μ)
have mpr : ∀ [IsCountablyGenerated.{u_1} (α := γ) ⊥],
  (∀ (f : Ω → ℝ),
      (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
        (∃ (L : ℝ≥0), LipschitzWith L f) →
          Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) ⊥
            (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))) →
    Tendsto μs ⊥ (𝓝 μ)
Tactic: rcases F.eq_or_neBot with rfl | hne
Cleared hypotheses: F, inst_2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
mpr :
  ∀ [IsCountablyGenerated.{u_1} (α := γ) ⊥],
    (∀ (f : Ω → ℝ),
        (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
          (∃ (L : ℝ≥0), LipschitzWith L f) →
            Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) ⊥
              (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))) →
      Tendsto μs ⊥ (𝓝 μ)
⊢ (∀ (f : Ω → ℝ),
      (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
        (∃ (L : ℝ≥0), LipschitzWith L f) →
          Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F
            (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))) →
    Tendsto μs F (𝓝 μ)
have mpr₁ : ∀ (hne : F.NeBot),
  (∀ (f : Ω → ℝ),
      (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
        (∃ (L : ℝ≥0), LipschitzWith L f) →
          Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F
            (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))) →
    Tendsto μs F (𝓝 μ)
Tactic: rcases F.eq_or_neBot with rfl | hne