awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : TopologicalSpace 𝓨
inst_2 : MeasurableSpace 𝓨
inst_3 : OpensMeasurableSpace 𝓨
inst_4 : T2Space 𝓨
hS : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst, inst_1] f
ε : ℝ≥0∞
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : AEMeasurable f μ
⊢ f ⁻¹' (f '' K)ᶜ ⊆ Kᶜ
have pos : K ⊆ f ⁻¹' f '' K
Tactic: simp only [preimage_compl, compl_subset_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (hypothesis)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ≥0∞
hε : 0 < ε
hεbound : ε ≤ 1
⊢ ∃ (k : ℕ), ∀ μ ∈ S, 1 - ε < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)
have εfin : ε ≠ ∞
Tactic: have εfin : ε ≠ ∞ := ne_top_of_le_ne_top (by simp) hεbound
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ≥0∞
hε : 0 < ε
hεbound : ε ≤ 1
εfin : ε ≠ ∞
⊢ ∃ (k : ℕ), ∀ μ ∈ S, 1 - ε < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)
have lift : ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ≥0∞)) (hεbound : (↑ε : ℝ≥0∞) ≤ 1),
  ∃ (k : ℕ), ∀ μ ∈ S, 1 - (↑ε : ℝ≥0∞) < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)
Tactic: lift ε to ℝ≥0 using εfin
Cleared hypotheses: ε, hε, hεbound, εfin
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ≥0
hε : 0 < (↑ε : ℝ≥0∞)
hεbound : (↑ε : ℝ≥0∞) ≤ 1
⊢ ∃ (k : ℕ), ∀ μ ∈ S, 1 - (↑ε : ℝ≥0∞) < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)
have obtain : ∀ (ε : ℝ) (hε' : 0 ≤ ε) (hε : 0 < (↑(NNReal.mk ε hε') : ℝ≥0∞)) (hεbound : (↑(NNReal.mk ε hε') : ℝ≥0∞) ≤ 1),
  ∃ (k : ℕ),
    ∀ μ ∈ S, 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞) < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)
Tactic: obtain ⟨ε, hε', rfl⟩ : ∃ (ε' : ℝ) (hε' : 0 ≤ ε'), ε = .mk ε' hε' := ⟨↑ε, ε.2, rfl⟩
Cleared hypotheses: ε, hε, hεbound
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (hypothesis)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < (↑(NNReal.mk ε hε') : ℝ≥0∞)
hεbound : (↑(NNReal.mk ε hε') : ℝ≥0∞) ≤ 1
⊢ ∃ (k : ℕ),
    ∀ μ ∈ S, 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞) < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)
have hε₁ : 0 < ε
Tactic: simp only [ENNReal.coe_pos, ← NNReal.coe_lt_coe, NNReal.coe_zero, coe_mk, coe_le_one_iff,
      ← NNReal.coe_le_coe, NNReal.coe_one] at hε hεbound
Cleared hypotheses: hε, hεbound
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (hypothesis)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < (↑(NNReal.mk ε hε') : ℝ≥0∞)
hεbound : (↑(NNReal.mk ε hε') : ℝ≥0∞) ≤ 1
hε₁ : 0 < ε
⊢ ∃ (k : ℕ),
    ∀ μ ∈ S, 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞) < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)
have hεbound₁ : ε ≤ 1
Tactic: simp only [ENNReal.coe_pos, ← NNReal.coe_lt_coe, NNReal.coe_zero, coe_mk, coe_le_one_iff,
      ← NNReal.coe_le_coe, NNReal.coe_one] at hε hεbound
Cleared hypotheses: hε, hεbound
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
⊢ ∃ (k : ℕ),
    ∀ μ ∈ S, 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞) < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)
have by_contra! : ∀
  (nh :
    ∀ (k : ℕ),
      ∃ μ ∈ S, (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)),
  False
Tactic: by_contra! nh
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
nh :
  ∀ (k : ℕ),
    ∃ μ ∈ S, (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
⊢ False
have choose : ∀ (μ : (k : ℕ) → ProbabilityMeasure 𝓧) (hμInS : ∀ (k : ℕ), μ k ∈ S)
  (hcontradiction :
    ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)),
  False
Tactic: choose μ hμInS hcontradiction using nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : (k : ℕ) → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction :
  ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
⊢ False
have obtain : ∀ μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S,
  ∀ (sub : ℕ → ℕ) (hsubmono : StrictMono sub) (hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)), False
Tactic: obtain ⟨μlim, _, sub, hsubmono, hμconverges⟩ :=
      hcomp.isSeqCompact (fun n ↦ subset_closure <| hμInS n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (hypothesis)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : (k : ℕ) → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction :
  ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
μlim : ProbabilityMeasure 𝓧
left : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
⊢ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤
    liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop
have hopen : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)
Tactic: have hopen : IsOpen (⋃ i ≤ n, U i) := isOpen_biUnion fun i a ↦ O i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (hypothesis)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : (k : ℕ) → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction :
  ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
μlim : ProbabilityMeasure 𝓧
left : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
hopen : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)
⊢ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤
    liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop
have this : LE.le (α := ℝ≥0∞) (((↑μlim : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i) : ℝ≥0∞)
  (liminf (fun (i : ℕ) ↦ ((↑((μ ∘ sub) i) : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) atTop :
    ℝ≥0∞)
Tactic: have := ProbabilityMeasure.le_liminf_measure_open_of_tendsto hμconverges hopen
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (hypothesis)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : (k : ℕ) → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction :
  ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
μlim : ProbabilityMeasure 𝓧
left : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
hopen : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)
this :
  LE.le (α := ℝ≥0∞) (((↑μlim : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i) : ℝ≥0∞)
    (liminf (fun (i : ℕ) ↦ ((↑((μ ∘ sub) i) : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) atTop :
      ℝ≥0∞)
⊢ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤
    liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop
have this₁ : (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ≥0∞) ≤
  liminf (fun (i : ℕ) ↦ (↑((μ (sub i) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ≥0∞)) atTop
Tactic: simp_rw [Function.comp_apply, ← ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : (k : ℕ) → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction :
  ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
μlim : ProbabilityMeasure 𝓧
left : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
hopen : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)
this :
  (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ≥0∞) ≤
    liminf (fun (i : ℕ) ↦ (↑((μ (sub i) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ≥0∞)) atTop
⊢ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤
    liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop
have rw : ∀
  (this :
    (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ≥0∞) ≤
      (↑(liminf (fun (i : ℕ) ↦ (μ (sub i) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) atTop) : ℝ≥0∞)),
  (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤
    liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop
Tactic: rw [← ofNNReal_liminf] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : (k : ℕ) → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction :
  ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
μlim : ProbabilityMeasure 𝓧
left : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
hopen : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)
this :
  (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ≥0∞) ≤
    liminf (fun (i : ℕ) ↦ (↑((μ (sub i) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ≥0∞)) atTop
rw :
  ∀
    (this :
      (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ≥0∞) ≤
        (↑(liminf (fun (i : ℕ) ↦ (μ (sub i) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) atTop) : ℝ≥0∞)),
    (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤
      liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop
⊢ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤
    liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop
have rw₁ : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) atTop fun (i : ℕ) ↦
  (μ (sub i) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)
Tactic: rw [← ofNNReal_liminf] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : (k : ℕ) → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction :
  ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
μlim : ProbabilityMeasure 𝓧
left : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
hopen : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)
this :
  (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ≥0∞) ≤
    liminf (fun (i : ℕ) ↦ (↑((μ (sub i) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ≥0∞)) atTop
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) atTop fun (i : ℕ) ↦
    (μ (sub i) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)
have h : ∀ (a : ℝ≥0),
  (∀ᶠ (x : ℝ≥0) in Filter.map (fun (i : ℕ) ↦ (μ (sub i) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) atTop,
      (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) x a) →
    (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) 1 a
Tactic: use 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : (k : ℕ) → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction :
  ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
μlim : ProbabilityMeasure 𝓧
left : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
⊢ LE.le (α := ℝ) (liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop)
    (liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ)) atTop)
have h : ∀ᶠ (a : ℕ) in atTop,
  (↑((μ (sub a) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤
    (↑((μ (sub a) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub a), U i)) : ℝ)
Tactic: apply Filter.liminf_le_liminf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : (k : ℕ) → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction :
  ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
μlim : ProbabilityMeasure 𝓧
left : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
h :
  ∀ᶠ (a : ℕ) in atTop,
    (↑((μ (sub a) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤
      (↑((μ (sub a) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub a), U i)) : ℝ)
⊢ LE.le (α := ℝ) (liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop)
    (liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ)) atTop)
have hu : autoParam
  (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) atTop fun (k : ℕ) ↦
    (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ))
  liminf_le_liminf._auto_1
Tactic: apply Filter.liminf_le_liminf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : (k : ℕ) → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction :
  ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
μlim : ProbabilityMeasure 𝓧
left : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
h :
  ∀ᶠ (a : ℕ) in atTop,
    (↑((μ (sub a) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤
      (↑((μ (sub a) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub a), U i)) : ℝ)
hu :
  autoParam
    (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) atTop fun (k : ℕ) ↦
      (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ))
    liminf_le_liminf._auto_1
⊢ LE.le (α := ℝ) (liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop)
    (liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ)) atTop)
have hv : autoParam
  (IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) atTop fun (k : ℕ) ↦
    (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ))
  liminf_le_liminf._auto_3
Tactic: apply Filter.liminf_le_liminf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : (k : ℕ) → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction :
  ∀ (k : ℕ), (↑((μ k : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)
μlim : ProbabilityMeasure 𝓧
left : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
⊢ ∀ᶠ (a : ℕ) in atTop,
    (↑((μ (sub a) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤
      (↑((μ (sub a) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub a), U i)) : ℝ)
have h : ∃ (a : ℕ),
  ∀ (b : ℕ),
    a ≤ b →
      LE.le (α := ℝ≥0) ((μ (sub b) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i) : ℝ≥0)
        ((μ (sub b) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b), U i) : ℝ≥0)
Tactic: simp only [NNReal.coe_le_coe, eventually_atTop, ge_iff_le]