awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
hμ : μ.mass = 1
h'μ : ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
ν : ProbabilityMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (↑μ : Measure E) ⋯
this : ν.toFiniteMeasure = μ
⊢ ∃ (x : ProbabilityMeasure E), (∀ (n : ℕ), (x : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n) ∧ x.toFiniteMeasure = μ

Tactic:
exact ⟨ν, by simpa [← this] using h'μ , this⟩
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
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}

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⟩
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
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}
rw :
  IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : 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})

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
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)
    {μ : FiniteMeasure E | μ.mass = 1 ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}

Tactic:
isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le 1 hu hK h

Premises used: isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
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)
    {μ : FiniteMeasure E | μ.mass = 1 ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}

Tactic:
exact isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le 1 hu hK h

Premises used: isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le, OfNat.ofNat
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
⊢ ∃ (u : ℕ → ℝ≥0), StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto 0

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- 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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
obtain :
  ∀ (u : ℕ → ℝ≥0) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)),
    IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
⊢ 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

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- 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
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 : ℕ
norm_cast : 0 < u n
⊢ 0 < (↑(u n) : ℝ≥0∞)

Tactic:
norm_cast
-- 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
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

Tactic:
u_pos n
-- 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
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

Tactic:
exact u_pos n
-- 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
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 : ℕ
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
⊢ ∃ (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⟩

Premises used: ENNReal.ofNNReal, MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le, Iff.mp
-- 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
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

Tactic:
⟨K, K_comp, fun μ hμ ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
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∞)
refine : ∀ (μ : ProbabilityMeasure E) (hμ : μ ∈ S), (μ : (a : Set E) → ℝ≥0) Kᶜ ≤ u n
⊢ ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) Kᶜ ≤ u n

Tactic:
refine ⟨K, K_comp, fun μ hμ ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
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
⊢ ((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) Kᶜ ≤ (↑(u n) : ℝ≥0∞)

Tactic:
have : (μ : Measure E) Kᶜ ≤ u n := hK _ ⟨μ, hμ, rfl⟩
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
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
this : ((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) Kᶜ ≤ (↑(u n) : ℝ≥0∞)
⊢ (↑((μ : (a : Set E) → ℝ≥0) Kᶜ) : ℝ≥0∞) ≤ (↑(u n) : ℝ≥0∞)

Tactic:
simpa using 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
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
this : ((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) Kᶜ ≤ (↑(u n) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0) Kᶜ ≤ u n

Tactic:
exact ENNReal.coe_le_coe.1 (by simpa using this)

Premises used: ENNReal.coe_le_coe, Iff.mp
-- 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
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

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)
-- 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
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
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)
⊢ IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)

Tactic:
choose K K_comp hK using A
-- 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
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)
h : NormalSpace E ∨ Monotone K'
⊢ IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}

Tactic:
apply isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le u_lim

Premises used: isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le
-- 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
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
⊢ ∀ (n : ℕ), IsCompact (K' n)

Tactic:
fun n ↦ (finite_Iic n).isCompact_biUnion (fun i hi ↦ K_comp i)

Premises used: Set.finite_Iic, Set.Finite.isCompact_biUnion
-- 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
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
⊢ ∀ (n : ℕ), IsCompact (K' n)

Tactic:
exact fun n ↦ (finite_Iic n).isCompact_biUnion (fun i hi ↦ K_comp i)

Premises used: Set.finite_Iic, Set.Finite.isCompact_biUnion
-- 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
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 : Monotone K'
⊢ NormalSpace E ∨ Monotone K'

Tactic:
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
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 : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (i : ℕ) (i_1 : i ≤ a), K i ⊆ ⋃ (i : ℕ), ⋃ (_ : i ≤ b), K i
⊢ Monotone K'

Tactic:
simp only [Monotone, mem_Iic, le_eq_subset, iUnion_subset_iff, K']

Premises used: Set.iUnion_subset_iff, Set.le_eq_subset, Monotone, Set.mem_Iic
-- 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
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
h : Membership.mem (γ := Set ℕ) (fun (x : ℕ) ↦ x.le b) i
⊢ K i ⊆ ⋃ (i : ℕ), ⋃ (_ : i ≤ b), K i

Tactic:
apply subset_biUnion_of_mem

Premises used: Set.subset_biUnion_of_mem
-- 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
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
⊢ Membership.mem (γ := Set ℕ) (fun (x : ℕ) ↦ x.le b) i

Tactic:
hi.trans hab

Premises used: Set.Mem, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
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
⊢ Membership.mem (γ := Set ℕ) (fun (x : ℕ) ↦ x.le b) i

Tactic:
exact hi.trans hab

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
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}

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
-- 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
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}
apply : S ⊆ {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
⊢ IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)

Tactic:
apply IsCompact.closure_of_subset h'K

Premises used: IsCompact.closure_of_subset
-- 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
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 : ℕ
h : K n ⊆ K' n
⊢ LE.le (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (K' n)ᶜ : ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (K n)ᶜ : ℝ≥0)

Tactic:
gcongr
-- 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
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 : ℕ
h : K n ⊆ ⋃ (i : ℕ), ⋃ (_ : i ≤ n), K i
⊢ K n ⊆ K' n

Tactic:
simp only [mem_Iic, K']

Premises used: Set.mem_Iic
-- 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
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 : ℕ
h : Membership.mem (γ := Set ℕ) (fun (x : ℕ) ↦ x.le n) n
⊢ K n ⊆ ⋃ (i : ℕ), ⋃ (_ : i ≤ n), K i

Tactic:
apply subset_biUnion_of_mem

Premises used: Set.subset_biUnion_of_mem
-- 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
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 : ℕ
⊢ Membership.mem (γ := Set ℕ) (fun (x : ℕ) ↦ x.le n) n

Tactic:
le_rfl (a := n)

Premises used: le_rfl, Set.Mem