awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ),
    ∀ (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)
have 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)
Tactic: use n + 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 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)
have h : ∀ (i : ℕ) (hi : i ≤ n), n ≤ sub b
Tactic: refine (μ (sub b)).apply_mono
            <| Set.biUnion_mono (fun i (hi : i ≤ n) ↦ hi.trans ?_) fun _ _ ↦ le_rfl
-- 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 : ℕ
⊢ 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
have 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
Tactic: use 0
-- 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 : ℕ
⊢ 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
have 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
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 : ℕ
⊢ liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ)) atTop ≤ 1 - ε
have 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
Tactic: apply Filter.liminf_le_of_le
-- 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 : ℕ
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
⊢ liminf (fun (k : ℕ) ↦ (↑((μ (sub k) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub k), U i)) : ℝ)) atTop ≤ 1 - ε
have h : ∀ (b : ℝ),
  (∀ᶠ (n : ℕ) in atTop, b ≤ (↑((μ (sub n) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub n), U i)) : ℝ)) → b ≤ 1 - ε
Tactic: apply Filter.liminf_le_of_le
-- 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 : ℕ
⊢ 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
have 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
Tactic: use 0
-- 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 : ℕ
⊢ ∀ (b : ℝ),
    (∀ᶠ (n : ℕ) in atTop, b ≤ (↑((μ (sub n) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub n), U i)) : ℝ)) → b ≤ 1 - ε
have 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 - ε
Tactic: simp only [eventually_atTop, ge_iff_le, forall_exists_index]
-- 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 : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
⊢ b ≤ 1 - ε
have h₁ : (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ) ≤ 1 - ε
Tactic: apply le_trans (h c le_rfl)
-- 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 : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
⊢ (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ) ≤ 1 - ε
have h₁ : ENNReal.ofReal (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ) ≤ ENNReal.ofReal (1 - ε)
Tactic: refine (ofReal_le_ofReal_iff (by rw [sub_nonneg]; exact hεbound)).mp ?_
-- 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 : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
⊢ ENNReal.ofReal (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ) ≤ ENNReal.ofReal (1 - ε)
have h₁ : (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ≥0∞) ≤ ENNReal.ofReal (1 - ε)
Tactic: rw [ofReal_coe_nnreal]
-- 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 : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
⊢ (↑((μ (sub c) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub c), U i)) : ℝ≥0∞) ≤ ENNReal.ofReal (1 - ε)
have h₁ : 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞) ≤ ENNReal.ofReal (1 - ε)
Tactic: apply le_trans (hcontradiction (sub c))
-- 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 : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ (↑((μ (sub b_1) : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ sub b_1), U i)) : ℝ)
⊢ 1 - (↑(NNReal.mk ε hε') : ℝ≥0∞) ≤ ENNReal.ofReal (1 - ε)
have h₁ : (↑(1 - NNReal.mk ε hε') : ℝ≥0∞) ≤ (↑(1 - NNReal.mk ε hε') : ℝ≥0∞)
Tactic: norm_cast
-- 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)
⊢ False
have Measurebound : ∀ (n : ℕ), (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤ 1 - ε
Tactic: have Measurebound n : (μlim (⋃ (i ≤ n), U i) : ℝ) ≤ 1 - ε := calc
    (μlim (⋃ (i ≤ n), U i) : ℝ)
    _ ≤ liminf (fun k ↦ (μ (sub k) (⋃ (i ≤ n), U i) : ℝ)) atTop := by
      have hopen : IsOpen (⋃ i ≤ n, U i) := isOpen_biUnion fun i a ↦ O i
      have := ProbabilityMeasure.le_liminf_measure_open_of_tendsto hμconverges hopen
      simp_rw [Function.comp_apply, ← ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure] at this
      rw [← ofNNReal_liminf] at this
      · exact mod_cast this
      use 1
      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)
    _ ≤ liminf (fun k ↦ (μ (sub k) (⋃ (i ≤ sub k), U i) : ℝ)) atTop := by
      apply Filter.liminf_le_liminf
      · simp only [NNReal.coe_le_coe, eventually_atTop, ge_iff_le]
        use n + 1
        intro b hypo
        refine (μ (sub b)).apply_mono
            <| Set.biUnion_mono (fun i (hi : i ≤ n) ↦ hi.trans ?_) fun _ _ ↦ le_rfl
        exact le_trans (Nat.le_add_right n 1) (le_trans hypo (StrictMono.le_apply hsubmono))
      · use 0; simp
      · use 1
        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)
    _ ≤ 1 - ε := by
      apply Filter.liminf_le_of_le
      · use 0; simp
      simp only [eventually_atTop, ge_iff_le, forall_exists_index]
      intro b c h
      apply le_trans (h c le_rfl)
      refine (ofReal_le_ofReal_iff (by rw [sub_nonneg]; exact hεbound)).mp ?_
      rw [ofReal_coe_nnreal]
      apply le_trans (hcontradiction (sub c))
      norm_cast
-- 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)
Measurebound : ∀ (n : ℕ), (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤ 1 - ε
⊢ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i) : ℝ≥0)) atTop
    (𝓝 ((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), U i)) : Filter ℝ≥0)
have simp_rw : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ((μlim : (a : Set 𝓧) → ℝ≥0) (accumulate U n) : ℝ≥0)) atTop
  (𝓝 ((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), U i)) : Filter ℝ≥0)
Tactic: simp_rw [← Set.accumulate_def, ProbabilityMeasure.tendsto_measure_iUnion_accumulate]
-- 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)
Measurebound : ∀ (n : ℕ), (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤ 1 - ε
⊢ False
have accumulation : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i) : ℝ≥0)) atTop
  (𝓝 ((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), U i)) : Filter ℝ≥0)
Tactic: have accumulation : Tendsto (fun n ↦ μlim (⋃ i ≤ n, U i)) atTop (𝓝 (μlim (⋃ i, U i))) := by
    simp_rw [← Set.accumulate_def, ProbabilityMeasure.tendsto_measure_iUnion_accumulate]
-- 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)
Measurebound : ∀ (n : ℕ), (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ) ≤ 1 - ε
accumulation :
  Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i) : ℝ≥0)) atTop
    (𝓝 ((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), U i)) : Filter ℝ≥0)
⊢ False
have accumulation₁ : Tendsto (fun (a : ℕ) ↦ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ a), U i)) : ℝ)) atTop (𝓝 (↑1 : ℝ))
Tactic: rw [Cov, coeFn_univ, ← NNReal.tendsto_coe] at accumulation
Cleared hypotheses: accumulation