awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
μ : Measure E
x : E
hx : r < ‖⟪y, x⟫_𝕜‖
rw : r < ‖x‖ * ‖y‖
rw₁ : 0 < ‖y‖
⊢ r * ‖y‖⁻¹ < ‖x‖

Tactic:
rw [mul_inv_lt_iff₀]

Premises used: mul_inv_lt_iff₀
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
μ : Measure E
x : E
hx : r < ‖⟪y, x⟫_𝕜‖
rw : r < ‖y‖ * ‖x‖
⊢ r < ‖x‖ * ‖y‖

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
μ : Measure E
x : E
hx : r < ‖⟪y, x⟫_𝕜‖
⊢ r < ‖y‖ * ‖x‖

Tactic:
hx.trans_le (norm_inner_le_norm y x)

Premises used: LT.lt.trans_le, norm_inner_le_norm
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
μ : Measure E
x : E
hx : r < ‖⟪y, x⟫_𝕜‖
⊢ r < ‖y‖ * ‖x‖

Tactic:
exact hx.trans_le (norm_inner_le_norm y x)

Premises used: LT.lt.trans_le, norm_inner_le_norm
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
μ : Measure E
x : E
hx : r < ‖⟪y, x⟫_𝕜‖
⊢ 0 < ‖y‖

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
⊢ ∀ (μ : Measure E),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖} : ℝ≥0∞)

Tactic:
have h_le (μ : Measure E) : μ {x | r < ‖⟪y, x⟫_𝕜‖} ≤ μ {x | r * ‖y‖⁻¹ < ‖x‖} := by
    refine measure_mono fun x hx ↦ ?_
    simp only [Set.mem_setOf_eq] at hx ⊢
    rw [mul_inv_lt_iff₀]
    · rw [mul_comm]
      exact hx.trans_le (norm_inner_le_norm y x)
    · positivity
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
h_le :
  ∀ (μ : Measure E),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖} : ℝ≥0∞)
⊢ LE.le (α := (fun (a : ℝ) ↦ ℝ≥0∞) r)
    ((fun (r : ℝ) ↦ (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖} : ℝ≥0∞)) r)
    ((fun (r : ℝ) ↦ (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖} : ℝ≥0∞)) r)

Tactic:
iSup₂_le_iff.mpr fun μ hμS ↦ ?_

Premises used: Iff.mpr, iSup₂_le_iff
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
h_le :
  ∀ (μ : Measure E),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖} : ℝ≥0∞)
neg :
  ∀ (μ : Measure E) (hμS : μ ∈ S),
    LE.le (α := (fun (a : ℝ) ↦ ℝ≥0∞) r) ((μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖} : ℝ≥0∞)
      ((fun (r : ℝ) ↦ (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖} : ℝ≥0∞)) r : ℝ≥0∞)
⊢ LE.le (α := (fun (a : ℝ) ↦ ℝ≥0∞) r)
    ((fun (r : ℝ) ↦ (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖} : ℝ≥0∞)) r)
    ((fun (r : ℝ) ↦ (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖} : ℝ≥0∞)) r)

Tactic:
refine iSup₂_le_iff.mpr fun μ hμS ↦ ?_

Premises used: Iff.mpr, iSup₂_le_iff
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
h_le :
  ∀ (μ : Measure E),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖} : ℝ≥0∞)
μ : Measure E
hμS : μ ∈ S
⊢ LE.le (α := (fun (a : ℝ) ↦ ℝ≥0∞) r) ((μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖} : ℝ≥0∞)
    (⨆ (_ : μ ∈ S), (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖} : ℝ≥0∞)

Tactic:
simp [hμS, h_le]
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
h_le :
  ∀ (μ : Measure E),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖} : ℝ≥0∞)
μ : Measure E
hμS : μ ∈ S
⊢ LE.le (α := (fun (a : ℝ) ↦ ℝ≥0∞) r) ((μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖} : ℝ≥0∞)
    ((fun (r : ℝ) ↦ (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖} : ℝ≥0∞)) r : ℝ≥0∞)

Tactic:
exact le_iSup_of_le (i := μ) <| by simp [hμS, h_le]

Premises used: le_iSup_of_le
-- 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 : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
⊢ IsTightMeasureSet (Set.range μ)

Tactic:
isTightMeasureSet_of_inner_tendsto 𝕜 fun z ↦ ?_

Premises used: MeasureTheory.isTightMeasureSet_of_inner_tendsto
-- 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 : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
refine :
  ∀ (z : E),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop
      (𝓝 0)
⊢ IsTightMeasureSet (Set.range μ)

Tactic:
refine isTightMeasureSet_of_inner_tendsto 𝕜 fun z ↦ ?_

Premises used: MeasureTheory.isTightMeasureSet_of_inner_tendsto
-- 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 : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
simp_rw : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ (i : ℕ), (μ i : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop
    (𝓝 0)

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 : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
n : ℕ
u v : ℝ
huv : u ≤ v
⊢ LE.le (α := ℝ≥0∞) ((μ n : (a : Set E) → ℝ≥0∞) {x : E | v < ‖⟪z, x⟫_𝕜‖} : ℝ≥0∞)
    ((μ n : (a : Set E) → ℝ≥0∞) {x : E | u < ‖⟪z, x⟫_𝕜‖} : ℝ≥0∞)

Tactic:
gcongr
-- 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 : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
refine : ∀ (n : ℕ), Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ (i : ℕ), (μ i : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)

Tactic:
refine Nat.tendsto_iSup_of_tendsto_limsup (fun n ↦ ?_) (h z) (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
𝕜 : 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 : ℕ
⊢ IsTightMeasureSet (𝓧 := 𝕜) (m𝓧 := RCLike.measurableSpace) {Measure.map (fun (x : E) ↦ ⟪z, x⟫_𝕜) (μ n)}

Tactic:
have h_tight : IsTightMeasureSet {(μ n).map (fun x ↦ ⟪z, x⟫_𝕜)} := isTightMeasureSet_singleton
-- 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 : ℝ) ↦ 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 : ℝ) ↦
      ⨆ (μ_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

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
𝕜 : 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
funProp₁ : MeasurableEmbedding.{u_1, u_2} (β := 𝕜) fun (x : E) ↦ ⟪z, x⟫_𝕜
⊢ Measurable.{u_1, u_2} (β := 𝕜) fun (x : E) ↦ ⟪z, x⟫_𝕜

Tactic:
fun_prop
-- 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 : ℝ) ↦ 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∞)
rw₁ : MeasurableSet.{u_2} (α := 𝕜) {x : 𝕜 | r < ‖x‖}
⊢ 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:
rw [Measure.map_apply (by fun_prop)]

Premises used: MeasureTheory.Measure.map_apply
-- 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 : ℝ) ↦ 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∞)
    ((μ 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:
simp
-- 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 : ℝ) ↦ 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_2, 0} (α := 𝕜) norm

Tactic:
fun_prop
-- 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 : ℝ) ↦ 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 : ℝ
⊢ MeasurableSet.{u_2} (α := 𝕜) {x : 𝕜 | r < ‖x‖}

Tactic:
exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)

Premises used: MeasurableSet.preimage, measurableSet_Ioi
-- 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 : ℝ) ↦ 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∞)

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)
-- 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 : ℝ) ↦ 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)
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∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)

Tactic:
simpa [h_map] using h_tight
-- 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)
⊢ 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)

Tactic:
⟨fun h z ↦ ?_, isTightMeasureSet_range_of_tendsto_limsup_inner 𝕜⟩

Premises used: MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_inner, Iff.intro
-- 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)
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)
⊢ 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)

Tactic:
refine ⟨fun h z ↦ ?_, 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 : IsTightMeasureSet (Set.range μ)
z : E
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)
⊢ 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

Premises used: MeasureTheory.isTightMeasureSet_iff_inner_tendsto
-- 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
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)

Tactic:
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