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
ι : Type u_3
inst_1 : RCLike 𝕜
inst_2 : Fintype ι
inst_3 : InnerProductSpace 𝕜 E
inst_4 : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (i : ι),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
      atTop (𝓝 0)
hE : Nontrivial E
h_rank : LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)
this_1 : Nonempty ι
this : ProperSpace E
r : ℝ
μ : Measure E
hμS : μ ∈ S
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖} : ℝ≥0∞)
    (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖} : ℝ≥0∞)

Tactic:
le_biSup (fun μ ↦ μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) hμS

Premises used: le_biSup
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst_1 : RCLike 𝕜
inst_2 : Fintype ι
inst_3 : InnerProductSpace 𝕜 E
inst_4 : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (i : ι),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
      atTop (𝓝 0)
hE : Nontrivial E
h_rank : LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)
this_1 : Nonempty ι
this : ProperSpace E
r : ℝ
μ : Measure E
hμS : μ ∈ S
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖} : ℝ≥0∞)
    (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖} : ℝ≥0∞)

Tactic:
exact le_biSup (fun μ ↦ μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) hμS

Premises used: le_biSup
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst_1 : RCLike 𝕜
inst_2 : Fintype ι
inst_3 : InnerProductSpace 𝕜 E
inst_4 : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (i : ι),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
      atTop (𝓝 0)
hE : Nontrivial E
h_rank : LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)
this_1 : Nonempty ι
this : ProperSpace E
r : ℝ
calc :
  LE.le (α := ℝ≥0∞) (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖})
    (⨆ μ ∈ S,
      (μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ι), {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}))
calc₁ :
  LE.le (α := ℝ≥0∞)
    (⨆ μ ∈ S,
      (μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ι), {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}))
    (⨆ μ ∈ S, ∑ i : ι, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
calc₂ :
  LE.le (α := ℝ≥0∞)
    (⨆ μ ∈ S, ∑ i : ι, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
    (∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
⊢ LE.le (α := (fun (r : ℝ) ↦ ℝ≥0∞) r) ((fun (r : ℝ) ↦ (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖} : ℝ≥0∞)) r)
    ((fun (r : ℝ) ↦
        (∑ i : ι,
            ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖} :
          ℝ≥0∞))
      r)

Tactic:
calc ⨆ μ ∈ S, μ {x | r < ‖x‖}
    _ ≤ ⨆ μ ∈ S, μ (⋃ i, {x : E | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) := by
      gcongr with μ hμS
      intro x hx
      simp only [Set.mem_setOf_eq, Set.mem_iUnion] at hx ⊢
      have hx' : r < √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫_𝕜‖ :=
        hx.trans_le (b.norm_le_card_mul_iSup_norm_inner x)
      rw [← div_lt_iff₀' (by positivity)] at hx'
      by_contra! h_le
      exact lt_irrefl (r / √(Fintype.card ι)) (hx'.trans_le (ciSup_le h_le))
    _ ≤ ⨆ μ ∈ S, ∑ i, μ {x : E | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} := by
      gcongr with μ hμS
      exact measure_iUnion_fintype_le μ _
    _ ≤ ∑ i, ⨆ μ ∈ S, μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} := by
      refine iSup_le fun μ ↦ (iSup_le fun hμS ↦ ?_)
      gcongr with i
      exact le_biSup (fun μ ↦ μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) hμS
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst_1 : RCLike 𝕜
inst_2 : Fintype ι
inst_3 : InnerProductSpace 𝕜 E
inst_4 : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (i : ι),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
      atTop (𝓝 0)
hE : Nontrivial E
h_rank : LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)
this_1 : Nonempty ι
this : ProperSpace E
⊢ LE.le (α := (r : ℝ) → ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) fun (r : ℝ) ↦
    ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}

Tactic:
have h_le : (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖})
      ≤ fun r ↦ ∑ i, ⨆ μ ∈ S, μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} := by
    intro r
    calc ⨆ μ ∈ S, μ {x | r < ‖x‖}
    _ ≤ ⨆ μ ∈ S, μ (⋃ i, {x : E | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) := by
      gcongr with μ hμS
      intro x hx
      simp only [Set.mem_setOf_eq, Set.mem_iUnion] at hx ⊢
      have hx' : r < √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫_𝕜‖ :=
        hx.trans_le (b.norm_le_card_mul_iSup_norm_inner x)
      rw [← div_lt_iff₀' (by positivity)] at hx'
      by_contra! h_le
      exact lt_irrefl (r / √(Fintype.card ι)) (hx'.trans_le (ciSup_le h_le))
    _ ≤ ⨆ μ ∈ S, ∑ i, μ {x : E | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} := by
      gcongr with μ hμS
      exact measure_iUnion_fintype_le μ _
    _ ≤ ∑ i, ⨆ μ ∈ S, μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} := by
      refine iSup_le fun μ ↦ (iSup_le fun hμS ↦ ?_)
      gcongr with i
      exact le_biSup (fun μ ↦ μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) hμS
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst_1 : RCLike 𝕜
inst_2 : Fintype ι
inst_3 : InnerProductSpace 𝕜 E
inst_4 : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (i : ι),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
      atTop (𝓝 0)
hE : Nontrivial E
h_rank : LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)
this_1 : Nonempty ι
this : ProperSpace E
h_le :
  LE.le (α := (r : ℝ) → ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) fun (r : ℝ) ↦
    ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ?_ (fun _ ↦ zero_le) h_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
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst_1 : RCLike 𝕜
inst_2 : Fintype ι
inst_3 : InnerProductSpace 𝕜 E
inst_4 : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (i : ι),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
      atTop (𝓝 0)
hE : Nontrivial E
h_rank : LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)
this_1 : Nonempty ι
this : ProperSpace E
h_le :
  LE.le (α := (r : ℝ) → ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) fun (r : ℝ) ↦
    ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}
inr :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ?_ (fun _ ↦ zero_le) h_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
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst_1 : RCLike 𝕜
inst_2 : Fintype ι
inst_3 : InnerProductSpace 𝕜 E
inst_4 : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (i : ι),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
      atTop (𝓝 0)
hE : Nontrivial E
h_rank : LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)
this_1 : Nonempty ι
this : ProperSpace E
h_le :
  LE.le (α := (r : ℝ) → ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) fun (r : ℝ) ↦
    ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}
inr :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
    atTop (𝓝 (∑ _x : ι, 0))
rw : Type u_3
rw₁ : Finset ι
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
    atTop (𝓝 0)

Tactic:
rw [← Finset.sum_const_zero]

Premises used: Finset.sum_const_zero
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst_1 : RCLike 𝕜
inst_2 : Fintype ι
inst_3 : InnerProductSpace 𝕜 E
inst_4 : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (i : ι),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
      atTop (𝓝 0)
hE : Nontrivial E
h_rank : LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)
this_1 : Nonempty ι
this : ProperSpace E
h_le :
  LE.le (α := (r : ℝ) → ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) fun (r : ℝ) ↦
    ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
    atTop (𝓝 (∑ _x : ι, 0))

Tactic:
tendsto_finsetSum Finset.univ fun i _ ↦ (h i).comp ?_

Premises used: Finset.univ, tendsto_finsetSum, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
Goal:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst_1 : RCLike 𝕜
inst_2 : Fintype ι
inst_3 : InnerProductSpace 𝕜 E
inst_4 : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (i : ι),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
      atTop (𝓝 0)
hE : Nontrivial E
h_rank : LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)
this_1 : Nonempty ι
this : ProperSpace E
h_le :
  LE.le (α := (r : ℝ) → ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) fun (r : ℝ) ↦
    ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
⊢ 0 < √(↑(Fintype.card ι) : ℝ)

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
ι : Type u_3
inst_1 : RCLike 𝕜
inst_2 : Fintype ι
inst_3 : InnerProductSpace 𝕜 E
inst_4 : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (i : ι),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
      atTop (𝓝 0)
hE : Nontrivial E
h_rank : LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)
this_1 : Nonempty ι
this : ProperSpace E
h_le :
  LE.le (α := (r : ℝ) → ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) fun (r : ℝ) ↦
    ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Tendsto (β := ℝ) (fun (r : ℝ) ↦ r / √(↑(Fintype.card ι) : ℝ)) atTop atTop

Tactic:
exact tendsto_id.atTop_div_const (by positivity)

Premises used: Filter.tendsto_id, Filter.Tendsto.atTop_div_const
-- 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 :
  ∀ (y : E), Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)
⊢ IsTightMeasureSet S

Tactic:
isTightMeasureSet_of_forall_basis_tendsto (stdOrthonormalBasis 𝕜 E)
    fun i ↦ h (stdOrthonormalBasis 𝕜 E i)

Premises used: DFunLike.coe, MeasureTheory.isTightMeasureSet_of_forall_basis_tendsto, stdOrthonormalBasis
-- 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
⊢ IsTightMeasureSet S ↔
    ∀ (y : E),
      Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)

Tactic:
⟨fun h y ↦ ?_, isTightMeasureSet_of_inner_tendsto 𝕜⟩

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

Tactic:
refine ⟨fun h y ↦ ?_, isTightMeasureSet_of_inner_tendsto 𝕜⟩
-- 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 : IsTightMeasureSet S
y : E
⊢ ProperSpace E

Tactic:
have : ProperSpace E := FiniteDimensional.proper 𝕜 E
-- 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 : IsTightMeasureSet S
y : E
this : ProperSpace E
rw :
  ∀ (h : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)) (y : E)
    (this : ProperSpace E),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)

Tactic:
rw [isTightMeasureSet_iff_tendsto_measure_norm_gt] at h

Premises used: MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt
-- 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
pos :
  ∀ (hy : y = 0),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)
neg :
  ∀ (hy : ¬y = 0),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)

Tactic:
by_cases hy : y = 0
-- 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
pos :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) 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
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
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) 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
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
pos :
  EventuallyEq (β := ℝ≥0∞) atTop (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0})
    fun (x : ℝ) ↦ 0
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) 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
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₁ : ∀ (r : ℝ) (hr : 0 ≤ r), Eq (α := ℝ≥0∞) (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) 0
⊢ EventuallyEq (β := ℝ≥0∞) atTop (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0})
    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
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
r : ℝ
hr : 0 ≤ r
⊢ Eq (α := ℝ≥0∞) (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) 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
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
⊢ 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
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)

Tactic:
have h' : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0) :=
    h.comp <| (tendsto_mul_const_atTop_of_pos (by positivity)).mpr tendsto_id
-- 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)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h' (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
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)
neg :
  LE.le (α := ℝ → ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) fun (r : ℝ) ↦
    ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖}
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h' (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
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:
measure_mono fun x hx ↦ ?_

Premises used: MeasureTheory.measure_mono
-- 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
refine :
  ∀ (x : E) (hx : Membership.mem (γ := Set E) {x : E | r < ‖⟪y, x⟫_𝕜‖} x),
    Membership.mem (γ := Set E) {x : E | r * ‖y‖⁻¹ < ‖x‖} x
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {x : E | r * ‖y‖⁻¹ < ‖x‖} : ℝ≥0∞)

Tactic:
refine measure_mono fun x hx ↦ ?_

Premises used: MeasureTheory.measure_mono