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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
⊢ ∀ (s : Set { x : E // x ∈ K }), MeasurableSet s → MeasurableSet (Subtype.val (p := fun (x : E) ↦ x ∈ K) '' s)

Tactic:
fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht

Premises used: MeasurableEmbedding.measurableSet_image', Topology.IsClosedEmbedding.measurableEmbedding
-- 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
⊢ ∀ (s : Set { x : E // x ∈ K }), MeasurableSet s → MeasurableSet (Subtype.val (p := fun (x : E) ↦ x ∈ K) '' s)

Tactic:
exact fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht

Premises used: MeasurableEmbedding.measurableSet_image', Topology.IsClosedEmbedding.measurableEmbedding
-- 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
⊢ MeasurableSet (α := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K) ⁻¹' s)

Tactic:
hf.continuous.measurable hs

Premises used: Topology.IsClosedEmbedding.continuous, Continuous.measurable
-- 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
⊢ MeasurableSet (α := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K) ⁻¹' s)

Tactic:
exact hf.continuous.measurable hs

Premises used: Topology.IsClosedEmbedding.continuous, Continuous.measurable
-- 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
h₂ :
  ∀ (a : FiniteMeasure (↑K : Type u_1)),
    a.mass ≤ C →
      mass (a.map f) ≤ C ∧
        Eq (α := ℝ≥0∞) (((Measure.map f (↑a : Measure (↑K : Type u_1)) : Measure E) : (a : Set E) → ℝ≥0∞) Kᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)
⊢ F '' T ⊆ {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)}

Tactic:
simp only [null_iff_toMeasure_null, image_subset_iff, preimage_setOf_eq, toMeasure_map,
        setOf_subset_setOf, F, T]

Premises used: Set.preimage_setOf_eq, Set.setOf_subset_setOf, Set.image_subset_iff, MeasureTheory.FiniteMeasure.toMeasure_map, 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure (↑K : Type u_1)
hμ : μ.mass ≤ C
h₂ :
  mass (μ.map f) ≤ C ∧
    Eq (α := ℝ≥0∞) (((↑μ : Measure (↑K : Type u_1)) : (a : Set (↑K : Type u_1)) → ℝ≥0∞) (f ⁻¹' Kᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ mass (μ.map f) ≤ C ∧
    Eq (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure (↑K : Type u_1)) : Measure E) : (a : Set E) → ℝ≥0∞) Kᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
rw [Measure.map_apply hf.continuous.measurable hK.measurableSet.compl]

Premises used: MeasureTheory.Measure.map_apply, MeasurableSet.compl, Topology.IsClosedEmbedding.continuous, Continuous.measurable, 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure (↑K : Type u_1)
hμ : μ.mass ≤ C
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure (↑K : Type u_1)) : (a : Set (↑K : Type u_1)) → ℝ≥0∞) (f ⁻¹' Kᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [f]
-- 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure (↑K : Type u_1)
hμ : μ.mass ≤ C
⊢ mass (μ.map f) ≤ C ∧
    Eq (α := ℝ≥0∞) (((↑μ : Measure (↑K : Type u_1)) : (a : Set (↑K : Type u_1)) → ℝ≥0∞) (f ⁻¹' Kᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine ⟨(mass_map_le _ _).trans hμ, by simp [f]⟩
-- 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
⊢ {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} = F '' T

Tactic:
have : {μ : FiniteMeasure E | μ.mass ≤ C ∧ μ Kᶜ = 0} = F '' T := by
    apply Subset.antisymm
    · intro μ hμ
      simp only [mem_image]
      refine ⟨μ.comap f, (FiniteMeasure.mass_comap_le _ _).trans hμ.1, ?_⟩
      ext s hs
      simp only [toMeasure_map, F]
      rw [Measure.map_apply measurable_subtype_coe hs]
      simp only [toMeasure_comap]
      rw [Measure.comap_apply _ (Subtype.val_injective), image_preimage_eq_inter_range]
      · rw [← Measure.restrict_apply hs, Measure.restrict_eq_self_of_ae_mem]
        apply (null_iff_toMeasure_null (↑μ) (range f)ᶜ).mp
        rw [rf]
        exact hμ.2
      · exact fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht
      · exact hf.continuous.measurable hs
    · simp only [null_iff_toMeasure_null, image_subset_iff, preimage_setOf_eq, toMeasure_map,
        setOf_subset_setOf, F, T]
      intro μ hμ
      rw [Measure.map_apply hf.continuous.measurable hK.measurableSet.compl]
      refine ⟨(mass_map_le _ _).trans hμ, by simp [f]⟩
-- 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
this : {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} = F '' T
rw : IsCompact (F '' T)
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)}

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
this : {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} = F '' T
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] F

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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
this : {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} = F '' T
apply : IsCompact T
⊢ IsCompact (F '' T)

Tactic:
apply IsCompact.image _ (by fun_prop)

Premises used: IsCompact.image
-- 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
this : {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} = F '' T
⊢ CompactSpace.{u_1} (↑K : Type u_1)

Tactic:
have : CompactSpace K := isCompact_iff_compactSpace.mp hK
-- 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
this_1 : {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} = F '' T
this : CompactSpace.{u_1} (↑K : Type u_1)
⊢ IsCompact T

Tactic:
isCompact_setOf_finiteMeasure_le_of_compactSpace _ _

Premises used: setOf, isCompact_setOf_finiteMeasure_le_of_compactSpace
-- 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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
this_1 : {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} = F '' T
this : CompactSpace.{u_1} (↑K : Type u_1)
⊢ IsCompact T

Tactic:
exact isCompact_setOf_finiteMeasure_le_of_compactSpace _ _

Premises used: isCompact_setOf_finiteMeasure_le_of_compactSpace
-- 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
μ : FiniteMeasure E
n : ℕ
hd : (↑(Finset.range (n + 1)) : Set ℕ).Pairwise (Disjoint on disjointed K)
hm : ∀ (i : ℕ), MeasurableSet (disjointed K i)
⊢ ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)

Tactic:
rw [← biUnion_range_succ_disjointed, FiniteMeasure.restrict_biUnion_finset]

Premises used: biUnion_range_succ_disjointed, MeasureTheory.FiniteMeasure.restrict_biUnion_finset
-- 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
μ : FiniteMeasure E
n : ℕ
⊢ (↑(Finset.range (n + 1)) : 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)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
n : ℕ
⊢ (↑(Finset.range (n + 1)) : 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)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
n : ℕ
⊢ ∀ (i : ℕ), MeasurableSet (disjointed K i)

Tactic:
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)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
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)
h : NormalSpace E ∨ Monotone K
⊢ ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)

Tactic:
have I (μ : FiniteMeasure E) (n : ℕ) :
      ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict (partialSups K n) := by
    rw [← biUnion_range_succ_disjointed, 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)
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)
n : ℕ
⊢ IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)

Tactic:
simpa [partialSups_eq_accumulate] using isCompact_accumulate hK _

Premises used: Set.partialSups_eq_accumulate, isCompact_accumulate
-- 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)
⊢ ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)

Tactic:
have A n : IsCompact (partialSups K n) := by
    simpa [partialSups_eq_accumulate] using isCompact_accumulate hK _
-- 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)
apply :
  ∀ (f : Ultrafilter (FiniteMeasure E))
    (hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f),
    ∃ (x : FiniteMeasure E),
      Membership.mem (γ := Set (FiniteMeasure E))
          {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} x ∧
        (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}

Tactic:
apply isCompact_iff_ultrafilter_le_nhds'.2 (fun f hf ↦ ?_)

Premises used: Iff.mpr, isCompact_iff_ultrafilter_le_nhds'
-- 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 : ℕ
a :
  Membership.mem (γ := Ultrafilter (FiniteMeasure E))
    (Ultrafilter.map (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) f)
    {μ : FiniteMeasure E |
      μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)}
⊢ ∃ (ν : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E))
        {ρ : FiniteMeasure E |
          ρ.mass ≤ C ∧ Eq (α := ℝ≥0) ((ρ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)}
        ν ∧
      (↑(Ultrafilter.map (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) f) : Filter (FiniteMeasure E)) ≤ 𝓝 ν

Tactic:
apply IsCompact.ultrafilter_le_nhds'
        (isCompact_setOf_finiteMeasure_le_of_isCompact C (A n))

Premises used: isCompact_setOf_finiteMeasure_le_of_isCompact, IsCompact.ultrafilter_le_nhds'
-- 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 : ℕ
a :
  {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
⊢ Membership.mem (γ := Ultrafilter (FiniteMeasure E))
    (Ultrafilter.map (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) f)
    {μ : FiniteMeasure E |
      μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)}

Tactic:
simp only [null_iff_toMeasure_null, Ultrafilter.mem_map, preimage_setOf_eq]

Premises used: Ultrafilter.mem_map, Set.preimage_setOf_eq, MeasureTheory.FiniteMeasure.null_iff_toMeasure_null