awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop
      (𝓝 0)
z : E
refine :
  ∀ (r : ℝ),
    LE.le (α := (fun (a : ℝ) ↦ ℝ≥0∞) r)
      (limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
      (⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖})
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (h z)
    (fun _ ↦ zero_le) fun r ↦ ?_

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
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop
      (𝓝 0)
z : E
r : ℝ
simp_rw :
  LE.le (α := ℝ≥0∞) (limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    (⨆ (n : ℕ), (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖})
⊢ LE.le (α := (fun (a : ℝ) ↦ ℝ≥0∞) r) (limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    (⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖})

Tactic:
simp_rw [iSup_range]

Premises used: iSup_range
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop
      (𝓝 0)
z : E
r : ℝ
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    (⨆ (n : ℕ), (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖})

Tactic:
limsup_le_iSup

Premises used: Filter.limsup_le_iSup
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop
      (𝓝 0)
z : E
r : ℝ
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    (⨆ (n : ℕ), (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖})

Tactic:
exact limsup_le_iSup

Premises used: Filter.limsup_le_iSup
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
⊢ IsTightMeasureSet (Set.range μ)

Tactic:
isTightMeasureSet_range_of_tendsto_limsup_inner 𝕜 fun y ↦ ?_

Premises used: MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_inner
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
refine :
  ∀ (y : E),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
⊢ IsTightMeasureSet (Set.range μ)

Tactic:
refine isTightMeasureSet_range_of_tendsto_limsup_inner 𝕜 fun y ↦ ?_

Premises used: MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_inner
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
pos :
  ∀ (hy : y = 0),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
neg :
  ∀ (hy : ¬y = 0),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : y = 0
pos :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) atTop) atTop
    (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)

Tactic:
simp only [hy, inner_zero_left]

Premises used: inner_zero_left
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : y = 0
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) atTop) atTop
    (𝓝 0)

Tactic:
(tendsto_congr' ?_).mpr tendsto_const_nhds

Premises used: Iff.mpr, tendsto_const_nhds, Filter.tendsto_congr'
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : y = 0
pos :
  EventuallyEq (β := ℝ≥0∞) atTop
    (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) atTop)
    fun (x : ℝ) ↦ 0
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) atTop) atTop
    (𝓝 0)

Tactic:
refine (tendsto_congr' ?_).mpr tendsto_const_nhds

Premises used: Iff.mpr, tendsto_const_nhds, Filter.tendsto_congr'
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : y = 0
h₁ :
  ∀ (r : ℝ) (hr : 0 ≤ r),
    Eq (α := ℝ≥0∞) (limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) atTop) 0
⊢ EventuallyEq (β := ℝ≥0∞) atTop
    (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) atTop)
    fun (x : ℝ) ↦ 0

Tactic:
filter_upwards [eventually_ge_atTop 0] with r hr

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : y = 0
r : ℝ
hr : 0 ≤ r
⊢ Eq (α := ℝ≥0∞) (limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) atTop) 0

Tactic:
simp [not_lt.mpr hr]

Premises used: Iff.mpr, not_lt
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
specialize : ‖HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y‖ = 1
specialize₁ :
  ∀
    (h :
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦
          limsup
            (fun (n : ℕ) ↦
              (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
            atTop)
        atTop (𝓝 0)),
    Tendsto (β := ℝ≥0∞)
      (fun (r : ℝ) ↦
        limsup
          (fun (n : ℕ) ↦
            (μ n : (a : Set E) → ℝ≥0∞)
              {x : E | ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
          atTop)
      atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)

Tactic:
specialize h ((‖y‖⁻¹ : 𝕜) • y) ?_

Premises used: Norm.norm, RCLike.ofReal, Inv.inv, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
simp : ‖y‖⁻¹ * ‖y‖ = 1
⊢ ‖HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y‖ = 1

Tactic:
simp only [norm_smul, norm_inv, norm_algebraMap', Real.norm_eq_abs, abs_norm]

Premises used: norm_smul, norm_inv, abs_norm, norm_algebraMap', Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
⊢ ‖y‖ ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
rw rw₁ : Eq (α := ℝ) 1 1
⊢ ‖y‖⁻¹ * ‖y‖ = 1

Tactic:
rw [inv_mul_cancel₀ (by positivity)]

Premises used: inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
y : E
hy : ¬y = 0
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)
⊢ 0 < ‖y‖⁻¹

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
y : E
hy : ¬y = 0
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)

Tactic:
exact h.comp <| (tendsto_const_mul_atTop_of_pos (by positivity)).mpr tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, Filter.Tendsto.comp, Filter.tendsto_const_mul_atTop_of_pos
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)

Tactic:
have h' : Tendsto (fun r : ℝ ↦ limsup (fun n ↦ μ n {x | ‖y‖⁻¹ * r < ‖⟪(‖y‖⁻¹ : 𝕜) • y, x⟫_𝕜‖})
      atTop) atTop (𝓝 0) := by
    specialize h ((‖y‖⁻¹ : 𝕜) • y) ?_
    · simp only [norm_smul, norm_inv, norm_algebraMap', Real.norm_eq_abs, abs_norm]
      rw [inv_mul_cancel₀ (by positivity)]
    exact h.comp <| (tendsto_const_mul_atTop_of_pos (by positivity)).mpr tendsto_id
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
h' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)

Tactic:
h'
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
h' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)
h₁ :
  ∀ (r : ℝ) (n : ℕ) (x : E), r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)

Tactic:
convert! h' using 7 with r n x
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
h' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)
r : ℝ
n : ℕ
x : E
h₁ : r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑‖y‖ : 𝕜)⁻¹ : 𝕜) ⟪y, x⟫_𝕜‖
⊢ r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖

Tactic:
rw [inner_smul_left]

Premises used: inner_smul_left
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
h' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)
r : ℝ
n : ℕ
x : E
h₁ : r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖y‖⁻¹ * ‖⟪y, x⟫_𝕜‖
⊢ r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑‖y‖ : 𝕜)⁻¹ : 𝕜) ⟪y, x⟫_𝕜‖

Tactic:
simp only [map_inv₀, RCLike.conj_ofReal, norm_mul, norm_inv, norm_algebraMap', norm_norm]

Premises used: RCLike.conj_ofReal, map_inv₀, norm_mul, norm_norm, norm_inv, norm_algebraMap'
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
h' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)
r : ℝ
n : ℕ
x : E
h₁ : 0 < ‖y‖⁻¹
⊢ r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖y‖⁻¹ * ‖⟪y, x⟫_𝕜‖

Tactic:
rw [mul_lt_mul_iff_right₀]

Premises used: mul_lt_mul_iff_right₀
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
h' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      limsup
        (fun (n : ℕ) ↦
          (μ n : (a : Set E) → ℝ≥0∞) {x : E | ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖})
        atTop)
    atTop (𝓝 0)
r : ℝ
n : ℕ
x : E
⊢ 0 < ‖y‖⁻¹

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)
⊢ IsTightMeasureSet (Set.range μ)

Tactic:
isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one 𝕜 fun z hz ↦ ?_

Premises used: MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)
refine :
  ∀ (z : E) (hz : ‖z‖ = 1),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
⊢ IsTightMeasureSet (Set.range μ)

Tactic:
refine isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one 𝕜 fun z hz ↦ ?_

Premises used: MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)
z : E
hz : ‖z‖ = 1
r : ℝ
rw : ∀ᶠ (a : ℕ) in atTop, (μ a : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} ≤ (↑C : ℝ≥0∞)
⊢ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop =
    ENNReal.ofReal (limsup (fun (n : ℕ) ↦ ENNReal.toReal ((μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖})) atTop)

Tactic:
rw [ENNReal.ofReal_limsup_toReal (C := C)]

Premises used: ENNReal.ofReal_limsup_toReal