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
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
⊢ (ρ.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∞)
have 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∞)
Tactic: simp only [restrict_mass, restrict_measure_eq,
        Measure.restrict_apply (A n).measurableSet.compl]
-- 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
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∞)
have h₁ : 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, ?_⟩
-- 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
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ Eq (α := ℝ≥0∞)
    (((↑ρ : Measure E) : (a : Set E) → ℝ≥0∞) (((partialSups K : (a : ℕ) → Set E) n)ᶜ ∩ disjointed K n) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have h₁ : Eq (α := Set E) (((partialSups K : (a : ℕ) → Set E) n)ᶜ ∩ disjointed K n : Set E) (∅ : Set E)
Tactic: convert! measure_empty (μ := (ρ : Measure E))
-- 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
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ Eq (α := Set E) (((partialSups K : (a : ℕ) → Set E) n)ᶜ ∩ disjointed K n : Set E) (∅ : Set E)
have h₁ : Disjoint ((partialSups K : (a : ℕ) → Set E) n)ᶜ (disjointed K n)
Tactic: apply disjoint_iff.1
-- 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
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ Disjoint ((partialSups K : (a : ℕ) → Set E) n)ᶜ (disjointed K n)
have h₁ : disjointed K n ≤ (partialSups K : (a : ℕ) → Set E) n
Tactic: apply disjoint_compl_left.mono_right
-- 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),
    (↑ν : 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)) (𝓝 ν)
have 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)) (𝓝 ν)
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 _ _)
-- 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
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),
    ν'.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 ∂ν')
have apply : Eq (α := ℝ≥0∞) (((↑ν : Measure E) : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply Measure.exists_innerRegular_eq_of_isCompact _ (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 : ℕ
ν : 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∞) (((↑ν : Measure E) : (a : Set E) → ℝ≥0∞) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0) ((ν : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
Tactic: rw [← MeasureTheory.FiniteMeasure.null_iff_toMeasure_null]
-- 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
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)) (𝓝 ν)
have 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)) (𝓝 ν)
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
-- 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
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
⊢ ∃ (ν : 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)) (𝓝 ν)
have refine : Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
Tactic: refine ⟨μ, ν'_reg, by simp [μ, ν'K], ?_⟩
-- 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
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
⊢ Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
have apply : ∀ (g : E →ᵇ ℝ),
  Tendsto (β := ℝ)
    (fun (i : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(i.restrict (disjointed K n)) : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)))
Tactic: apply tendsto_of_forall_integral_tendsto (fun g ↦ ?_)
-- 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
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
g : E →ᵇ ℝ
⊢ Tendsto (β := ℝ)
    (fun (i : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(i.restrict (disjointed K n)) : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)))
have h₁ : Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ν : Measure E))
Tactic: convert! tendsto_iff_forall_integral_tendsto.1 ν_lim g using 2
-- 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)
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
⊢ ∃ (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
have M : ∀ (n : ℕ),
  ∃ (ν : 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: have M n : ∃ (ν : FiniteMeasure E), Measure.InnerRegular (ν : Measure E) ∧
      ν (partialSups K n)ᶜ = 0 ∧
      Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) f (𝓝 ν) := by
    -- the existence of a limit follows from the fact that these measures are supported in
    -- the compact set `partialSups K n`.
    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 _ _)
    -- We can find an inner regular measure which coincides with the above limit wrt
    -- integration of bounded continuous functions.
    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
    -- This inner regular measure is also a limit for our ultrafilter
    let μ : FiniteMeasure E := ⟨ν', ν'_fin⟩
    refine ⟨μ, ν'_reg, by simp [μ, ν'K], ?_⟩
    apply tendsto_of_forall_integral_tendsto (fun g ↦ ?_)
    convert! tendsto_iff_forall_integral_tendsto.1 ν_lim g using 2
    exact (hν' g).symm
-- 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
M :
  ∀ (n : ℕ),
    ∃ (ν : 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)) (𝓝 ν)
⊢ ∃ (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
have choose! : ∀ (ν : (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))),
  ∃ (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: choose! ν ν_reg νK hν using M
Cleared hypotheses: M
-- 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
ν_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))
⊢ ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
have simp : ∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
Tactic: simp only [MeasurableSet.univ, Measure.sum_apply]