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∞)
μ_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:
exact MeasurableSet.disjointed (fun i ↦ (hK i).measurableSet)

Premises used: MeasurableSet.disjointed, 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)
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 ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)

Tactic:
have : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n) := by
      rw [← biUnion_Ioc_disjointed_of_monotone h hm, FiniteMeasure.restrict_biUnion_finset]
      · exact (disjoint_disjointed K).set_pairwise _
      · exact MeasurableSet.disjointed (fun i ↦ (hK i).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)
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_3 :
  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
this : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
h₁ : (μ : (a : Set E) → ℝ≥0) (K m \ K n) ≤ u n
⊢ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)) ≤ u n

Tactic:
rw [this, 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)
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_3 :
  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
this : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
⊢ (μ : (a : Set E) → ℝ≥0) (K m \ K n) ≤ u n

Tactic:
le_trans (apply_mono _ (diff_subset_compl (K m) (K n))) (hμ.2 n)

Premises used: MeasureTheory.FiniteMeasure.apply_mono, And.right, Set.diff_subset_compl, 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)
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_3 :
  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
this : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
⊢ (μ : (a : Set E) → ℝ≥0) (K m \ K n) ≤ u n

Tactic:
exact le_trans (apply_mono _ (diff_subset_compl (K m) (K n))) (hμ.2 n)

Premises used: MeasureTheory.FiniteMeasure.apply_mono, And.right, Set.diff_subset_compl, 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
h₁ :
  ∀ (x : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E))
        {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} x ↔
      Membership.mem (γ := Set (FiniteMeasure E))
        ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
          {μ : FiniteMeasure E | μ.mass = C})
        x
⊢ Eq.{u_1 + 1} (α := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
    ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
      {μ : FiniteMeasure E | μ.mass = C})

Tactic:
ext
-- 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
x : FiniteMeasure E
⊢ Membership.mem (γ := Set (FiniteMeasure E))
      {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} x ↔
    Membership.mem (γ := Set (FiniteMeasure E))
      ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
        {μ : FiniteMeasure E | μ.mass = C})
      x

Tactic:
grind
-- 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
⊢ Eq.{u_1 + 1} (α := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
    ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
      {μ : FiniteMeasure E | μ.mass = C})

Tactic:
have : {μ : FiniteMeasure E | μ.mass = C ∧ ∀ n, μ (K n)ᶜ ≤ u n} =
    {μ | μ.mass ≤ C ∧ ∀ n, μ (K n)ᶜ ≤ u n} ∩ {μ | μ.mass = C} := by ext; grind
-- 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
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
    ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
      {μ : FiniteMeasure E | μ.mass = C})
rw :
  IsCompact.{u_1} (X := FiniteMeasure E)
    ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
      {μ : FiniteMeasure E | μ.mass = C})
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}

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
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
    ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
      {μ : FiniteMeasure E | μ.mass = C})
apply : IsClosed[instTopologicalSpace] {μ : FiniteMeasure E | μ.mass = C}
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
      {μ : FiniteMeasure E | μ.mass = C})

Tactic:
apply IsCompact.inter_right (isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le C hu hK h)

Premises used: isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le, IsCompact.inter_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
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
    ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
      {μ : FiniteMeasure E | μ.mass = C})
⊢ Continuous[instTopologicalSpace, _] mass

Tactic:
fun_prop
-- 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
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
    ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
      {μ : FiniteMeasure E | μ.mass = C})
⊢ Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure E) ↦ C

Tactic:
fun_prop
-- 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
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
    ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
      {μ : FiniteMeasure E | μ.mass = C})
⊢ IsClosed[instTopologicalSpace] {μ : FiniteMeasure E | μ.mass = C}

Tactic:
exact isClosed_eq (by fun_prop) (by fun_prop)

Premises used: isClosed_eq
-- 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
apply :
  IsCompact.{u_1} (X := FiniteMeasure E)
    (ProbabilityMeasure.toFiniteMeasure '' {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n})
⊢ IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}

Tactic:
apply (ProbabilityMeasure.toFiniteMeasure_isEmbedding E).isCompact_iff.2

Premises used: Iff.mpr, Topology.IsEmbedding.isCompact_iff, MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding
-- 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
h₁ :
  ∀ (μ : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E))
        (ProbabilityMeasure.toFiniteMeasure ''
          {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n})
        μ ↔
      Membership.mem (γ := Set (FiniteMeasure E))
        {μ : FiniteMeasure E | μ.mass = 1 ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} μ
⊢ Eq.{u_1 + 1} (α := Set (FiniteMeasure E))
    (ProbabilityMeasure.toFiniteMeasure '' {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n})
    {μ : FiniteMeasure E | μ.mass = 1 ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}

Tactic:
ext μ
-- 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
⊢ (∃ (x : ProbabilityMeasure E), (∀ (n : ℕ), (x : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n) ∧ x.toFiniteMeasure = μ) ↔
    μ.mass = 1 ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
h₁ :
  (∃ (x : ProbabilityMeasure E), (∀ (n : ℕ), (x : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n) ∧ x.toFiniteMeasure = μ) →
    μ.mass = 1 ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
h₂ :
  (μ.mass = 1 ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n) →
    ∃ (x : ProbabilityMeasure E), (∀ (n : ℕ), (x : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n) ∧ x.toFiniteMeasure = μ
⊢ (∃ (x : ProbabilityMeasure E), (∀ (n : ℕ), (x : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n) ∧ x.toFiniteMeasure = μ) ↔
    μ.mass = 1 ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n

Tactic:
refine ⟨?_, ?_⟩
-- 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
ν : ProbabilityMeasure E
hν : ∀ (n : ℕ), (ν : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ ν.toFiniteMeasure.mass = 1 ∧ ∀ (n : ℕ), (ν.toFiniteMeasure : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n

Tactic:
simpa using 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
hμ : μ.mass = 1
h'μ : ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ (↑μ : Measure E).real univ = 1

Tactic:
simpa using 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
hμ : μ.mass = 1
h'μ : ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
ν : ProbabilityMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (↑μ : Measure E) ⋯
h₁ :
  ∀ (s : Set E),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((↑ν.toFiniteMeasure : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
        (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ν.toFiniteMeasure = μ

Tactic:
ext
-- 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
hμ : μ.mass = 1
h'μ : ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
ν : ProbabilityMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (↑μ : Measure E) ⋯
s : Set E
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((↑ν.toFiniteMeasure : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl
-- 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
hμ : μ.mass = 1
h'μ : ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
ν : ProbabilityMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (↑μ : Measure E) ⋯
⊢ ν.toFiniteMeasure = μ

Tactic:
have : ν.toFiniteMeasure = μ := by ext; rfl
-- 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
hμ : μ.mass = 1
h'μ : ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
ν : ProbabilityMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (↑μ : Measure E) ⋯
this : ν.toFiniteMeasure = μ
⊢ ∀ (n : ℕ), (ν : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n

Tactic:
simpa [← this] using h'μ