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
ν_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
h₁ :
  (((↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ =
    (↑(mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i)) : ℝ≥0∞)
⊢ (((↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)

Tactic:
convert! ENNReal.coe_le_coe.2 this

Premises used: Iff.mpr, ENNReal.coe_le_coe
-- 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
⊢ (((↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ =
    (↑(mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i)) : ℝ≥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_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∞)
suffices : mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i) ≤ C
⊢ (((↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)

Tactic:
suffices (∑ i ∈ Finset.range (n + 1), ν i).mass ≤ C by
      convert! ENNReal.coe_le_coe.2 this
      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∞)
h₁ :
  Tendsto (β := FiniteMeasure E)
    (fun (i : FiniteMeasure E) ↦ ∑ i_1 ∈ Finset.range (n + 1), i.restrict (disjointed K i_1))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∑ i ∈ Finset.range (n + 1), ν i))
⊢ Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i)))

Tactic:
apply Tendsto.mass

Premises used: Filter.Tendsto.mass
-- 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∞)
⊢ Tendsto (β := FiniteMeasure E)
    (fun (i : FiniteMeasure E) ↦ ∑ i_1 ∈ Finset.range (n + 1), i.restrict (disjointed K i_1))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∑ i ∈ Finset.range (n + 1), ν i))

Tactic:
tendsto_finsetSum _ (fun i hi ↦ hν i)

Premises used: tendsto_finsetSum
-- 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∞)
⊢ Tendsto (β := FiniteMeasure E)
    (fun (i : FiniteMeasure E) ↦ ∑ i_1 ∈ Finset.range (n + 1), i.restrict (disjointed K i_1))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∑ i ∈ Finset.range (n + 1), ν i))

Tactic:
exact tendsto_finsetSum _ (fun i hi ↦ hν i)

Premises used: tendsto_finsetSum
-- 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∞)
⊢ Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i)))

Tactic:
have : Tendsto (fun (μ : FiniteMeasure E) ↦
        (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)).mass) f
        (𝓝 ((∑ i ∈ Finset.range (n + 1), ν i).mass)) := by
      apply Tendsto.mass
      exact tendsto_finsetSum _ (fun i hi ↦ hν i)
-- 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 :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i)))
apply :
  ∀ᶠ (c : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
    mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), c.restrict (disjointed K i)) ≤ C
⊢ mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i) ≤ C

Tactic:
apply le_of_tendsto this

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_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 :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i)))
h₁ :
  ∀ (μ : FiniteMeasure E) (hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n),
    mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)) ≤ C
⊢ ∀ᶠ (c : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
    mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), c.restrict (disjointed K i)) ≤ C

Tactic:
filter_upwards [hf] with μ hμ
-- 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 :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i)))
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
h₁ : (μ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n) ≤ C
⊢ mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)) ≤ C

Tactic:
rw [I, restrict_mass]

Premises used: MeasureTheory.FiniteMeasure.restrict_mass
-- 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 :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i)))
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ (μ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n) ≤ C

Tactic:
le_trans (apply_mono _ (subset_univ _)) hμ.1

Premises used: Set.subset_univ, MeasureTheory.FiniteMeasure.apply_mono, And.left, le_trans
-- 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 :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.range (n + 1), ν i)))
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ (μ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n) ≤ C

Tactic:
exact le_trans (apply_mono _ (subset_univ _)) hμ.1

Premises used: Set.subset_univ, MeasureTheory.FiniteMeasure.apply_mono, And.left, le_trans
-- 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))
⊢ ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)

Tactic:
have B : (Measure.sum (fun n ↦ (ν n : Measure E))) univ ≤ C := by
    -- this follows from the corresponding result for finite sums, where we can use the
    -- continuity of the mass of a finite measure under weak convergence.
    simp only [MeasurableSet.univ, Measure.sum_apply]
    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)
    apply le_of_tendsto' this (fun n ↦ ?_)
    have : ∑ i ∈ Finset.range (n + 1), (ν i : Measure E) univ
        = (∑ i ∈ Finset.range (n + 1), ν i).toMeasure univ := by simp
    rw [this]
    suffices (∑ i ∈ Finset.range (n + 1), ν i).mass ≤ C by
      convert! ENNReal.coe_le_coe.2 this
      simp
    have : Tendsto (fun (μ : FiniteMeasure E) ↦
        (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)).mass) f
        (𝓝 ((∑ i ∈ Finset.range (n + 1), ν i).mass)) := by
      apply Tendsto.mass
      exact tendsto_finsetSum _ (fun i hi ↦ hν i)
    apply le_of_tendsto this
    filter_upwards [hf] with μ hμ
    rw [I, restrict_mass]
    exact le_trans (apply_mono _ (subset_univ _)) hμ.1