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 𝓧)
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 : ℕ
refine_1 : 0 < ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ))
⊢ ∃ (k : ℕ),
    ∀ μ ∈ S,
      1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
        (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), ball (D i) (u m))) : ℝ≥0∞)
have refine_2 : ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) ≤ 1
Tactic: refine exists_measure_iUnion_gt_of_isCompact_closure
      (fun i ↦ ball (D i) (u m)) (fun _ ↦ isOpen_ball) (hcov m) hcomp (ε * 2 ^ (-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 < ε
hεbound : ε ≤ 1
m : ℕ
⊢ LE.le (α := ℤ) (-(↑m : ℤ)) 0
have linarith : LT.lt (α := ℤ) 0 (-(↑m : ℤ)) → -1 + HSub.hSub (α := ℤ) 0 (↑m : ℤ) + (HAdd.hAdd (α := ℤ) 0 1 - -(↑m : ℤ)) = 0
Tactic: linarith
-- 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)
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 byclaim : ∀ (m : ℕ),
  ∃ (k : ℕ),
    ∀ μ ∈ S,
      1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
        (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), ball (D i) (u m))) : ℝ≥0∞)
Tactic: have byclaim (m : ℕ) : ∃ k, ∀ μ ∈ S, 1 - (ε * 2 ^ (-m : ℤ) : ℝ≥0∞) <
      μ (⋃ i ≤ k, ball (D i) (u m)) := by
    refine exists_measure_iUnion_gt_of_isCompact_closure
      (fun i ↦ ball (D i) (u m)) (fun _ ↦ isOpen_ball) (hcov m) hcomp (ε * 2 ^ (-m : ℤ)) ?_ ?_
    · simpa using ⟨εpos, (ENNReal.zpow_pos (by simp) (by simp) (-↑m))⟩
    · exact Left.mul_le_one hεbound <| zpow_le_one_of_nonpos (by linarith) (by simp)
-- 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
byclaim :
  ∀ (m : ℕ),
    ∃ (k : ℕ),
      ∀ μ ∈ S,
        1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
          (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), ball (D i) (u m))) : ℝ≥0∞)
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧
      ∀ (μ : Measure 𝓧),
        Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
          (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have inr : ∀ (km : (m : ℕ) → ℕ)
  (hbound :
    ∀ (m : ℕ),
      ∀ μ ∈ S,
        1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
          (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km m), ball (D i) (u m))) : ℝ≥0∞)),
  ∃ (K : Set 𝓧),
    IsCompact K ∧
      ∀ (μ : Measure 𝓧),
        Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
          (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: choose! km hbound using byclaim
Cleared hypotheses: byclaim
-- 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
km : (m : ℕ) → ℕ
hbound :
  ∀ (m : ℕ),
    ∀ μ ∈ S,
      1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
        (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km m), ball (D i) (u m))) : ℝ≥0∞)
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
⊢ Eq (α := ℝ≥0∞)
    (∑' (m : ℕ),
      ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
        (⋃ (i : ℕ),
            ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))ᶜ)
    (∑' (m : ℕ),
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
        (((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
            (⋃ (i : ℕ),
              ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))) :
          ℝ≥0∞))
have h : ∀ (m : ℕ),
  ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
      (⋃ (i : ℕ),
          ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))ᶜ =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      (((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
          (⋃ (i : ℕ),
            ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))) :
        ℝ≥0∞)
Tactic: congr! with 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 < ε
hεbound : ε ≤ 1
km : (m : ℕ) → ℕ
hbound :
  ∀ (m : ℕ),
    ∀ μ ∈ S,
      1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
        (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km m), ball (D i) (u m))) : ℝ≥0∞)
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
m : ℕ
⊢ ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
      (⋃ (i : ℕ),
          ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))ᶜ =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      (((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
          (⋃ (i : ℕ),
            ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))) :
        ℝ≥0∞)
have h : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞)
    (((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
        (⋃ (i : ℕ),
          ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))) :
      ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
    (((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
        (⋃ (i : ℕ),
          ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))) :
      ℝ≥0∞)
Tactic: rw [measure_compl (by measurability) (by simp)]
-- 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
km : (m : ℕ) → ℕ
hbound :
  ∀ (m : ℕ),
    ∀ μ ∈ S,
      1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
        (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km m), ball (D i) (u m))) : ℝ≥0∞)
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
⊢ LE.le (α := ℝ≥0∞)
    (∑' (m : ℕ),
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
        (((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
            (⋃ (i : ℕ),
              ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))) :
          ℝ≥0∞))
    (∑' (m : ℕ), ε * HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1))
have refine : ∀ (m : ℕ),
  1 - ε * HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) ≤
    ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
      (⋃ (i : ℕ),
        ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))
Tactic: refine ENNReal.tsum_le_tsum fun m ↦ tsub_le_iff_tsub_le.mp ?_
-- 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)
hcov : ∀ (m : ℕ), Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), ball (D i) (u m)) univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
km : (m : ℕ) → ℕ
hbound :
  ∀ (m : ℕ),
    ∀ μ ∈ S,
      1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
        (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km m), ball (D i) (u m))) : ℝ≥0∞)
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
m : ℕ
⊢ 1 - ε * HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) ≤
    ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
      (⋃ (i : ℕ),
        ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))
have hbound₁ : 1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑(m + 1) : ℤ)) ≤
  (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), ball (D i) (u (m + 1)))) : ℝ≥0∞)
Tactic: replace hbound := (hbound (m + 1) μ hs).le
Cleared hypotheses: hbound
-- 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
km : (m : ℕ) → ℕ
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
m : ℕ
hbound :
  1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑(m + 1) : ℤ)) ≤
    (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), ball (D i) (u (m + 1)))) : ℝ≥0∞)
⊢ 1 - ε * HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) ≤
    ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞)
      (⋃ (i : ℕ),
        ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))
have simp_all : ∀
  (hbound :
    1 ≤
      (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), ball (D i) (u (m + 1)))) : ℝ≥0∞) +
        ε * (↑2 : ℝ≥0∞) ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ))),
  1 ≤
    (↑((μ : (a : Set 𝓧) → ℝ≥0)
            (⋃ (i : ℕ),
              ⋃ (_ : i ≤ km (m + 1)),
                closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))) :
        ℝ≥0∞) +
      ε * (↑2 : ℝ≥0∞) ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ))
Tactic: simp_all only [neg_add_rev, Int.reduceNeg, tsub_le_iff_right, Nat.cast_add, Nat.cast_one,
          ← coe_ofNat, ← ennreal_coeFn_eq_coeFn_toMeasure]
Cleared hypotheses: hbound
-- 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
km : (m : ℕ) → ℕ
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
m : ℕ
hbound :
  1 ≤
    (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), ball (D i) (u (m + 1)))) : ℝ≥0∞) +
      ε * (↑2 : ℝ≥0∞) ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ))
⊢ 1 ≤
    (↑((μ : (a : Set 𝓧) → ℝ≥0)
            (⋃ (i : ℕ),
              ⋃ (_ : i ≤ km (m + 1)),
                closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))) :
        ℝ≥0∞) +
      ε * (↑2 : ℝ≥0∞) ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ))
have grw : (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), ball (D i) (u (m + 1)))) : ℝ≥0∞) +
    ε * (↑2 : ℝ≥0∞) ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) ≤
  (↑((μ : (a : Set 𝓧) → ℝ≥0)
          (⋃ (i : ℕ),
            ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))) :
      ℝ≥0∞) +
    ε * (↑2 : ℝ≥0∞) ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ))
Tactic: grw [hbound]
-- 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
km : (m : ℕ) → ℕ
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
m : ℕ
hbound :
  1 ≤
    (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), ball (D i) (u (m + 1)))) : ℝ≥0∞) +
      ε * (↑2 : ℝ≥0∞) ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ))
⊢ (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), ball (D i) (u (m + 1)))) : ℝ≥0∞) +
      ε * (↑2 : ℝ≥0∞) ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) ≤
    (↑((μ : (a : Set 𝓧) → ℝ≥0)
            (⋃ (i : ℕ),
              ⋃ (_ : i ≤ km (m + 1)),
                closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))) :
        ℝ≥0∞) +
      ε * (↑2 : ℝ≥0∞) ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ))
have bc : ∀ (i : ℕ) (hi : i ≤ km (m + 1)),
  ball (D i) (u (m + 1)) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
Tactic: gcongr with i hi
-- 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
km : (m : ℕ) → ℕ
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
m : ℕ
hbound :
  1 ≤
    (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), ball (D i) (u (m + 1)))) : ℝ≥0∞) +
      ε * (↑2 : ℝ≥0∞) ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ))
i : ℕ
hi : i ≤ km (m + 1)
⊢ ball (D i) (u (m + 1)) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
have bc : u (m + 1) ≤ u m
Tactic: grw [← subset_closure (s := ball (D i) (u m)), ball_subset_ball]
-- 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
km : (m : ℕ) → ℕ
hbound :
  ∀ (m : ℕ),
    ∀ μ ∈ S,
      1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
        (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km m), ball (D i) (u m))) : ℝ≥0∞)
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
⊢ ∑' (m : ℕ), ε * HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) = ε
have rw : ε * ∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = ε
Tactic: rw [ENNReal.tsum_mul_left]
-- 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
km : (m : ℕ) → ℕ
hbound :
  ∀ (m : ℕ),
    ∀ μ ∈ S,
      1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
        (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km m), ball (D i) (u m))) : ℝ≥0∞)
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
⊢ ε * ∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = ε
have nth_rw : ε * ∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = ε * 1
Tactic: nth_rw 2 [← mul_one (a := ε)]
-- 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
km : (m : ℕ) → ℕ
hbound :
  ∀ (m : ℕ),
    ∀ μ ∈ S,
      1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
        (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km m), ball (D i) (u m))) : ℝ≥0∞)
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
⊢ ε * ∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = ε * 1
have e_a : Eq (α := ℝ≥0∞) (∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)) 1
Tactic: congr
-- 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
km : (m : ℕ) → ℕ
hbound :
  ∀ (m : ℕ),
    ∀ μ ∈ S,
      1 - ε * HPow.hPow (α := ℝ≥0∞) (β := ℤ) 2 (-(↑m : ℤ)) <
        (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ km m), ball (D i) (u m))) : ℝ≥0∞)
bigK : Set 𝓧 :=
  ⋂ (m : ℕ),
    ⋃ (i : ℕ), ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)) 1
have e_a : Eq (α := ℝ≥0∞) (∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (HSub.hSub (α := ℤ) (-1) (↑i : ℤ))) 1
Tactic: ring_nf