awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (fun (a : ℕ) ↦ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ a), U i)) : ℝ)) atTop (𝓝 (↑1 : ℝ))
⊢ False
have exceeds_bound : ∀ᶠ (n : ℕ) in atTop, 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)
Tactic: have exceeds_bound : ∀ᶠ n in atTop, (1 - ε / 2 : ℝ) ≤ μlim (⋃ i ≤ n, U i) :=
      Tendsto.eventually_const_le (v := 1)
        (by simp only [sub_lt_self_iff, Nat.ofNat_pos, div_pos_iff_of_pos_right]; positivity)
        accumulation
-- 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 - ε
accumulation :
  Tendsto (fun (a : ℕ) ↦ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ a), U i)) : ℝ)) atTop (𝓝 (↑1 : ℝ))
exceeds_bound : ∀ᶠ (n : ℕ) in atTop, 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)
⊢ False
have suffices : ∀ᶠ (n : ℕ) in atTop, False
Tactic: suffices ∀ᶠ n : ℕ in atTop, False from this.exists.choose_spec
-- 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 - ε
accumulation :
  Tendsto (fun (a : ℕ) ↦ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ a), U i)) : ℝ)) atTop (𝓝 (↑1 : ℝ))
exceeds_bound : ∀ᶠ (n : ℕ) in atTop, 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, False
have h : ∀ (n : ℕ) (hn : 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)), False
Tactic: filter_upwards [exceeds_bound] with n hn
-- 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 - ε
accumulation :
  Tendsto (fun (a : ℕ) ↦ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ a), U i)) : ℝ)) atTop (𝓝 (↑1 : ℝ))
exceeds_bound : ∀ᶠ (n : ℕ) in atTop, 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)
n : ℕ
hn : 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)
⊢ False
have linarith : 2 / 2 = 1
Tactic: linarith [hn.trans <| Measurebound n]
-- 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 - ε
accumulation :
  Tendsto (fun (a : ℕ) ↦ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ a), U i)) : ℝ)) atTop (𝓝 (↑1 : ℝ))
exceeds_bound : ∀ᶠ (n : ℕ) in atTop, 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)
n : ℕ
hn : 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)
linarith : 2 / 2 = 1
⊢ False
have linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hn.trans <| Measurebound n]
-- 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 - ε
accumulation :
  Tendsto (fun (a : ℕ) ↦ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ a), U i)) : ℝ)) atTop (𝓝 (↑1 : ℝ))
exceeds_bound : ∀ᶠ (n : ℕ) in atTop, 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)
n : ℕ
hn : 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
⊢ False
have linarith₂ : GT.gt (α := ℝ) 2 0
Tactic: linarith [hn.trans <| Measurebound n]
-- 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 - ε
accumulation :
  Tendsto (fun (a : ℕ) ↦ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ a), U i)) : ℝ)) atTop (𝓝 (↑1 : ℝ))
exceeds_bound : ∀ᶠ (n : ℕ) in atTop, 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)
n : ℕ
hn : 1 - ε / 2 ≤ (↑((μlim : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), U i)) : ℝ)
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
⊢ False
have linarith₆ : 0 - ε + (HMul.hMul (α := ℝ) 2 1 - 1 * ε - (HMul.hMul (α := ℝ) 2 1 - 2 * ε)) = 0
Tactic: linarith [hn.trans <| Measurebound n]
-- 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
⊢ IsTightMeasureSet.{u_1} (𝓧 := 𝓧) (m𝓧 := m𝓧) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x}
have rw : ∀ (ε : ℝ≥0∞),
  0 < ε →
    ∃ (K : Set 𝓧),
      IsCompact K ∧
        ∀ (μ : Measure 𝓧),
          Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
            (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: rw [isTightMeasureSet_iff_exists_isCompact_measure_compl_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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
⊢ ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (K : Set 𝓧),
        IsCompact K ∧
          ∀ (μ : Measure 𝓧),
            Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
              (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have inl : ∀ (hempty : IsEmpty 𝓧) (ε : ℝ≥0∞),
  0 < ε →
    ∃ (K : Set 𝓧),
      IsCompact K ∧
        ∀ (μ : Measure 𝓧),
          Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
            (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: rcases isEmpty_or_nonempty 𝓧 with hempty | hnonempty
-- 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
inl :
  ∀ (hempty : IsEmpty 𝓧) (ε : ℝ≥0∞),
    0 < ε →
      ∃ (K : Set 𝓧),
        IsCompact K ∧
          ∀ (μ : Measure 𝓧),
            Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
              (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
⊢ ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (K : Set 𝓧),
        IsCompact K ∧
          ∀ (μ : Measure 𝓧),
            Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
              (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have inr : ∀ (hnonempty : Nonempty 𝓧) (ε : ℝ≥0∞),
  0 < ε →
    ∃ (K : Set 𝓧),
      IsCompact K ∧
        ∀ (μ : Measure 𝓧),
          Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
            (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: rcases isEmpty_or_nonempty 𝓧 with hempty | hnonempty
-- 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hempty : IsEmpty 𝓧
⊢ ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (K : Set 𝓧),
        IsCompact K ∧
          ∀ (μ : Measure 𝓧),
            Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
              (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have hempty₁ : Eq.{u_1 + 1} (α := Set 𝓧) univ ∅
Tactic: rw [← univ_eq_empty_iff] at hempty
Cleared hypotheses: hempty
-- 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
⊢ ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (K : Set 𝓧),
        IsCompact K ∧
          ∀ (μ : Measure 𝓧),
            Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
              (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have inr : ∀ (D : ℕ → 𝓧) (hD : DenseRange D) (ε : ℝ≥0∞),
  0 < ε →
    ∃ (K : Set 𝓧),
      IsCompact K ∧
        ∀ (μ : Measure 𝓧),
          Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
            (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: obtain ⟨D, hD⟩ := exists_dense_seq 𝓧
-- 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
⊢ ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (K : Set 𝓧),
        IsCompact K ∧
          ∀ (μ : Measure 𝓧),
            Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
              (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have inr : ∀ (u : ℕ → ℝ) (hu_anti : StrictAnti u) (hu_pos : ∀ (n : ℕ), 0 < u n) (hu : Tendsto u atTop (𝓝 0)) (ε : ℝ≥0∞),
  0 < ε →
    ∃ (K : Set 𝓧),
      IsCompact K ∧
        ∀ (μ : Measure 𝓧),
          Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
            (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: obtain ⟨u, hu_anti, hu_pos, hu⟩ : ∃ u, StrictAnti u ∧ (∀ n, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
m : ℕ
⊢ Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) univ
have rw : ∀ (hD : ∀ (x : 𝓧), ∀ r > 0, ∃ (y : ℕ), dist x (D y) < r) (u : ℕ → ℝ) (hu_anti : StrictAnti u)
  (hu_pos : ∀ (n : ℕ), 0 < u n) (hu : Tendsto u atTop (𝓝 0)) (m : ℕ),
  Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) univ
Tactic: rw [denseRange_iff] at hD
Cleared hypotheses: hD, u, hu_anti, hu_pos, hu, m
-- 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : ∀ (x : 𝓧), ∀ r > 0, ∃ (y : ℕ), dist x (D y) < r
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
m : ℕ
⊢ Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) univ
have h : ∀ (p : 𝓧), Membership.mem (γ := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) p ↔ Membership.mem (γ := Set 𝓧) univ p
Tactic: ext p
-- 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
⊢ ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (K : Set 𝓧),
        IsCompact K ∧
          ∀ (μ : Measure 𝓧),
            Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
              (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have hcov : ∀ (m : ℕ), Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) univ
Tactic: have hcov (m : ℕ) : ⋃ i, ball (D i) (u m) = univ := by
    rw [denseRange_iff] at hD
    ext p
    exact ⟨fun a ↦ trivial, fun _ ↦ mem_iUnion.mpr <| hD p (u m) (hu_pos m)⟩
-- 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) univ
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧
      ∀ (μ : Measure 𝓧),
        Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
          (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have inr : ∀ (hεbound : 1 < ε),
  ∃ (K : Set 𝓧),
    IsCompact K ∧
      ∀ (μ : Measure 𝓧),
        Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
          (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: rcases lt_or_ge 1 ε with hεbound | 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) univ
ε : ℝ≥0∞
εpos : 0 < ε
inr :
  ∀ (hεbound : 1 < ε),
    ∃ (K : Set 𝓧),
      IsCompact K ∧
        ∀ (μ : Measure 𝓧),
          Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
            (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧
      ∀ (μ : Measure 𝓧),
        Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
          (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have inr₁ : ∀ (hεbound : ε ≤ 1),
  ∃ (K : Set 𝓧),
    IsCompact K ∧
      ∀ (μ : Measure 𝓧),
        Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
          (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: rcases lt_or_ge 1 ε with hεbound | 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : 1 < ε
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧
      ∀ (μ : Measure 𝓧),
        Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
          (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have inr : ∀ (μ : Measure 𝓧) (hμ : Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ),
  (μ : (a : Set 𝓧) → ℝ≥0∞) ∅ᶜ ≤ ε
Tactic: refine ⟨∅, isCompact_empty, fun μ hμ ↦ ?_⟩
-- 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : 1 < ε
μ : Measure 𝓧
hμ : ∃ μ_1 ∈ S, (↑μ_1 : Measure 𝓧) = μ
⊢ (μ : (a : Set 𝓧) → ℝ≥0∞) ∅ᶜ ≤ ε
have inr : ∀ (μ' : ProbabilityMeasure 𝓧) (hμ' : μ' ∈ S), ((↑μ' : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) ∅ᶜ ≤ ε
Tactic: obtain ⟨μ', hμ', rfl⟩ := hμ
Cleared hypotheses: μ, hμ
-- 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : 1 < ε
μ' : ProbabilityMeasure 𝓧
hμ' : μ' ∈ S
⊢ ((↑μ' : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) ∅ᶜ ≤ ε
have inr : 1 ≤ ε
Tactic: rw [compl_empty, measure_univ]
-- 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 𝓧)
inst_3 : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
m : ℕ
⊢ ∃ (k : ℕ),
    ∀ μ ∈ S,
      1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
        (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), ball (D i) (u m))) : ℝ≥0∞)
have refine_1 : 0 < ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ))
Tactic: refine exists_measure_iUnion_gt_of_isCompact_closure
      (fun i ↦ ball (D i) (u m)) (fun _ ↦ isOpen_ball) (hcov m) hcomp (ε * 2 ^ (-m : ℤ)) ?_ ?_