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 : ℕ
h₁ :
  ∀ (ρ : FiniteMeasure E) (hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n),
    (ρ.restrict (disjointed K n)).mass ≤ C ∧
      Eq (α := ℝ≥0∞)
        (((↑(ρ.restrict (disjointed K n)) : Measure E) : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ :
          ℝ≥0∞)
        (0 : ℝ≥0∞)
⊢ {a : FiniteMeasure E |
      (a.restrict (disjointed K n)).mass ≤ C ∧
        Eq (α := ℝ≥0∞)
          (((↑(a.restrict (disjointed K n)) : Measure E) : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ :
            ℝ≥0∞)
          (0 : ℝ≥0∞)} ∈
    f

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
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
h₁ :
  (ρ : (a : Set E) → ℝ≥0) (disjointed K n) ≤ C ∧
    Eq (α := ℝ≥0∞)
      (((↑ρ : Measure E) : (a : Set E) → ℝ≥0∞) (((partialSups K : (a : ℕ) → Set E) n)ᶜ ∩ disjointed K n) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ (ρ.restrict (disjointed K n)).mass ≤ C ∧
    Eq (α := ℝ≥0∞)
      (((↑(ρ.restrict (disjointed K n)) : Measure E) : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
simp only [restrict_mass, restrict_measure_eq,
        Measure.restrict_apply (A n).measurableSet.compl]

Premises used: MeasureTheory.Measure.restrict_apply, MeasurableSet.compl, MeasureTheory.FiniteMeasure.restrict_mass, MeasureTheory.FiniteMeasure.restrict_measure_eq, IsCompact.measurableSet
-- 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ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ (ρ : (a : Set E) → ℝ≥0) (disjointed K n) ≤ C ∧
    Eq (α := ℝ≥0∞)
      (((↑ρ : Measure E) : (a : Set E) → ℝ≥0∞) (((partialSups K : (a : ℕ) → Set E) n)ᶜ ∩ disjointed K n) : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
⟨(apply_le_mass ρ _).trans hρ.1, ?_⟩

Premises used: And.left, And.intro, MeasureTheory.FiniteMeasure.apply_le_mass, LE.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
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
h₁ :
  Eq (α := ℝ≥0∞)
    (((↑ρ : Measure E) : (a : Set E) → ℝ≥0∞) (((partialSups K : (a : ℕ) → Set E) n)ᶜ ∩ disjointed K n) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ (ρ : (a : Set E) → ℝ≥0) (disjointed K n) ≤ C ∧
    Eq (α := ℝ≥0∞)
      (((↑ρ : Measure E) : (a : Set E) → ℝ≥0∞) (((partialSups K : (a : ℕ) → Set E) n)ᶜ ∩ disjointed K n) : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
refine ⟨(apply_le_mass ρ _).trans hρ.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
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ Eq (α := ℝ≥0∞) (((↑ρ : Measure E) : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_empty (μ := (ρ : Measure E))

Premises used: MeasureTheory.measure_empty
-- 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ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
h₁ : Eq (α := Set E) (((partialSups K : (a : ℕ) → Set E) n)ᶜ ∩ disjointed K n : Set E) (∅ : Set E)
⊢ Eq (α := ℝ≥0∞)
    (((↑ρ : Measure E) : (a : Set E) → ℝ≥0∞) (((partialSups K : (a : ℕ) → Set E) n)ᶜ ∩ disjointed K n) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
convert! measure_empty (μ := (ρ : Measure E))

Premises used: MeasureTheory.measure_empty
-- 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ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
h₁ : Disjoint ((partialSups K : (a : ℕ) → Set E) n)ᶜ (disjointed K n)
⊢ Eq (α := Set E) (((partialSups K : (a : ℕ) → Set E) n)ᶜ ∩ disjointed K n : Set E) (∅ : Set E)

Tactic:
apply disjoint_iff.1

Premises used: disjoint_iff, 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ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
h₁ : disjointed K n ≤ (partialSups K : (a : ℕ) → Set E) n
⊢ Disjoint ((partialSups K : (a : ℕ) → Set E) n)ᶜ (disjointed K n)

Tactic:
apply disjoint_compl_left.mono_right

Premises used: disjoint_compl_left, Disjoint.mono_right
-- 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ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ disjointed K n ≤ (partialSups K : (a : ℕ) → Set E) n

Tactic:
le_trans sdiff_le (le_partialSups _ _)

Premises used: sdiff_le, le_partialSups, 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
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ disjointed K n ≤ (partialSups K : (a : ℕ) → Set E) n

Tactic:
exact le_trans sdiff_le (le_partialSups _ _)

Premises used: sdiff_le, le_partialSups, 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 : ℕ
obtain :
  ∀ (ν : 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)) (𝓝 ν)),
    ∃ (ν : 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)) (𝓝 ν)
⊢ ∃ (ν : 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:
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 _ _)

Premises used: MeasureTheory.FiniteMeasure
-- 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)) (𝓝 ν)
apply :
  Eq (α := ℝ≥0∞) (((↑ν : Measure E) : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (ν' : Measure E),
    ν'.InnerRegular ∧
      IsFiniteMeasure ν' ∧
        Eq (α := ℝ≥0∞) ((ν' : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          ∀ (g : E →ᵇ ℝ),
            Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ν : Measure E)) (∫ (x : E), (g : (a : E) → ℝ) x ∂ν')

Tactic:
apply Measure.exists_innerRegular_eq_of_isCompact _ (A n)

Premises used: MeasureTheory.Measure.exists_innerRegular_eq_of_isCompact
-- 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)) (𝓝 ν)
rw : Eq (α := ℝ≥0) ((ν : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
⊢ Eq (α := ℝ≥0∞) (((↑ν : Measure E) : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← MeasureTheory.FiniteMeasure.null_iff_toMeasure_null]

Premises used: MeasureTheory.FiniteMeasure.null_iff_toMeasure_null
-- 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)) (𝓝 ν)
⊢ Eq (α := ℝ≥0) ((ν : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)

Tactic:
hν.2

Premises used: And.right
-- 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)) (𝓝 ν)
⊢ Eq (α := ℝ≥0) ((ν : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)

Tactic:
exact hν.2

Premises used: And.right
-- 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)) (𝓝 ν)
obtain :
  ∀ (ν' : 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),
      (↑ν : 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)) (𝓝 ν)
⊢ ∃ (ν : 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:
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
-- 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
⊢ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp [μ, ν'K]
-- 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
refine : Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
⊢ ∃ (ν : 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:
refine ⟨μ, ν'_reg, by simp [μ, ν'K], ?_⟩