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 𝓧)
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))
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧
      ∀ (μ : Measure 𝓧),
        Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
          (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have bigcalc : ∀ (μ : 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
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧
      ∀ (μ : Measure 𝓧),
        Membership.mem (γ := Set (Measure 𝓧)) {x : Measure 𝓧 | ∃ μ ∈ S, (↑μ : Measure 𝓧) = x} μ →
          (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have inr : IsCompact bigK
Tactic: refine ⟨bigK, ?_, by simpa⟩
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
⊢ IsCompact bigK
have inr : TotallyBounded bigK
Tactic: refine TotallyBounded.isCompact_of_isClosed ?_ ?_
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
inr : TotallyBounded bigK
⊢ IsCompact bigK
have inr₁ : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] bigK
Tactic: refine TotallyBounded.isCompact_of_isClosed ?_ ?_
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
⊢ TotallyBounded bigK
have inr : ∀ (δ : ℝ) (δpos : δ > 0), ∃ (t : Set 𝓧), t.Finite ∧ bigK ⊆ ⋃ y ∈ t, ball y δ
Tactic: refine Metric.totallyBounded_iff.mpr fun δ δpos ↦ ?_
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
⊢ ∃ (t : Set 𝓧), t.Finite ∧ bigK ⊆ ⋃ y ∈ t, ball y δ
have inr : ∀ (δ_inv : ℕ) (hδ_inv : u δ_inv < δ), ∃ (t : Set 𝓧), t.Finite ∧ bigK ⊆ ⋃ y ∈ t, ball y δ
Tactic: have ⟨δ_inv, hδ_inv⟩ : ∃ x, u x < δ := (Tendsto.eventually_lt_const δpos hu).exists
-- 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))
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 δ
have inr : bigK ⊆ ⋃ y ∈ D '' Iic (km (δ_inv + 1)), ball y δ
Tactic: refine ⟨D '' .Iic (km (δ_inv + 1)), (Set.finite_Iic _).image _, ?_⟩
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
⊢ bigK ⊆ ⋃ y ∈ D '' Iic (km (δ_inv + 1)), ball y δ
have 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) δ)
Tactic: simp only [mem_image, iUnion_exists, biUnion_and', iUnion_iUnion_eq_right, bigK]
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
⊢ 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) δ)
have h : ∀ i ≤ km (δ_inv + 1), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u δ_inv)) ⊆ ball (D i) δ
Tactic: gcongr
-- 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))
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)))
    (⋃ y ∈ Iic (km (δ_inv + 1)), ball (D y) δ)
have 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: 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
-- 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))
bigcalc : ∀ (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S), ((↑μ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) bigKᶜ ≤ ε
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] bigK
have inr : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (⋂ (m : ℕ), ⋃ i ∈ Iic (km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))
Tactic: simp_rw [bigK, ← Set.mem_Iic]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
hS : IsTightMeasureSet S
x : E
this :
  Tendsto (α := ℝ) (β := ℝ≥0∞)
    (Function.comp.{1, u_1 + 1, 1} (β := Set E) (⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) fun (r : ℝ) ↦
      (Metric.closedBall x r)ᶜ)
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x r)ᶜ) atTop (𝓝 0)
have h : ∀ (r : ℝ),
  Eq (α := ℝ≥0∞) (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x r)ᶜ)
    (Function.comp.{1, u_1 + 1, 1} (β := Set E) (⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞))
      (fun (r : ℝ) ↦ (Metric.closedBall x r)ᶜ) r)
Tactic: convert! this with r
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
hS : IsTightMeasureSet S
x : E
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x r)ᶜ) atTop (𝓝 0)
have suffices : Tendsto (α := ℝ) (β := ℝ≥0∞)
  (Function.comp.{1, u_1 + 1, 1} (β := Set E) (⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) fun (r : ℝ) ↦
    (Metric.closedBall x r)ᶜ)
  atTop (𝓝 0)
Tactic: suffices Tendsto ((⨆ μ ∈ S, μ) ∘ (fun r ↦ (Metric.closedBall x r)ᶜ)) atTop (𝓝 0) by
    convert! this with r
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
hS : IsTightMeasureSet S
x : E
⊢ Tendsto (α := ℝ) (β := ℝ≥0∞)
    (Function.comp.{1, u_1 + 1, 1} (β := Set E) (⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) fun (r : ℝ) ↦
      (Metric.closedBall x r)ᶜ)
    atTop (𝓝 0)
have refine : Tendsto (fun (r : ℝ) ↦ (Metric.closedBall x r)ᶜ) atTop (Bornology.cobounded E).smallSets
Tactic: refine hS.comp <| .mono_right ?_ <| monotone_smallSets Metric.cobounded_le_cocompact
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
inst_1 : ProperSpace E
x : E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x r)ᶜ) atTop (𝓝 0)
⊢ IsTightMeasureSet S
have refine : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: refine isTightMeasureSet_iff_exists_isCompact_measure_compl_le.mpr fun ε hε ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
inst_1 : ProperSpace E
x : E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x r)ᶜ) atTop (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) Kᶜ ≤ ε
have rw : ∀ (h : ∀ ε > 0, ∃ (N : ℝ), ∀ n ≥ N, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x n)ᶜ ≤ ε) (ε : ℝ≥0∞)
  (hε : 0 < ε), ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: rw [ENNReal.tendsto_atTop_zero] at h
Cleared hypotheses: h, ε, hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
inst_1 : ProperSpace E
x : E
h : ∀ ε > 0, ∃ (N : ℝ), ∀ n ≥ N, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x n)ᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) Kᶜ ≤ ε
have obtain : ∀ (r : ℝ) (h : ∀ n ≥ r, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x n)ᶜ ≤ ε),
  ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: obtain ⟨r, h⟩ := h ε hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
hS : IsTightMeasureSet S
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
have h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 r)ᶜ) atTop (𝓝 0)
Tactic: have h := tendsto_measure_compl_closedBall_of_isTightMeasureSet hS 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
hS : IsTightMeasureSet S
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 r)ᶜ) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
have h₁ : ∀ (r : ℝ), ∀ x ∈ S, Eq.{u_1 + 1} (α := Set E) {x : E | r < ‖x‖} (Metric.closedBall 0 r)ᶜ
Tactic: convert! h using 6 with r
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
hS : IsTightMeasureSet S
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 r)ᶜ) atTop (𝓝 0)
r : ℝ
x : Measure E
h_1 : x ∈ S
⊢ Eq.{u_1 + 1} (α := Set E) {x : E | r < ‖x‖} (Metric.closedBall 0 r)ᶜ
have h₁ : ∀ (x : E), Membership.mem (γ := Set E) {x : E | r < ‖x‖} x ↔ Membership.mem (γ := Set E) (Metric.closedBall 0 r)ᶜ x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
⊢ IsTightMeasureSet S
have refine : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 r)ᶜ) atTop (𝓝 0)
Tactic: refine isTightMeasureSet_of_tendsto_measure_compl_closedBall (x := 0) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 r)ᶜ) atTop (𝓝 0)
have h₁ : ∀ (r : ℝ), ∀ x ∈ S, Eq.{u_1 + 1} (α := Set E) (Metric.closedBall 0 r)ᶜ {x : E | r < ‖x‖}
Tactic: convert! h using 6 with r
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
r : ℝ
x : Measure E
h_1 : x ∈ S
⊢ Eq.{u_1 + 1} (α := Set E) (Metric.closedBall 0 r)ᶜ {x : E | r < ‖x‖}
have h₁ : ∀ (x : E), Membership.mem (γ := Set E) (Metric.closedBall 0 r)ᶜ x ↔ Membership.mem (γ := Set E) {x : E | r < ‖x‖} x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : ProperSpace E
μ : ℕ → Measure E
inst_3 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
    (𝓝 0)
⊢ IsTightMeasureSet (Set.range μ)
have simp_rw : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ (i : ℕ), (μ i : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
Tactic: simp_rw [isTightMeasureSet_iff_tendsto_measure_norm_gt, iSup_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : ProperSpace E
μ : ℕ → Measure E
inst_3 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
    (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ (i : ℕ), (μ i : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
have refine : ∀ (n : ℕ), Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
Tactic: refine Nat.tendsto_iSup_of_tendsto_limsup (fun n ↦ ?_) h (fun n u v huv ↦ by gcongr)