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
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})
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
have rw : IsCompact.{u_1} (X := FiniteMeasure E)
  ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
    {μ : FiniteMeasure E | μ.mass = C})
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
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})
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
      {μ : FiniteMeasure E | μ.mass = C})
have apply : IsClosed[instTopologicalSpace] {μ : FiniteMeasure E | μ.mass = C}
Tactic: apply IsCompact.inter_right (isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le C hu hK h)
-- 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
⊢ IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
have apply : IsCompact.{u_1} (X := FiniteMeasure E)
  (ProbabilityMeasure.toFiniteMeasure '' {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n})
Tactic: apply (ProbabilityMeasure.toFiniteMeasure_isEmbedding E).isCompact_iff.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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
⊢ 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}
have 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} μ
Tactic: ext μ
-- 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
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
have 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
Tactic: refine ⟨?_, ?_⟩
-- 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
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
⊢ (∃ (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
have 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 = μ
Tactic: refine ⟨?_, ?_⟩
-- 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
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 = μ
have 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∞)
Tactic: ext
-- 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
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) ⋯
⊢ ∃ (x : ProbabilityMeasure E), (∀ (n : ℕ), (x : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n) ∧ x.toFiniteMeasure = μ
have this : ν.toFiniteMeasure = μ
Tactic: have : ν.toFiniteMeasure = μ := by ext; rfl
-- 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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    (ProbabilityMeasure.toFiniteMeasure '' {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n})
have this : 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: have : ProbabilityMeasure.toFiniteMeasure '' {μ | ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
      = {μ : FiniteMeasure E | μ.mass = 1 ∧ ∀ n, μ (K n)ᶜ ≤ u n} := by
    ext μ
    simp only [mem_image, mem_setOf_eq]
    refine ⟨?_, ?_⟩
    · rintro ⟨ν, hν, rfl⟩
      simpa using hν
    · rintro ⟨hμ, h'μ⟩
      let ν : ProbabilityMeasure E := ⟨μ, isProbabilityMeasure_iff_real.2 (by simpa using hμ)⟩
      have : ν.toFiniteMeasure = μ := by ext; rfl
      exact ⟨ν, by simpa [← this] using h'μ , 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
u : ℕ → ℝ≥0
K : ℕ → Set E
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
this :
  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}
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    (ProbabilityMeasure.toFiniteMeasure '' {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n})
have rw : IsCompact.{u_1} (X := FiniteMeasure E)
  {μ : FiniteMeasure E | μ.mass = 1 ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
⊢ IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
have obtain : ∀ (u : ℕ → ℝ≥0) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)),
  IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
Tactic: obtain ⟨u, -, u_pos, u_lim⟩ :
      ∃ u : ℕ → ℝ≥0, StrictAnti u ∧ (∀ n, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto 0
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
n : ℕ
⊢ 0 < (↑(u n) : ℝ≥0∞)
have norm_cast : 0 < u n
Tactic: norm_cast
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
n : ℕ
⊢ ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) Kᶜ ≤ u n
have rcases : ∀ (K : Set E) (K_comp : IsCompact K)
  (hK :
    ∀ (μ : Measure E),
      Membership.mem (γ := Set (Measure E)) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x} μ →
        (μ : (a : Set E) → ℝ≥0∞) Kᶜ ≤ (↑(u n) : ℝ≥0∞)),
  ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) Kᶜ ≤ u n
Tactic: rcases isTightMeasureSet_iff_exists_isCompact_measure_compl_le.1 hS (u n)
      (by norm_cast; exact u_pos n) with ⟨K, K_comp, 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
n : ℕ
K : Set E
K_comp : IsCompact K
hK :
  ∀ (μ : Measure E),
    Membership.mem (γ := Set (Measure E)) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x} μ →
      (μ : (a : Set E) → ℝ≥0∞) Kᶜ ≤ (↑(u n) : ℝ≥0∞)
⊢ ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) Kᶜ ≤ u n
have refine : ∀ (μ : ProbabilityMeasure E) (hμ : μ ∈ S), (μ : (a : Set E) → ℝ≥0) Kᶜ ≤ u n
Tactic: refine ⟨K, K_comp, fun μ hμ ↦ ?_⟩
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
n : ℕ
K : Set E
K_comp : IsCompact K
hK :
  ∀ (μ : Measure E),
    Membership.mem (γ := Set (Measure E)) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x} μ →
      (μ : (a : Set E) → ℝ≥0∞) Kᶜ ≤ (↑(u n) : ℝ≥0∞)
μ : ProbabilityMeasure E
hμ : μ ∈ S
⊢ (μ : (a : Set E) → ℝ≥0) Kᶜ ≤ u n
have this : ((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) Kᶜ ≤ (↑(u n) : ℝ≥0∞)
Tactic: have : (μ : Measure E) Kᶜ ≤ u n := hK _ ⟨μ, hμ, rfl⟩
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
have A : ∀ (n : ℕ), ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) Kᶜ ≤ u n
Tactic: have A n : ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ u n := by
    rcases isTightMeasureSet_iff_exists_isCompact_measure_compl_le.1 hS (u n)
      (by norm_cast; exact u_pos n) with ⟨K, K_comp, hK⟩
    refine ⟨K, K_comp, fun μ hμ ↦ ?_⟩
    have : (μ : Measure E) Kᶜ ≤ u n := hK _ ⟨μ, hμ, rfl⟩
    exact ENNReal.coe_le_coe.1 (by simpa using 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
A : ∀ (n : ℕ), ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) Kᶜ ≤ u n
⊢ IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
have choose : ∀ (K : (n : ℕ) → Set E) (K_comp : ∀ (n : ℕ), IsCompact (K n))
  (hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n),
  IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
Tactic: choose K K_comp hK using A
Cleared hypotheses: A
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
⊢ IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
have hK₁ : ∀ (n : ℕ), IsCompact (K' n)
Tactic: apply isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le u_lim
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
hK₁ : ∀ (n : ℕ), IsCompact (K' n)
⊢ IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
have h : NormalSpace E ∨ Monotone K'
Tactic: apply isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le u_lim
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
⊢ NormalSpace E ∨ Monotone K'
have h : Monotone K'
Tactic: 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
⊢ Monotone K'
have h : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (i : ℕ) (i_1 : i ≤ a), K i ⊆ ⋃ (i : ℕ), ⋃ (_ : i ≤ b), K i
Tactic: simp only [Monotone, mem_Iic, le_eq_subset, iUnion_subset_iff, 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
a b : ℕ
hab : a ≤ b
i : ℕ
hi : i ≤ a
⊢ K i ⊆ ⋃ (i : ℕ), ⋃ (_ : i ≤ b), K i
have h : Membership.mem (γ := Set ℕ) (fun (x : ℕ) ↦ x.le b) i
Tactic: apply subset_biUnion_of_mem
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
⊢ IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
have h'K : IsCompact.{u_1} (X := ProbabilityMeasure E)
  {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
Tactic: have h'K : IsCompact {μ : ProbabilityMeasure E | ∀ n, μ (K' n)ᶜ ≤ u n} := by
    apply isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le u_lim
    · exact fun n ↦ (finite_Iic n).isCompact_biUnion (fun i hi ↦ K_comp i)
    · right
      simp only [Monotone, mem_Iic, le_eq_subset, iUnion_subset_iff, K']
      intro a b hab i hi
      apply subset_biUnion_of_mem
      exact hi.trans hab
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
h'K :
  IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
⊢ IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
have apply : S ⊆ {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
Tactic: apply IsCompact.closure_of_subset h'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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
h'K :
  IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
μ : ProbabilityMeasure E
hμ : μ ∈ S
n : ℕ
⊢ LE.le (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (K' n)ᶜ : ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (K n)ᶜ : ℝ≥0)
have h : K n ⊆ K' n
Tactic: gcongr
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
h'K :
  IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
μ : ProbabilityMeasure E
hμ : μ ∈ S
n : ℕ
⊢ K n ⊆ K' n
have h : K n ⊆ ⋃ (i : ℕ), ⋃ (_ : i ≤ n), K i
Tactic: simp only [mem_Iic, 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
h'K :
  IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
μ : ProbabilityMeasure E
hμ : μ ∈ S
n : ℕ
⊢ K n ⊆ ⋃ (i : ℕ), ⋃ (_ : i ≤ n), K i
have h : Membership.mem (γ := Set ℕ) (fun (x : ℕ) ↦ x.le n) n
Tactic: apply subset_biUnion_of_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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
h'K :
  IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
μ : ProbabilityMeasure E
hμ : μ ∈ S
n : ℕ
⊢ (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n
have calc : LE.le (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (K' n)ᶜ : ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (K n)ᶜ : ℝ≥0)
Tactic: calc μ (K' n)ᶜ
  _ ≤ μ (K n)ᶜ := by
    gcongr
    simp only [mem_Iic, K']
    apply subset_biUnion_of_mem
    exact le_rfl (a := n)
  _ ≤ u n := by grind
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
h'K :
  IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
μ : ProbabilityMeasure E
hμ : μ ∈ S
n : ℕ
calc : LE.le (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (K' n)ᶜ : ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (K n)ᶜ : ℝ≥0)
⊢ (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n
have calc₁ : (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
Tactic: calc μ (K' n)ᶜ
  _ ≤ μ (K n)ᶜ := by
    gcongr
    simp only [mem_Iic, K']
    apply subset_biUnion_of_mem
    exact le_rfl (a := n)
  _ ≤ u n := by grind