awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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∞)
apply : ∀ (u : ℕ → ι) (hu : Tendsto u atTop L), Tendsto ((fun (i : ι) ↦ μs i) ∘ u) atTop (𝓝 μ)
⊢ Tendsto (fun (i : ι) ↦ μs i) L (𝓝 μ)

Tactic:
apply Filter.tendsto_of_seq_tendsto fun u hu ↦ ?_

Premises used: Filter.tendsto_of_seq_tendsto
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
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∞)
⊢ Tendsto ((fun (i : ι) ↦ μs i) ∘ u) atTop (𝓝 μ)

Tactic:
apply tendsto_of_forall_isOpen_le_liminf_nat' fun G hG ↦ ?_

Premises used: MeasureTheory.tendsto_of_forall_isOpen_le_liminf_nat'
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
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:
(h_opens G hG).trans (liminf_le_liminf_of_le hu)

Premises used: LE.le.trans, Filter.liminf_le_liminf_of_le
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
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:
exact (h_opens G hG).trans (liminf_le_liminf_of_le hu)

Premises used: LE.le.trans, Filter.liminf_le_liminf_of_le
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
apply : ∀ (u : ℕ → ι) (hu : Tendsto u atTop L), Tendsto ((fun (i : ι) ↦ μs i) ∘ u) atTop (𝓝 μ)
⊢ Tendsto (fun (i : ι) ↦ μs i) L (𝓝 μ)

Tactic:
apply Filter.tendsto_of_seq_tendsto fun u hu ↦ ?_

Premises used: Filter.tendsto_of_seq_tendsto
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
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)
⊢ Tendsto ((fun (i : ι) ↦ μs i) ∘ u) atTop (𝓝 μ)

Tactic:
apply tendsto_of_forall_isOpen_le_liminf_nat fun G hG ↦ (h_opens G hG).trans ?_

Premises used: LE.le.trans, MeasureTheory.tendsto_of_forall_isOpen_le_liminf_nat
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
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)
⊢ 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:
change _ ≤ atTop.liminf ((fun i ↦ μs i G) ∘ u)

Premises used: Filter.liminf, Function.comp, Filter.atTop, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
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))
⊢ 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:
rw [liminf_comp]

Premises used: Filter.liminf_comp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) L fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
refine : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) (map u atTop) fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) 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))

Tactic:
refine liminf_le_liminf_of_le hu (by isBoundedDefault) ?_

Premises used: Filter.liminf_le_liminf_of_le
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
⊢ ∀ (x : ι), LE.le (α := ℝ≥0) ((μs x : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (1 : ℝ≥0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) (map u atTop) fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) G

Tactic:
exact isBoundedUnder_of ⟨1, by simp⟩ |>.isCoboundedUnder_ge

Premises used: Exists.intro, Filter.IsBoundedUnder.isCoboundedUnder_ge, OfNat.ofNat, Filter.isBoundedUnder_of
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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 (𝓝 μ)

Tactic:
tendsto_of_forall_isOpen_le_liminf' ?_

Premises used: MeasureTheory.tendsto_of_forall_isOpen_le_liminf'
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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∞)
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∞)
⊢ Tendsto μs L (𝓝 μ)

Tactic:
refine tendsto_of_forall_isOpen_le_liminf' ?_

Premises used: MeasureTheory.tendsto_of_forall_isOpen_le_liminf'
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : TopologicalSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_2 : L.IsCountablyGenerated
h rwa rwa₁ rwa₂ rwa₃ :
  ∀ (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∞)
⊢ ∀ (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:
rwa [← limsup_measure_closed_le_iff_liminf_measure_open_ge]

Premises used: MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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 (𝓝 μ)

Tactic:
tendsto_of_forall_isClosed_limsup_le' fun F hF_closed ↦ ?_

Premises used: MeasureTheory.tendsto_of_forall_isClosed_limsup_le'
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
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∞)
⊢ Tendsto μs atTop (𝓝 μ)

Tactic:
refine tendsto_of_forall_isClosed_limsup_le' fun F hF_closed ↦ ?_

Premises used: MeasureTheory.tendsto_of_forall_isClosed_limsup_le'
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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 : (a : Set Ω) → ℝ≥0) F) atTop : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) F : ℝ≥0)

Tactic:
specialize h F hF_closed
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
⊢ ContinuousAt ENNReal.ofNNReal (limsup (fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) F) atTop)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
⊢ ∀ᶠ (x : ℝ≥0) in map (fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) F) atTop, (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) x 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
⊢ ∀ (a : ℝ≥0),
    (∀ᶠ (x : ℝ≥0) in map (fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) F) atTop, (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) x a) →
      (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) 0 a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
⊢ (↑(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⟩
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
⊢ (↑(limsup (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop) : ℝ≥0∞) ≤ (↑((μ : (a : Set Ω) → ℝ≥0) F) : ℝ≥0∞)

Tactic:
have obs := ENNReal.coe_mono h
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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∞)
⊢ 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

Premises used: MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
⊢ limsup (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) atTop ≤
    ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F

Tactic:
obs
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
h₁ :
  ∀ (x : ℕ),
    ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F = (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) x
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) atTop : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)

Tactic:
convert! obs
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
x : ℕ
⊢ ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F = (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
apply : ∀ (u : ℕ → ι) (hu : Tendsto u atTop L), Tendsto (μs ∘ u) atTop (𝓝 μ)
⊢ Tendsto μs L (𝓝 μ)

Tactic:
apply Filter.tendsto_of_seq_tendsto fun u hu ↦ ?_

Premises used: Filter.tendsto_of_seq_tendsto
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
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)
⊢ Tendsto (μs ∘ u) atTop (𝓝 μ)

Tactic:
apply tendsto_of_forall_isClosed_limsup_le_nat fun F hF ↦ le_trans ?_ (h F hF)

Premises used: MeasureTheory.tendsto_of_forall_isClosed_limsup_le_nat, le_trans
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
F : Set Ω
hF : IsClosed[inst] F
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) (map u atTop) fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) F

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
F : Set Ω
hF : IsClosed[inst] F
⊢ ∀ᶠ (x : ℝ≥0) in map (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) L, (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) x 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
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:
exact (limsup_comp (fun i ↦ μs i F) u _).trans_le
    (limsup_le_limsup_of_le hu (by isBoundedDefault) ⟨1, by simp⟩)

Premises used: Filter.limsup_comp, Eq.trans_le, Exists.intro, OfNat.ofNat, DFunLike.coe, Filter.limsup_le_limsup_of_le