awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
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 : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
n : ℕ
h_tight : IsTightMeasureSet (𝓧 := 𝕜) (m𝓧 := RCLike.measurableSpace) {Measure.map (fun (x : E) ↦ ⟪z, x⟫_𝕜) (μ n)}
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)
have h_tight₁ : Tendsto (β := ℝ≥0∞)
  (fun (r : ℝ) ↦
    ⨆ (μ_1 : Measure 𝕜),
      ⨆ (_ : Membership.mem (γ := Set (Measure 𝕜)) {Measure.map (fun (x : E) ↦ ⟪z, x⟫_𝕜) (μ n)} μ_1),
        (μ_1 : (a : Set 𝕜) → ℝ≥0∞) {x : 𝕜 | r < ‖x‖})
  atTop (𝓝 0)
Tactic: rw [isTightMeasureSet_iff_tendsto_measure_norm_gt] at h_tight
Cleared hypotheses: h_tight
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
n : ℕ
h_tight :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ⨆ (μ_1 : Measure 𝕜),
        ⨆ (_ : Membership.mem (γ := Set (Measure 𝕜)) {Measure.map (fun (x : E) ↦ ⟪z, x⟫_𝕜) (μ n)} μ_1),
          (μ_1 : (a : Set 𝕜) → ℝ≥0∞) {x : 𝕜 | r < ‖x‖})
    atTop (𝓝 0)
r : ℝ
⊢ Measurable.{u_1, u_2} (β := 𝕜) fun (x : E) ↦ ⟪z, x⟫_𝕜
have funProp : mE ≤ mE
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
n : ℕ
h_tight :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ⨆ (μ_1 : Measure 𝕜),
        ⨆ (_ : Membership.mem (γ := Set (Measure 𝕜)) {Measure.map (fun (x : E) ↦ ⟪z, x⟫_𝕜) (μ n)} μ_1),
          (μ_1 : (a : Set 𝕜) → ℝ≥0∞) {x : 𝕜 | r < ‖x‖})
    atTop (𝓝 0)
r : ℝ
funProp : mE ≤ mE
⊢ Measurable.{u_1, u_2} (β := 𝕜) fun (x : E) ↦ ⟪z, x⟫_𝕜
have funProp₁ : MeasurableEmbedding.{u_1, u_2} (β := 𝕜) fun (x : E) ↦ ⟪z, x⟫_𝕜
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
n : ℕ
h_tight :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ⨆ (μ_1 : Measure 𝕜),
        ⨆ (_ : Membership.mem (γ := Set (Measure 𝕜)) {Measure.map (fun (x : E) ↦ ⟪z, x⟫_𝕜) (μ n)} μ_1),
          (μ_1 : (a : Set 𝕜) → ℝ≥0∞) {x : 𝕜 | r < ‖x‖})
    atTop (𝓝 0)
r : ℝ
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (fun (x : E) ↦ ⟪z, x⟫_𝕜) (μ n) : Measure 𝕜) : (a : Set 𝕜) → ℝ≥0∞) {x : 𝕜 | r < ‖x‖} : ℝ≥0∞)
    ((μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((μ n : (a : Set E) → ℝ≥0∞) (Set.preimage.{u_1, u_2} (β := 𝕜) (fun (x : E) ↦ ⟪z, x⟫_𝕜) {x : 𝕜 | r < ‖x‖}) : ℝ≥0∞)
  ((μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} : ℝ≥0∞)
Tactic: rw [Measure.map_apply (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
n : ℕ
h_tight :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ⨆ (μ_1 : Measure 𝕜),
        ⨆ (_ : Membership.mem (γ := Set (Measure 𝕜)) {Measure.map (fun (x : E) ↦ ⟪z, x⟫_𝕜) (μ n)} μ_1),
          (μ_1 : (a : Set 𝕜) → ℝ≥0∞) {x : 𝕜 | r < ‖x‖})
    atTop (𝓝 0)
r : ℝ
rw :
  Eq (α := ℝ≥0∞)
    ((μ n : (a : Set E) → ℝ≥0∞) (Set.preimage.{u_1, u_2} (β := 𝕜) (fun (x : E) ↦ ⟪z, x⟫_𝕜) {x : 𝕜 | r < ‖x‖}) : ℝ≥0∞)
    ((μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (fun (x : E) ↦ ⟪z, x⟫_𝕜) (μ n) : Measure 𝕜) : (a : Set 𝕜) → ℝ≥0∞) {x : 𝕜 | r < ‖x‖} : ℝ≥0∞)
    ((μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} : ℝ≥0∞)
have rw₁ : MeasurableSet.{u_2} (α := 𝕜) {x : 𝕜 | r < ‖x‖}
Tactic: rw [Measure.map_apply (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
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 : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
n : ℕ
h_tight :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ⨆ (μ_1 : Measure 𝕜),
        ⨆ (_ : Membership.mem (γ := Set (Measure 𝕜)) {Measure.map (fun (x : E) ↦ ⟪z, x⟫_𝕜) (μ n)} μ_1),
          (μ_1 : (a : Set 𝕜) → ℝ≥0∞) {x : 𝕜 | r < ‖x‖})
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)
have h_map : ∀ (r : ℝ),
  Eq (α := ℝ≥0∞)
    (((Measure.map (fun (x : E) ↦ ⟪z, x⟫_𝕜) (μ n) : Measure 𝕜) : (a : Set 𝕜) → ℝ≥0∞) {x : 𝕜 | r < ‖x‖} : ℝ≥0∞)
    ((μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} : ℝ≥0∞)
Tactic: have h_map r : (μ n).map (fun x ↦ ⟪z, x⟫_𝕜) {x | r < ‖x‖} = μ n {x | r < ‖⟪z, x⟫_𝕜‖} := by
    rw [Measure.map_apply (by fun_prop)]
    · simp
    · exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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)
⊢ IsTightMeasureSet (Set.range μ) ↔
    ∀ (y : E),
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
have refine : ∀ (h : IsTightMeasureSet (Set.range μ)) (z : E),
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
Tactic: refine ⟨fun h z ↦ ?_, isTightMeasureSet_range_of_tendsto_limsup_inner 𝕜⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 : IsTightMeasureSet (Set.range μ)
z : E
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
have rw : ∀
  (h :
    ∀ (y : E),
      Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop
        (𝓝 0))
  (z : E),
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
Tactic: rw [isTightMeasureSet_iff_inner_tendsto 𝕜] at h
Cleared hypotheses: h, z
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
have 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⟫_𝕜‖})
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (h z)
    (fun _ ↦ zero_le) fun r ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 (α := (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⟫_𝕜‖})
have 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⟫_𝕜‖})
Tactic: simp_rw [iSup_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 μ)
have refine : ∀ (y : E),
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
Tactic: refine isTightMeasureSet_range_of_tendsto_limsup_inner 𝕜 fun y ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
have pos : ∀ (hy : y = 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
have neg : ∀ (hy : ¬y = 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 < ‖⟪y, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
have pos : Tendsto (β := ℝ≥0∞)
  (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) atTop) atTop
  (𝓝 0)
Tactic: simp only [hy, inner_zero_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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)
have 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
Tactic: refine (tendsto_congr' ?_).mpr tendsto_const_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
⊢ 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
have 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
Tactic: filter_upwards [eventually_ge_atTop 0] with r hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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)
have specialize : ‖HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y‖ = 1
Tactic: specialize h ((‖y‖⁻¹ : 𝕜) • y) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
⊢ 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)
have 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)
Tactic: specialize h ((‖y‖⁻¹ : 𝕜) • y) ?_
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
⊢ ‖HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y‖ = 1
have simp : ‖y‖⁻¹ * ‖y‖ = 1
Tactic: simp only [norm_smul, norm_inv, norm_algebraMap', Real.norm_eq_abs, abs_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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‖⁻¹ * ‖y‖ = 1
have rw : Eq (α := ℝ) 1 1
Tactic: rw [inv_mul_cancel₀ (by positivity)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
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 < ‖⟪y, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
have 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)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 | r < ‖⟪y, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
have h₁ : ∀ (r : ℝ) (n : ℕ) (x : E), r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖
Tactic: convert! h' using 7 with r n x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
⊢ r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖⟪HSMul.hSMul.{u_2, u_1, u_1} (α := 𝕜) (↑‖y‖ : 𝕜)⁻¹ y, x⟫_𝕜‖
have h₁ : r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑‖y‖ : 𝕜)⁻¹ : 𝕜) ⟪y, x⟫_𝕜‖
Tactic: rw [inner_smul_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
⊢ r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑‖y‖ : 𝕜)⁻¹ : 𝕜) ⟪y, x⟫_𝕜‖
have h₁ : r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖y‖⁻¹ * ‖⟪y, x⟫_𝕜‖
Tactic: simp only [map_inv₀, RCLike.conj_ofReal, norm_mul, norm_inv, norm_algebraMap', norm_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
⊢ r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖y‖⁻¹ * ‖⟪y, x⟫_𝕜‖
have h₁ : 0 < ‖y‖⁻¹
Tactic: rw [mul_lt_mul_iff_right₀]