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), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε

Tactic:
have bigcalc (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S) : μ.toMeasure bigKᶜ ≤ ε := calc
    μ.toMeasure bigKᶜ
    _ = μ.toMeasure (⋃ m, (⋃ (i ≤ km (m + 1)), closure (ball (D i) (u m)))ᶜ) := by simp [bigK]
    _ ≤ ∑' m, μ.toMeasure (⋃ (i ≤ km (m + 1)), closure (ball (D i) (u m)))ᶜ :=
      measure_iUnion_le _
    _ = ∑' m, (1 - μ.toMeasure (⋃ (i ≤ km (m + 1)), closure (ball (D i) (u m)))) := by
      congr! with m; rw [measure_compl (by measurability) (by simp)]; simp
    _ ≤ (∑' (m : ℕ), (ε : ℝ≥0∞) * 2 ^ (-(m + 1) : ℤ)) := by
      refine ENNReal.tsum_le_tsum fun m ↦ tsub_le_iff_tsub_le.mp ?_
      replace hbound := (hbound (m + 1) μ hs).le
      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]
      grw [hbound]
      gcongr with i hi
      grw [← subset_closure (s := ball (D i) (u m)), ball_subset_ball]
      exact hu_anti.antitone (by grind)
    _ = ε := by
      rw [ENNReal.tsum_mul_left]
      nth_rw 2 [← mul_one (a := ε)]
      congr
      ring_nf
      exact 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
⊢ ∀ (μ : Measure 𝓧),
    Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
      (μ : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε

Tactic:
simpa
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
inr : IsCompact bigK
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧
      ∀ (μ : Measure 𝓧),
        Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
          (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
refine ⟨bigK, ?_, by simpa⟩
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
⊢ IsCompact bigK

Tactic:
TotallyBounded.isCompact_of_isClosed ?_ ?_

Premises used: TotallyBounded.isCompact_of_isClosed
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
inr : TotallyBounded bigK
inr₁ : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] bigK
⊢ IsCompact bigK

Tactic:
refine TotallyBounded.isCompact_of_isClosed ?_ ?_

Premises used: TotallyBounded.isCompact_of_isClosed
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
⊢ TotallyBounded bigK

Tactic:
Metric.totallyBounded_iff.mpr fun δ δpos ↦ ?_

Premises used: Iff.mpr, Metric.totallyBounded_iff
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
inr : ∀ (δ : ℝ) (δpos : δ > 0), ∃ (t : Set 𝓧), t.Finite ∧ bigK ⊆ ⋃ y ∈ t, ball y δ
⊢ TotallyBounded bigK

Tactic:
refine Metric.totallyBounded_iff.mpr fun δ δpos ↦ ?_

Premises used: Iff.mpr, Metric.totallyBounded_iff
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
inr : ∀ (δ_inv : ℕ) (hδ_inv : u δ_inv < δ), ∃ (t : Set 𝓧), t.Finite ∧ bigK ⊆ ⋃ y ∈ t, ball y δ
⊢ ∃ (t : Set 𝓧), t.Finite ∧ bigK ⊆ ⋃ y ∈ t, ball y δ

Tactic:
have ⟨δ_inv, hδ_inv⟩ : ∃ x, u x < δ := (Tendsto.eventually_lt_const δpos hu).exists
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
⊢ ∃ (t : Set 𝓧), t.Finite ∧ bigK ⊆ ⋃ y ∈ t, ball y δ

Tactic:
⟨D '' .Iic (km (δ_inv + 1)), (Set.finite_Iic _).image _, ?_⟩

Premises used: Set.finite_Iic, Set.Finite.image, HAdd.hAdd, And.intro, Exists.intro, Set.image, Set.Iic, OfNat.ofNat
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
inr : bigK ⊆ ⋃ y ∈ D '' Iic (km (δ_inv + 1)), ball y δ
⊢ ∃ (t : Set 𝓧), t.Finite ∧ bigK ⊆ ⋃ y ∈ t, ball y δ

Tactic:
refine ⟨D '' .Iic (km (δ_inv + 1)), (Set.finite_Iic _).image _, ?_⟩
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
inr :
  Subset.{u_1} (α := Set 𝓧)
    (⋂ (m : ℕ),
      ⋃ (i : ℕ),
        ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))
    (⋃ y ∈ Iic (km (δ_inv + 1)), ball (D y) δ)
⊢ bigK ⊆ ⋃ y ∈ D '' Iic (km (δ_inv + 1)), ball y δ

Tactic:
simp only [mem_image, iUnion_exists, biUnion_and', iUnion_iUnion_eq_right, bigK]

Premises used: Set.iUnion_iUnion_eq_right, Set.mem_image, Set.iUnion_exists, Set.biUnion_and'
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
⊢ Subset.{u_1} (α := Set 𝓧)
    (⋂ (m : ℕ),
      ⋃ (i : ℕ),
        ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))
    (⋃ (i : ℕ),
      ⋃ (_ : i ≤ km (δ_inv + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u δ_inv)))

Tactic:
iInter_subset ..

Premises used: Set.iInter_subset
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
h :
  ∀ i ≤ km (δ_inv + 1),
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u δ_inv)) ⊆ ball (D i) δ
⊢ Subset.{u_1} (α := Set 𝓧)
    (⋃ (i : ℕ),
      ⋃ (_ : i ≤ km (δ_inv + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u δ_inv)))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ km (δ_inv + 1)), ball (D i) δ)

Tactic:
gcongr
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
i : ℕ
i_1 : i ≤ km (δ_inv + 1)
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u δ_inv)) ⊆ ball (D i) δ

Tactic:
closure_ball_subset_closedBall.trans <| closedBall_subset_ball <| hδ_inv

Premises used: Metric.closedBall_subset_ball, HasSubset.Subset.trans, Metric.closure_ball_subset_closedBall
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
i : ℕ
i_1 : i ≤ km (δ_inv + 1)
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u δ_inv)) ⊆ ball (D i) δ

Tactic:
exact closure_ball_subset_closedBall.trans <| closedBall_subset_ball <| hδ_inv

Premises used: Metric.closedBall_subset_ball, HasSubset.Subset.trans, Metric.closure_ball_subset_closedBall
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
i :
  Subset.{u_1} (α := Set 𝓧)
    (⋃ (i : ℕ),
      ⋃ (_ : i ≤ km (δ_inv + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u δ_inv)))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ km (δ_inv + 1)), ball (D i) δ)
⊢ Subset.{u_1} (α := Set 𝓧)
    (⋂ (m : ℕ),
      ⋃ (i : ℕ),
        ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))
    (⋃ y ∈ Iic (km (δ_inv + 1)), ball (D y) δ)

Tactic:
calc
        ⋂ m, ⋃ i ≤ km (m + 1), closure (ball (D i) (u m))
    _ ⊆ ⋃ i ≤ km (δ_inv + 1), closure (ball (D i) (u δ_inv)) := iInter_subset ..
    _ ⊆ ⋃ i ≤ km (δ_inv + 1), ball (D i) δ := by
        gcongr
        exact closure_ball_subset_closedBall.trans <| closedBall_subset_ball <| hδ_inv

Premises used: HAdd.hAdd, Set.iInter_subset, OfNat.ofNat
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
inr :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⋂ (m : ℕ), ⋃ i ∈ Iic (km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] bigK

Tactic:
simp_rw [bigK, ← Set.mem_Iic]

Premises used: Set.mem_Iic