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)
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))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
h₁ : mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i) ≤ u n
⊢ (((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑(u n) : ℝ≥0∞)

Tactic:
suffices (∑ i ∈ Finset.Ioc n m, ν i).mass ≤ u n 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)
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))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
h₁ :
  Tendsto (β := FiniteMeasure E) (fun (i : FiniteMeasure E) ↦ ∑ i_1 ∈ Finset.Ioc n m, i.restrict (disjointed K i_1))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∑ i ∈ Finset.Ioc n m, ν i))
⊢ Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν 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)
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))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
⊢ Tendsto (β := FiniteMeasure E) (fun (i : FiniteMeasure E) ↦ ∑ i_1 ∈ Finset.Ioc n m, i.restrict (disjointed K i_1))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∑ i ∈ Finset.Ioc n m, ν 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)
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))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
⊢ Tendsto (β := FiniteMeasure E) (fun (i : FiniteMeasure E) ↦ ∑ i_1 ∈ Finset.Ioc n m, i.restrict (disjointed K i_1))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∑ i ∈ Finset.Ioc n m, ν 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)
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))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
⊢ Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))

Tactic:
have : Tendsto (fun (μ : FiniteMeasure E) ↦
        (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass) f
        (𝓝 ((∑ i ∈ Finset.Ioc n m, ν 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)
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))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
h₁ :
  ∀ᶠ (c : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
    mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, c.restrict (disjointed K i)) ≤ u n
⊢ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i) ≤ u n

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)
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))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
h₁ :
  ∀ (μ : FiniteMeasure E) (hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n),
    mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)) ≤ u n
⊢ ∀ᶠ (c : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
    mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, c.restrict (disjointed K i)) ≤ u n

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)
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))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ_1 : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ_1)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
hd : (↑(Finset.Ioc n m) : Set ℕ).Pairwise (Disjoint on disjointed K)
hm₁ : ∀ (i : ℕ), MeasurableSet (disjointed K i)
⊢ ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)

Tactic:
rw [← biUnion_Ioc_disjointed_of_monotone h hm, FiniteMeasure.restrict_biUnion_finset]

Premises used: MeasureTheory.FiniteMeasure.restrict_biUnion_finset, biUnion_Ioc_disjointed_of_monotone
-- 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)
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))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ_1 : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ_1)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ (↑(Finset.Ioc n m) : Set ℕ).Pairwise (Disjoint on disjointed K)

Tactic:
(disjoint_disjointed K).set_pairwise _

Premises used: disjoint_disjointed, Pairwise.set_pairwise
-- 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)
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))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ_1 : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ_1)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ (↑(Finset.Ioc n m) : Set ℕ).Pairwise (Disjoint on disjointed K)

Tactic:
exact (disjoint_disjointed K).set_pairwise _

Premises used: disjoint_disjointed, Pairwise.set_pairwise
-- 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)
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))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ_1 : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ_1)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ ∀ (i : ℕ), MeasurableSet (disjointed K i)

Tactic:
MeasurableSet.disjointed (fun i ↦ (hK i).measurableSet)

Premises used: MeasurableSet.disjointed, IsCompact.measurableSet