awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
n : ℕ
ν : FiniteMeasure E
hν :
  Membership.mem (γ := Set (FiniteMeasure E))
    {ρ : FiniteMeasure E |
      ρ.mass ≤ C ∧ Eq (α := ℝ≥0) ((ρ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)}
    ν
ν_lim : Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 ν)
ν' : Measure E
ν'_reg : ν'.InnerRegular
ν'_fin : IsFiniteMeasure ν'
ν'K : Eq (α := ℝ≥0∞) ((ν' : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hν' :
  ∀ (g : E →ᵇ ℝ), Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ν : Measure E)) (∫ (x : E), (g : (a : E) → ℝ) x ∂ν')
μ : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) ν' ν'_fin
apply :
  ∀ (g : E →ᵇ ℝ),
    Tendsto (β := ℝ)
      (fun (i : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(i.restrict (disjointed K n)) : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)))
⊢ Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 μ)

Tactic:
apply tendsto_of_forall_integral_tendsto (fun g ↦ ?_)

Premises used: MeasureTheory.FiniteMeasure.tendsto_of_forall_integral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
n : ℕ
ν : FiniteMeasure E
hν :
  Membership.mem (γ := Set (FiniteMeasure E))
    {ρ : FiniteMeasure E |
      ρ.mass ≤ C ∧ Eq (α := ℝ≥0) ((ρ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)}
    ν
ν_lim : Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 ν)
ν' : Measure E
ν'_reg : ν'.InnerRegular
ν'_fin : IsFiniteMeasure ν'
ν'K : Eq (α := ℝ≥0∞) ((ν' : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hν' :
  ∀ (g : E →ᵇ ℝ), Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ν : Measure E)) (∫ (x : E), (g : (a : E) → ℝ) x ∂ν')
μ : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) ν' ν'_fin
g : E →ᵇ ℝ
⊢ Tendsto (β := ℝ)
    (fun (i : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(i.restrict (disjointed K n)) : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ν : Measure E)))

Tactic:
tendsto_iff_forall_integral_tendsto.1 ν_lim g

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
n : ℕ
ν : FiniteMeasure E
hν :
  Membership.mem (γ := Set (FiniteMeasure E))
    {ρ : FiniteMeasure E |
      ρ.mass ≤ C ∧ Eq (α := ℝ≥0) ((ρ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)}
    ν
ν_lim : Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 ν)
ν' : Measure E
ν'_reg : ν'.InnerRegular
ν'_fin : IsFiniteMeasure ν'
ν'K : Eq (α := ℝ≥0∞) ((ν' : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hν' :
  ∀ (g : E →ᵇ ℝ), Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ν : Measure E)) (∫ (x : E), (g : (a : E) → ℝ) x ∂ν')
μ : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) ν' ν'_fin
g : E →ᵇ ℝ
h₁ : Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ν : Measure E))
⊢ Tendsto (β := ℝ)
    (fun (i : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(i.restrict (disjointed K n)) : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)))

Tactic:
convert! tendsto_iff_forall_integral_tendsto.1 ν_lim g using 2

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
n : ℕ
ν : FiniteMeasure E
hν :
  Membership.mem (γ := Set (FiniteMeasure E))
    {ρ : FiniteMeasure E |
      ρ.mass ≤ C ∧ Eq (α := ℝ≥0) ((ρ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)}
    ν
ν_lim : Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 ν)
ν' : Measure E
ν'_reg : ν'.InnerRegular
ν'_fin : IsFiniteMeasure ν'
ν'K : Eq (α := ℝ≥0∞) ((ν' : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hν' :
  ∀ (g : E →ᵇ ℝ), Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ν : Measure E)) (∫ (x : E), (g : (a : E) → ℝ) x ∂ν')
μ : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) ν' ν'_fin
g : E →ᵇ ℝ
⊢ Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ν : Measure E))

Tactic:
(hν' g).symm

Premises used: MeasureTheory.FiniteMeasure.toMeasure, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
n : ℕ
ν : FiniteMeasure E
hν :
  Membership.mem (γ := Set (FiniteMeasure E))
    {ρ : FiniteMeasure E |
      ρ.mass ≤ C ∧ Eq (α := ℝ≥0) ((ρ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)}
    ν
ν_lim : Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 ν)
ν' : Measure E
ν'_reg : ν'.InnerRegular
ν'_fin : IsFiniteMeasure ν'
ν'K : Eq (α := ℝ≥0∞) ((ν' : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hν' :
  ∀ (g : E →ᵇ ℝ), Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ν : Measure E)) (∫ (x : E), (g : (a : E) → ℝ) x ∂ν')
μ : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) ν' ν'_fin
g : E →ᵇ ℝ
⊢ Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ν : Measure E))

Tactic:
exact (hν' g).symm

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
⊢ ∀ (n : ℕ),
    ∃ (ν : FiniteMeasure E),
      (↑ν : Measure E).InnerRegular ∧
        Eq (α := ℝ≥0) ((ν : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0) ∧
          Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 ν)

Tactic:
have M n : ∃ (ν : FiniteMeasure E), Measure.InnerRegular (ν : Measure E) ∧
      ν (partialSups K n)ᶜ = 0 ∧
      Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) f (𝓝 ν) := by
    -- the existence of a limit follows from the fact that these measures are supported in
    -- the compact set `partialSups K n`.
    obtain ⟨ν, hν, ν_lim⟩ : ∃ ν ∈ {ρ : FiniteMeasure E | ρ.mass ≤ C ∧ ρ (partialSups K n)ᶜ = 0},
        Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) f (𝓝 ν) := by
      simp only [Tendsto]
      rw [← Ultrafilter.coe_map]
      apply IsCompact.ultrafilter_le_nhds'
        (isCompact_setOf_finiteMeasure_le_of_isCompact C (A n))
      simp only [null_iff_toMeasure_null, Ultrafilter.mem_map, preimage_setOf_eq]
      filter_upwards [hf] with ρ hρ
      simp only [restrict_mass, restrict_measure_eq,
        Measure.restrict_apply (A n).measurableSet.compl]
      refine ⟨(apply_le_mass ρ _).trans hρ.1, ?_⟩
      convert! measure_empty (μ := (ρ : Measure E))
      apply disjoint_iff.1
      apply disjoint_compl_left.mono_right
      exact le_trans sdiff_le (le_partialSups _ _)
    -- We can find an inner regular measure which coincides with the above limit wrt
    -- integration of bounded continuous functions.
    obtain ⟨ν', ν'_reg, ν'_fin, ν'K, hν'⟩ : ∃ ν', ν'.InnerRegular ∧ IsFiniteMeasure ν' ∧
        ν' (partialSups K n)ᶜ = 0 ∧ ∀ (g : E →ᵇ ℝ), ∫ x, g x ∂ν = ∫ x, g x ∂ν' := by
      apply Measure.exists_innerRegular_eq_of_isCompact _ (A n)
      rw [← MeasureTheory.FiniteMeasure.null_iff_toMeasure_null]
      exact hν.2
    -- This inner regular measure is also a limit for our ultrafilter
    let μ : FiniteMeasure E := ⟨ν', ν'_fin⟩
    refine ⟨μ, ν'_reg, by simp [μ, ν'K], ?_⟩
    apply tendsto_of_forall_integral_tendsto (fun g ↦ ?_)
    convert! tendsto_iff_forall_integral_tendsto.1 ν_lim g using 2
    exact (hν' g).symm
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
M :
  ∀ (n : ℕ),
    ∃ (ν : FiniteMeasure E),
      (↑ν : Measure E).InnerRegular ∧
        Eq (α := ℝ≥0) ((ν : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0) ∧
          Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 ν)
choose! :
  ∀ (ν : (n : ℕ) → FiniteMeasure E) (ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular)
    (νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0))
    (hν :
      ∀ (n : ℕ),
        Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))),
    ∃ (x : FiniteMeasure E),
      Membership.mem (γ := Set (FiniteMeasure E))
          {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} x ∧
        (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x
⊢ ∃ (x : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E))
        {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} x ∧
      (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x

Tactic:
choose! ν ν_reg νK hν using M
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
simp : ∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
⊢ ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)

Tactic:
simp only [MeasurableSet.univ, Measure.sum_apply]

Premises used: MeasureTheory.Measure.sum_apply, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ) atTop
    (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ))

Tactic:
have : Tendsto (fun n ↦ ∑ i ∈ Finset.range (n + 1), (ν i : Measure E) univ) atTop
        (𝓝 (∑' i, (ν i : Measure E) univ)) :=
      (ENNReal.tendsto_nat_tsum _).comp (tendsto_add_atTop_nat 1)
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
this :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ) atTop
    (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ))
apply : ∀ (n : ℕ), ∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
⊢ ∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)

Tactic:
apply le_of_tendsto' this (fun n ↦ ?_)

Premises used: le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
this :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ) atTop
    (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ))
n : ℕ
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
this :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ) atTop
    (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ))
n : ℕ
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
have : ∑ i ∈ Finset.range (n + 1), (ν i : Measure E) univ
        = (∑ i ∈ Finset.range (n + 1), ν i).toMeasure univ := by simp
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ) atTop
    (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ))
n : ℕ
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞)
rw : (((↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ) atTop
    (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ))
n : ℕ
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞)
this : mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i) ≤ C
⊢ (↑(mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i)) : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)

Tactic:
ENNReal.coe_le_coe.2 this

Premises used: Iff.mpr, ENNReal.coe_le_coe