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)
ε : ℝ
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
h : ∀ (i : ℕ) (hi : i ≤ n), n ≤ sub 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:
refine (μ (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
-- 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
i : ℕ
hi : i ≤ n
⊢ n ≤ sub b

Tactic:
le_trans (Nat.le_add_right n 1) (le_trans hypo (StrictMono.le_apply hsubmono))

Premises used: StrictMono.le_apply, Nat.le_add_right, OfNat.ofNat, le_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 b : ℕ
hypo : n + 1 ≤ b
i : ℕ
hi : i ≤ n
⊢ n ≤ sub b

Tactic:
exact le_trans (Nat.le_add_right n 1) (le_trans hypo (StrictMono.le_apply hsubmono))

Premises used: StrictMono.le_apply, Nat.le_add_right, OfNat.ofNat, le_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 : ℕ
h :
  ∀ᶠ (x : ℝ) in
    Filter.map (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop,
    (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) x 0
⊢ 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:
use 0
-- 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 : ℕ
⊢ ∀ᶠ (x : ℝ) in
    Filter.map (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)) atTop,
    (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) x 0

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 : ℕ
h :
  ∀ (a : ℝ),
    (∀ᶠ (x : ℝ) in
        Filter.map (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ)) atTop,
        (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) x a) →
      (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) 1 a
⊢ 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:
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 : ℕ
x : ℝ
d : ℕ
hyp : ∀ (b : ℕ), d ≤ b → x ≤ (↑((μ (sub b) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b), U i)) : ℝ)
⊢ d ≤ d

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 : ℕ
x : ℝ
d : ℕ
hyp : ∀ (b : ℕ), d ≤ b → x ≤ (↑((μ (sub b) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b), U i)) : ℝ)
⊢ (↑((μ (sub d) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub d), U i)) : ℝ) ≤ 1

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 : ℕ
⊢ ∀ (a : ℝ),
    (∀ᶠ (x : ℝ) in
        Filter.map (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ)) atTop,
        (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) x a) →
      (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) 1 a

Tactic:
simpa [ge_iff_le, eventually_map, eventually_atTop, ge_iff_le, forall_exists_index] using
            fun _ d hyp ↦ (hyp d (by simp)).trans (by simp)

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 : ℕ
hf :
  autoParam
    (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) atTop fun (k : ℕ) ↦
      (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ))
    liminf_le_of_le._auto_1
h :
  ∀ (b : ℝ),
    (∀ᶠ (n : ℕ) in atTop, b ≤ (↑((μ (sub n) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub n), U i)) : ℝ)) → b ≤ 1 - ε
⊢ liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ)) atTop ≤ 1 - ε

Tactic:
apply Filter.liminf_le_of_le

Premises used: Filter.liminf_le_of_le
-- 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 :
  ∀ᶠ (x : ℝ) in
    Filter.map (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ)) atTop,
    (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) x 0
⊢ autoParam
    (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) atTop fun (k : ℕ) ↦
      (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ))
    liminf_le_of_le._auto_1

Tactic:
use 0
-- 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 : ℕ
⊢ ∀ᶠ (x : ℝ) in
    Filter.map (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ)) atTop,
    (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) x 0

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 : ℕ
h :
  ∀ (b : ℝ) (x : ℕ)
    (h : ∀ (b_1 : ℕ), x ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)),
    b ≤ 1 - ε
⊢ ∀ (b : ℝ),
    (∀ᶠ (n : ℕ) in atTop, b ≤ (↑((μ (sub n) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub n), U i)) : ℝ)) → b ≤ 1 - ε

Tactic:
simp only [eventually_atTop, ge_iff_le, forall_exists_index]

Premises used: ge_iff_le, forall_exists_index, 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 : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
h₁ : (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ) ≤ 1 - ε
⊢ b ≤ 1 - ε

Tactic:
apply le_trans (h c le_rfl)

Premises used: le_rfl, le_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 : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
rw : ε ≤ 1
⊢ 0 ≤ 1 - ε

Tactic:
rw [sub_nonneg]

Premises used: sub_nonneg
-- 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 : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
⊢ ε ≤ 1

Tactic:
hεbound
-- 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 : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
⊢ ε ≤ 1

Tactic:
exact hεbound
-- 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 : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
h₁ :
  ENNReal.ofReal (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ) ≤ ENNReal.ofReal (1 - ε)
⊢ (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ) ≤ 1 - ε

Tactic:
refine (ofReal_le_ofReal_iff (by rw [sub_nonneg]; exact hεbound)).mp ?_

Premises used: ENNReal.ofReal_le_ofReal_iff, Iff.mp
-- 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 : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
h₁ : (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ≥0∞) ≤ ENNReal.ofReal (1 - ε)
⊢ ENNReal.ofReal (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ) ≤ ENNReal.ofReal (1 - ε)

Tactic:
rw [ofReal_coe_nnreal]

Premises used: ENNReal.ofReal_coe_nnreal
-- 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 : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
h₁ : 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞) ≤ ENNReal.ofReal (1 - ε)
⊢ (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ≥0∞) ≤ ENNReal.ofReal (1 - ε)

Tactic:
apply le_trans (hcontradiction (sub c))

Premises used: le_trans