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

Tactic:
isClosed_iInter fun n =>
      Finite.isClosed_biUnion (finite_Iic _) (fun _ _ ↦ isClosed_closure)

Premises used: Set.finite_Iic, HAdd.hAdd, OfNat.ofNat, isClosed_closure, Set.Finite.isClosed_biUnion, isClosed_iInter
-- 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ᶜ ≤ ε
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⋂ (m : ℕ), ⋃ i ∈ Iic (km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))

Tactic:
exact isClosed_iInter fun n =>
      Finite.isClosed_biUnion (finite_Iic _) (fun _ _ ↦ isClosed_closure)

Premises used: Set.finite_Iic, isClosed_closure, Set.Finite.isClosed_biUnion, isClosed_iInter
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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∞)
    (Function.comp.{1, u_1 + 1, 1} (β := Set E) (⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) fun (r : ℝ) ↦
      (Metric.closedBall x r)ᶜ)
    atTop (𝓝 0)

Tactic:
this
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x r)ᶜ) atTop (𝓝 0)

Tactic:
convert! this with r
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
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:
simp
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
hS : IsTightMeasureSet S
x : E
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x r)ᶜ) atTop (𝓝 0)

Tactic:
suffices Tendsto ((⨆ μ ∈ S, μ) ∘ (fun r ↦ (Metric.closedBall x r)ᶜ)) atTop (𝓝 0) by
    convert! this with r
    simp
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)

Tactic:
hS.comp <| .mono_right ?_ <| monotone_smallSets Metric.cobounded_le_cocompact

Premises used: Metric.cobounded_le_cocompact, Filter.monotone_smallSets, Filter.Tendsto.mono_right, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
hS : IsTightMeasureSet S
x : E
refine : Tendsto (fun (r : ℝ) ↦ (Metric.closedBall x r)ᶜ) atTop (Bornology.cobounded E).smallSets
⊢ 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:
refine hS.comp <| .mono_right ?_ <| monotone_smallSets Metric.cobounded_le_cocompact

Premises used: Metric.cobounded_le_cocompact, Filter.monotone_smallSets, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
hS : IsTightMeasureSet S
x : E
⊢ Tendsto (fun (r : ℝ) ↦ (Metric.closedBall x r)ᶜ) atTop (Bornology.cobounded E).smallSets

Tactic:
(Metric.hasAntitoneBasis_cobounded_compl_closedBall _).tendsto_smallSets

Premises used: Metric.hasAntitoneBasis_cobounded_compl_closedBall, Filter.HasAntitoneBasis.tendsto_smallSets
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
hS : IsTightMeasureSet S
x : E
⊢ Tendsto (fun (r : ℝ) ↦ (Metric.closedBall x r)ᶜ) atTop (Bornology.cobounded E).smallSets

Tactic:
exact (Metric.hasAntitoneBasis_cobounded_compl_closedBall _).tendsto_smallSets

Premises used: Metric.hasAntitoneBasis_cobounded_compl_closedBall, Filter.HasAntitoneBasis.tendsto_smallSets
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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

Tactic:
isTightMeasureSet_iff_exists_isCompact_measure_compl_le.mpr fun ε hε ↦ ?_

Premises used: Iff.mpr, MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
refine : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) Kᶜ ≤ ε
⊢ IsTightMeasureSet S

Tactic:
refine isTightMeasureSet_iff_exists_isCompact_measure_compl_le.mpr fun ε hε ↦ ?_

Premises used: Iff.mpr, MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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 < ε
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ᶜ ≤ ε
⊢ ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
rw [ENNReal.tendsto_atTop_zero] at h

Premises used: ENNReal.tendsto_atTop_zero
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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 < ε
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ᶜ ≤ ε
⊢ ∃ (K : Set E), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
obtain ⟨r, h⟩ := h ε hε
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
inst_1 : ProperSpace E
x : E
h_1 : ∀ ε > 0, ∃ (N : ℝ), ∀ n ≥ N, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x n)ᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ
h : ∀ n ≥ r, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x n)ᶜ ≤ ε
⊢ ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x r)ᶜ ≤ ε

Tactic:
simpa using h r le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
inst_1 : ProperSpace E
x : E
h_1 : ∀ ε > 0, ∃ (N : ℝ), ∀ n ≥ N, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x n)ᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
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:
exact ⟨Metric.closedBall x r, isCompact_closedBall x r, by simpa using h r le_rfl⟩
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : PseudoMetricSpace E
inst_1 : ProperSpace E
x : E
⊢ IsTightMeasureSet S ↔
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall x r)ᶜ) atTop (𝓝 0)

Tactic:
⟨fun hS ↦ tendsto_measure_compl_closedBall_of_isTightMeasureSet hS x,
    isTightMeasureSet_of_tendsto_measure_compl_closedBall⟩

Premises used: MeasureTheory.isTightMeasureSet_of_tendsto_measure_compl_closedBall, Iff.intro, MeasureTheory.tendsto_measure_compl_closedBall_of_isTightMeasureSet
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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∞) (Metric.closedBall 0 r)ᶜ) atTop (𝓝 0)

Tactic:
have h := tendsto_measure_compl_closedBall_of_isTightMeasureSet hS 0
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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∞) (Metric.closedBall 0 r)ᶜ) atTop (𝓝 0)

Tactic:
h
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
h₁ : ∀ (r : ℝ), ∀ x ∈ S, Eq.{u_1 + 1} (α := Set E) {x : E | r < ‖x‖} (Metric.closedBall 0 r)ᶜ
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)

Tactic:
convert! h using 6 with r
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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
h₁ : ∀ (x : E), Membership.mem (γ := Set E) {x : E | r < ‖x‖} x ↔ Membership.mem (γ := Set E) (Metric.closedBall 0 r)ᶜ x
⊢ Eq.{u_1 + 1} (α := Set E) {x : E | r < ‖x‖} (Metric.closedBall 0 r)ᶜ

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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
x_1 : E
⊢ Membership.mem (γ := Set E) {x : E | r < ‖x‖} x_1 ↔ Membership.mem (γ := Set E) (Metric.closedBall 0 r)ᶜ x_1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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

Tactic:
isTightMeasureSet_of_tendsto_measure_compl_closedBall (x := 0) ?_

Premises used: MeasureTheory.isTightMeasureSet_of_tendsto_measure_compl_closedBall
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
refine : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 r)ᶜ) atTop (𝓝 0)
⊢ IsTightMeasureSet S

Tactic:
refine isTightMeasureSet_of_tendsto_measure_compl_closedBall (x := 0) ?_

Premises used: MeasureTheory.isTightMeasureSet_of_tendsto_measure_compl_closedBall
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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∞) {x : E | r < ‖x‖}) atTop (𝓝 0)

Tactic:
h
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
h₁ : ∀ (r : ℝ), ∀ x ∈ S, Eq.{u_1 + 1} (α := Set E) (Metric.closedBall 0 r)ᶜ {x : E | r < ‖x‖}
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 r)ᶜ) atTop (𝓝 0)

Tactic:
convert! h using 6 with r
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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
h₁ : ∀ (x : E), Membership.mem (γ := Set E) (Metric.closedBall 0 r)ᶜ x ↔ Membership.mem (γ := Set E) {x : E | r < ‖x‖} x
⊢ Eq.{u_1 + 1} (α := Set E) (Metric.closedBall 0 r)ᶜ {x : E | r < ‖x‖}

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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
x_1 : E
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 r)ᶜ x_1 ↔ Membership.mem (γ := Set E) {x : E | r < ‖x‖} x_1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
⊢ IsTightMeasureSet S ↔
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)

Tactic:
⟨tendsto_measure_norm_gt_of_isTightMeasureSet, isTightMeasureSet_of_tendsto_measure_norm_gt⟩

Premises used: MeasureTheory.isTightMeasureSet_of_tendsto_measure_norm_gt, MeasureTheory.tendsto_measure_norm_gt_of_isTightMeasureSet, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
simp_rw : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ (i : ℕ), (μ i : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
⊢ IsTightMeasureSet (Set.range μ)

Tactic:
simp_rw [isTightMeasureSet_iff_tendsto_measure_norm_gt, iSup_range]

Premises used: iSup_range, MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
n : ℕ
u v : ℝ
huv : u ≤ v
⊢ LE.le (α := ℝ≥0∞) ((μ n : (a : Set E) → ℝ≥0∞) {x : E | v < ‖x‖} : ℝ≥0∞)
    ((μ n : (a : Set E) → ℝ≥0∞) {x : E | u < ‖x‖} : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
refine : ∀ (n : ℕ), Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ (i : ℕ), (μ i : (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)

Premises used: Nat.tendsto_iSup_of_tendsto_limsup
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
n : ℕ
⊢ IsTightMeasureSet (𝓧 := E) (m𝓧 := mE) {μ n}

Tactic:
have h_tight : IsTightMeasureSet {μ n} := isTightMeasureSet_singleton
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
n : ℕ
h_tight : IsTightMeasureSet (𝓧 := E) (m𝓧 := mE) {μ n}
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ⨆ (μ_1 : Measure E),
        ⨆ (_ : Membership.mem (γ := Set (Measure E)) {μ n} μ_1), (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖})
    atTop (𝓝 0)

Tactic:
rw [isTightMeasureSet_iff_tendsto_measure_norm_gt] at h_tight

Premises used: MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
n : ℕ
h_tight :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ⨆ (μ_1 : Measure E),
        ⨆ (_ : Membership.mem (γ := Set (Measure E)) {μ n} μ_1), (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖})
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)

Tactic:
simpa using h_tight
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
⊢ IsTightMeasureSet (Set.range μ) ↔
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
      (𝓝 0)

Tactic:
⟨fun h ↦ ?_, isTightMeasureSet_range_of_tendsto_limsup_measure_norm_gt⟩

Premises used: MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_measure_norm_gt, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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)
refine :
  ∀ (h : IsTightMeasureSet (Set.range μ)),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
      (𝓝 0)
⊢ IsTightMeasureSet (Set.range μ) ↔
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
      (𝓝 0)

Tactic:
refine ⟨fun h ↦ ?_, isTightMeasureSet_range_of_tendsto_limsup_measure_norm_gt⟩
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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 : IsTightMeasureSet (Set.range μ)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)

Tactic:
have h_sup := tendsto_measure_norm_gt_of_isTightMeasureSet h
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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 : IsTightMeasureSet (Set.range μ)
h_sup :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
    (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h_sup (fun _ ↦ zero_le) ?_

Premises used: zero_le, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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 : IsTightMeasureSet (Set.range μ)
h_sup :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
refine :
  LE.le (α := ℝ → ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop)
    fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
    (𝓝 0)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h_sup (fun _ ↦ zero_le) ?_

Premises used: zero_le, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds