awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
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∞)
⊢ ∃ (k : ℕ), ∀ μ ∈ S, 1 - (↑ε : ℝ≥0∞) < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)

Tactic:
obtain ⟨ε, hε', rfl⟩ : ∃ (ε' : ℝ) (hε' : 0 ≤ ε'), ε = .mk ε' hε' := ⟨↑ε, ε.2, rfl⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
⊢ 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

Premises used: NNReal.coe_zero, NNReal.coe_mk, ENNReal.coe_le_one_iff, ENNReal.coe_pos, NNReal.coe_lt_coe, NNReal.coe_one, NNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 < ε
⊢ ε ≤ 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

Premises used: NNReal.coe_zero, NNReal.coe_mk, ENNReal.coe_le_one_iff, ENNReal.coe_pos, NNReal.coe_lt_coe, NNReal.coe_one, NNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
by_contra! :
  ∀
    (nh :
      ∀ (k : ℕ),
        ∃ μ ∈ S, (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞) ≤ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞)),
    False
⊢ ∃ (k : ℕ),
    ∀ μ ∈ S, 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞) < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)

Tactic:
by_contra! nh
-- Module: Mathlib.MeasureTheory.Measure.Tight
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∞)
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
⊢ False

Tactic:
choose μ hμInS hcontradiction using nh
-- Module: Mathlib.MeasureTheory.Measure.Tight
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∞)
obtain :
  ∀ μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S,
    ∀ (sub : ℕ → ℕ) (hsubmono : StrictMono sub) (hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)), False
⊢ False

Tactic:
obtain ⟨μlim, _, sub, hsubmono, hμconverges⟩ :=
      hcomp.isSeqCompact (fun n ↦ subset_closure <| hμInS n)

Premises used: subset_closure, IsCompact.isSeqCompact
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 : ℕ
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)

Tactic:
have hopen : IsOpen (⋃ i ≤ n, U i) := isOpen_biUnion fun i a ↦ O i
-- Module: Mathlib.MeasureTheory.Measure.Tight
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)
⊢ 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
-- Module: Mathlib.MeasureTheory.Measure.Tight
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)) : ℝ≥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

Premises used: MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
rw₁ :
  IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) atTop fun (i : ℕ) ↦
    (μ (sub i) : (a : Set 𝓧) → ℝ≥0) (⋃ (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

Tactic:
rw [← ofNNReal_liminf] at this

Premises used: ENNReal.ofNNReal_liminf
-- Module: Mathlib.MeasureTheory.Measure.Tight
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)) 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:
mod_cast this

Premises used: congrArg, NNReal.coe_le_coe._simp_1, cast, LE.le, ENNReal.coe_le_coe._simp_1, Eq.symm, NNReal.toReal_liminf, DFunLike.coe, NNReal.toReal, Set.iUnion, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Tight
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)) 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:
exact mod_cast this
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
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
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) atTop fun (i : ℕ) ↦
    (μ (sub i) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)

Tactic:
use 1
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
x_1 : ℝ≥0
x : ℕ
h : ∀ (b : ℕ), x ≤ b → x_1 ≤ (μ (sub b) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)
⊢ x ≤ x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
⊢ ∀ (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:
simpa [ge_iff_le, eventually_map, eventually_atTop, forall_exists_index] using fun _ x h ↦
          (h x (by simp)).trans <| ProbabilityMeasure.apply_le_one (μ (sub x)) (⋃ i ≤ n, U i)

Premises used: ge_iff_le, forall_exists_index, Filter.eventually_map, Filter.eventually_atTop
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
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
⊢ 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)

Tactic:
apply Filter.liminf_le_liminf

Premises used: Filter.liminf_le_liminf
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 : ℕ),
    ∀ (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)
⊢ ∀ᶠ (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:
simp only [NNReal.coe_le_coe, eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.eventually_atTop, NNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 :
  ∀ (b : ℕ),
    n + 1 ≤ 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)
⊢ ∃ (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:
use n + 1
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 b : ℕ
hypo : n + 1 ≤ 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:
(μ (sub b)).apply_mono
            <| Set.biUnion_mono (fun i (hi : i ≤ n) ↦ hi.trans ?_) fun _ _ ↦ le_rfl

Premises used: le_rfl, MeasureTheory.ProbabilityMeasure.apply_mono, Set.biUnion_mono, LE.le.trans