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 𝓧)
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 : ℕ
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∞)
⊢ ((↑μ : 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:
rw [measure_compl (by measurability) (by simp)]

Premises used: MeasureTheory.measure_compl
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 : ℕ
⊢ 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:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tight
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))

Tactic:
ENNReal.tsum_le_tsum fun m ↦ tsub_le_iff_tsub_le.mp ?_

Premises used: ENNReal.tsum_le_tsum, Iff.mp, tsub_le_iff_tsub_le
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
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)))
⊢ 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))

Tactic:
refine ENNReal.tsum_le_tsum fun m ↦ tsub_le_iff_tsub_le.mp ?_

Premises used: ENNReal.tsum_le_tsum, Iff.mp, tsub_le_iff_tsub_le
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 (-(↑(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
-- Module: Mathlib.MeasureTheory.Measure.Tight
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∞)
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 : ℤ))
⊢ 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:
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]

Premises used: neg_add_rev, Int.reduceNeg, MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, tsub_le_iff_right, Nat.cast_add, ENNReal.coe_ofNat, Nat.cast_one
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 : ℤ))
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 : ℤ))
⊢ 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:
grw [hbound]
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 : ℤ))
bc :
  ∀ (i : ℕ) (hi : i ≤ km (m + 1)),
    ball (D i) (u (m + 1)) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u 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 : ℤ))

Tactic:
gcongr with i hi
-- Module: Mathlib.MeasureTheory.Measure.Tight
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)
bc : u (m + 1) ≤ u m
⊢ ball (D i) (u (m + 1)) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))

Tactic:
grw [← subset_closure (s := ball (D i) (u m)), ball_subset_ball]

Premises used: subset_closure, Metric.ball_subset_ball
-- Module: Mathlib.MeasureTheory.Measure.Tight
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)
⊢ m ≤ m + 1

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Tight
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)
⊢ u (m + 1) ≤ u m

Tactic:
exact hu_anti.antitone (by grind)

Premises used: StrictAnti.antitone
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
rw : ε * ∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = ε
⊢ ∑' (m : ℕ), ε * HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) = ε

Tactic:
rw [ENNReal.tsum_mul_left]

Premises used: ENNReal.tsum_mul_left
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
nth_rw : ε * ∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = ε * 1
⊢ ε * ∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = ε

Tactic:
nth_rw 2 [← mul_one (a := ε)]

Premises used: mul_one
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
e_a : Eq (α := ℝ≥0∞) (∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)) 1
⊢ ε * ∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = ε * 1

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
e_a : Eq (α := ℝ≥0∞) (∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (HSub.hSub (α := ℤ) (-1) (↑i : ℤ))) 1
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)) 1

Tactic:
ring_nf
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 (HSub.hSub (α := ℤ) (-1) (↑i : ℤ))) 1

Tactic:
tsum_two_zpow_neg_add_one

Premises used: ENNReal.tsum_two_zpow_neg_add_one
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 (HSub.hSub (α := ℤ) (-1) (↑i : ℤ))) 1

Tactic:
exact tsum_two_zpow_neg_add_one

Premises used: ENNReal.tsum_two_zpow_neg_add_one