awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
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∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
h : ∀ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) = (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞)
⊢ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)

Tactic:
convert! obs i with x
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
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∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x_1 : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
x : Ω
⊢ ENNReal.ofReal ((fun (f : Ω →ᵇ ℝ) ↦ f.toFun) f x) = (↑(NNReal.mk ((fun (f : Ω →ᵇ ℝ) ↦ f.toFun) f x) ⋯) : ℝ≥0∞)

Tactic:
have aux := ENNReal.ofReal_eq_coe_nnreal (f_nn x)
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
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∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x_1 : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
x : Ω
aux : ENNReal.ofReal ((f : (a : Ω) → ℝ) x) = (↑(NNReal.mk ((f : (a : Ω) → ℝ) x) ⋯) : ℝ≥0∞)
h : (↑(NNReal.mk ((f : (a : Ω) → ℝ) x) ⋯) : ℝ≥0∞) = (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞)
⊢ ENNReal.ofReal ((f : (a : Ω) → ℝ) x) = (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞)

Tactic:
rw [aux]
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
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∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x_1 : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
x : Ω
aux : ENNReal.ofReal ((f : (a : Ω) → ℝ) x) = (↑(NNReal.mk ((f : (a : Ω) → ℝ) x) ⋯) : ℝ≥0∞)
h : (f : (a : Ω) → ℝ) x = norm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)
⊢ (↑(NNReal.mk ((f : (a : Ω) → ℝ) x) ⋯) : ℝ≥0∞) = (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
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∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x_1 : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
x : Ω
aux : ENNReal.ofReal ((f : (a : Ω) → ℝ) x) = (↑(NNReal.mk ((f : (a : Ω) → ℝ) x) ⋯) : ℝ≥0∞)
⊢ (f : (a : Ω) → ℝ) x = norm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)

Tactic:
(Real.norm_of_nonneg (f_nn x)).symm

Premises used: Eq.symm, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
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∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x_1 : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
x : Ω
aux : ENNReal.ofReal ((f : (a : Ω) → ℝ) x) = (↑(NNReal.mk ((f : (a : Ω) → ℝ) x) ⋯) : ℝ≥0∞)
⊢ (f : (a : Ω) → ℝ) x = norm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)

Tactic:
exact (Real.norm_of_nonneg (f_nn x)).symm

Premises used: Eq.symm, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
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) atTop : ℝ≥0∞)
⊢ Tendsto (fun (i : ℕ) ↦ μs i) atTop (𝓝 μ)

Tactic:
ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.mpr ?_

Premises used: Iff.mpr, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
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) atTop : ℝ≥0∞)
refine :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs i) : Measure Ω)) atTop
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑μ : Measure Ω)))
⊢ Tendsto (fun (i : ℕ) ↦ μs i) atTop (𝓝 μ)

Tactic:
refine ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.mpr ?_

Premises used: Iff.mpr, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
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) atTop : ℝ≥0∞)
⊢ ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs i) : Measure Ω)) atTop
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑μ : Measure Ω)))

Tactic:
tendsto_integral_of_forall_integral_le_liminf_integral fun f f_nn ↦ ?_

Premises used: BoundedContinuousFunction.tendsto_integral_of_forall_integral_le_liminf_integral
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
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) atTop : ℝ≥0∞)
refine :
  ∀ (f : Ω →ᵇ ℝ) (f_nn : 0 ≤ f),
    LE.le (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω))
      (liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) atTop)
⊢ ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs i) : Measure Ω)) atTop
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑μ : Measure Ω)))

Tactic:
refine tendsto_integral_of_forall_integral_le_liminf_integral fun f f_nn ↦ ?_

Premises used: BoundedContinuousFunction.tendsto_integral_of_forall_integral_le_liminf_integral
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
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) atTop : ℝ≥0∞)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
⊢ LE.le (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω))
    (liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) atTop)

Tactic:
integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure f_nn h_opens

Premises used: MeasureTheory.integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
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) atTop : ℝ≥0∞)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
⊢ LE.le (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω))
    (liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) atTop)

Tactic:
exact integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure f_nn h_opens

Premises used: MeasureTheory.integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
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)
⊢ Tendsto (fun (i : ℕ) ↦ μs i) atTop (𝓝 μ)

Tactic:
tendsto_of_forall_isOpen_le_liminf_nat' fun G G_open ↦ ?_

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 Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
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)
refine :
  ∀ (G : Set Ω) (G_open : IsOpen[inst_1] G),
    LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
      (liminf (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
⊢ Tendsto (fun (i : ℕ) ↦ μs i) atTop (𝓝 μ)

Tactic:
refine tendsto_of_forall_isOpen_le_liminf_nat' fun G G_open ↦ ?_

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 Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
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)
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) atTop : ℝ≥0)

Tactic:
specialize h_opens G G_open
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
⊢ (↑(liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop) : ℝ≥0∞) =
    liminf (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop

Tactic:
Monotone.map_liminf_of_continuousAt (F := atTop) ENNReal.coe_mono (μs · G) ?_ ?_ ?_

Premises used: Monotone.map_liminf_of_continuousAt, ENNReal.coe_mono, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
refine_3 : IsBoundedUnder (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

Tactic:
refine Monotone.map_liminf_of_continuousAt (F := atTop) ENNReal.coe_mono (μs · G) ?_ ?_ ?_

Premises used: Monotone.map_liminf_of_continuousAt, ENNReal.coe_mono, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
⊢ ContinuousAt ENNReal.ofNNReal (liminf (fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) G) atTop)

Tactic:
ENNReal.continuous_coe.continuousAt

Premises used: Continuous.continuousAt, ENNReal.continuous_coe
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
⊢ ContinuousAt ENNReal.ofNNReal (liminf (fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) G) atTop)

Tactic:
exact ENNReal.continuous_coe.continuousAt

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

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

Tactic:
exact IsBoundedUnder.isCoboundedUnder_ge ⟨1, by simp⟩

Premises used: Exists.intro, Filter.IsBoundedUnder.isCoboundedUnder_ge, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
⊢ ∀ᶠ (x : ℝ≥0) in map (fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) G) atTop, (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) x 0

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

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

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

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

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

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

Tactic:
simp only [Function.comp_apply, ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure]

Premises used: MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, Function.comp_apply