awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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∞) (((↑(F (FiniteMeasure.comap f μ)) : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞)
  (((Measure.map f (↑(FiniteMeasure.comap f μ) : Measure (↑K : Type u_1)) : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
  (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp only [toMeasure_map, F]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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∞)
    (((Measure.map f (↑(FiniteMeasure.comap f μ) : Measure (↑K : Type u_1)) : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞)
  ((((↑(FiniteMeasure.comap f μ) : Measure (↑K : Type u_1)) : Measure (↑K : Type u_1)) :
        (a : Set { x : E // x ∈ K }) → ℝ≥0∞)
      (Subtype.val (p := fun (x : E) ↦ x ∈ K) ⁻¹' s) :
    ℝ≥0∞)
  (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Measure.map_apply measurable_subtype_coe hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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∞)
    (((Measure.comap f (↑μ : Measure E) : Measure (↑K : Type u_1)) : (a : Set { x : E // x ∈ K }) → ℝ≥0∞)
        (Subtype.val (p := fun (x : E) ↦ x ∈ K) ⁻¹' s) :
      ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞)
  (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞)
      (s ∩ range (ι := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K))) :
    ℝ≥0∞)
  (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Measure.comap_apply _ (Subtype.val_injective), image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
h₁ :
  Eq (α := ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞)
        (s ∩ range (ι := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K))) :
      ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap f (↑μ : Measure E) : Measure (↑K : Type u_1)) : (a : Set { x : E // x ∈ K }) → ℝ≥0∞)
        (Subtype.val (p := fun (x : E) ↦ x ∈ K) ⁻¹' s) :
      ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : ∀ (s : Set { x : E // x ∈ K }), MeasurableSet s → MeasurableSet (Subtype.val (p := fun (x : E) ↦ x ∈ K) '' s)
Tactic: rw [Measure.comap_apply _ (Subtype.val_injective), image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
h₁ :
  Eq (α := ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞)
        (s ∩ range (ι := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K))) :
      ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
h₂ : ∀ (s : Set { x : E // x ∈ K }), MeasurableSet s → MeasurableSet (Subtype.val (p := fun (x : E) ↦ x ∈ K) '' s)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap f (↑μ : Measure E) : Measure (↑K : Type u_1)) : (a : Set { x : E // x ∈ K }) → ℝ≥0∞)
        (Subtype.val (p := fun (x : E) ↦ x ∈ K) ⁻¹' s) :
      ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : MeasurableSet (α := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K) ⁻¹' s)
Tactic: rw [Measure.comap_apply _ (Subtype.val_injective), image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞)
        (s ∩ range (ι := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K))) :
      ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∀ᵐ (x : E) ∂(↑μ : Measure E),
  Membership.mem (γ := Set E) (range (ι := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K))) x
Tactic: rw [← Measure.restrict_apply hs, Measure.restrict_eq_self_of_ae_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
⊢ ∀ᵐ (x : E) ∂(↑μ : Measure E),
    Membership.mem (γ := Set E) (range (ι := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K))) x
have h₁ : Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)
Tactic: apply (null_iff_toMeasure_null (↑μ) (range f)ᶜ).mp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)
have h₁ : Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)
Tactic: rw [rf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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}
⊢ F '' T ⊆ {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)}
have 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∞)
Tactic: simp only [null_iff_toMeasure_null, image_subset_iff, preimage_setOf_eq, toMeasure_map,
        setOf_subset_setOf, F, T]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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.map f (↑μ : Measure (↑K : Type u_1)) : Measure E) : (a : Set E) → ℝ≥0∞) Kᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
have h₂ : mass (μ.map f) ≤ C ∧
  Eq (α := ℝ≥0∞) (((↑μ : Measure (↑K : Type u_1)) : (a : Set (↑K : Type u_1)) → ℝ≥0∞) (f ⁻¹' Kᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.map_apply hf.continuous.measurable hK.measurableSet.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (hypothesis)
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}
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)}
have this : {μ : 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]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)}
have rw : IsCompact (F '' T)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
⊢ IsCompact (F '' T)
have apply : IsCompact T
Tactic: apply IsCompact.image _ (by fun_prop)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (hypothesis)
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
⊢ IsCompact T
have this₁ : CompactSpace.{u_1} (↑K : Type u_1)
Tactic: have : CompactSpace K := isCompact_iff_compactSpace.mp hK
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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)
have hd : (↑(Finset.range (n + 1)) : Set ℕ).Pairwise (Disjoint on disjointed K)
Tactic: rw [← biUnion_range_succ_disjointed, FiniteMeasure.restrict_biUnion_finset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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)
⊢ ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
have hm : ∀ (i : ℕ), MeasurableSet (disjointed K i)
Tactic: rw [← biUnion_range_succ_disjointed, FiniteMeasure.restrict_biUnion_finset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (hypothesis)
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
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
have I : ∀ (μ : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (hypothesis)
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)
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
have A : ∀ (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 _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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)
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
have 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
Tactic: apply isCompact_iff_ultrafilter_le_nhds'.2 (fun f hf ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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),
    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)) ≤ 𝓝 ν
have 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)}
Tactic: apply IsCompact.ultrafilter_le_nhds'
        (isCompact_setOf_finiteMeasure_le_of_isCompact C (A n))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 : ℕ
⊢ 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)}
have 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
Tactic: simp only [null_iff_toMeasure_null, Ultrafilter.mem_map, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 : 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
have 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∞)
Tactic: filter_upwards [hf] with ρ hρ