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

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
inst_1 : BorelSpace E
inst_2 : ProperSpace E
μ : ℕ → Measure E
inst_3 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : IsTightMeasureSet (Set.range μ)
h_sup :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
r : ℝ
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop)
    (⨆ (n : ℕ), (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖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
inst_1 : BorelSpace E
inst_2 : ProperSpace E
μ : ℕ → Measure E
inst_3 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : IsTightMeasureSet (Set.range μ)
h_sup :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
r : ℝ
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop)
    (⨆ (n : ℕ), (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖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
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)
inl : ∀ (hE : Subsingleton E), IsTightMeasureSet S
inr : ∀ (hE : Nontrivial E), IsTightMeasureSet S
⊢ IsTightMeasureSet S

Tactic:
rcases subsingleton_or_nontrivial E with hE | hE

Premises used: subsingleton_or_nontrivial
-- 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 : Subsingleton E
inl : Tendsto.{u_1, 0} (α := Set E) (β := ℝ≥0∞) (⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) (pure ∅) (𝓝 0)
⊢ IsTightMeasureSet S

Tactic:
simp only [IsTightMeasureSet, cocompact_eq_bot, smallSets_bot]

Premises used: Filter.smallSets_bot, MeasureTheory.IsTightMeasureSet, Filter.cocompact_eq_bot
-- 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 : Subsingleton E
⊢ Tendsto.{u_1, 0} (α := Set E) (β := ℝ≥0∞) (⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) (pure ∅)
    (𝓝 ((⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) ∅))

Tactic:
tendsto_pure_nhds (a := ∅) _

Premises used: tendsto_pure_nhds, EmptyCollection.emptyCollection
-- 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 : Subsingleton E
h₁ : Eq (α := ℝ≥0∞) 0 ((⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) ∅)
⊢ Tendsto.{u_1, 0} (α := Set E) (β := ℝ≥0∞) (⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) (pure ∅) (𝓝 0)

Tactic:
convert! tendsto_pure_nhds (a := ∅) _

Premises used: tendsto_pure_nhds, EmptyCollection.emptyCollection
-- 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 : Subsingleton E
⊢ Eq (α := ℝ≥0∞) 0 ((⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) ∅)

Tactic:
simp
-- 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
⊢ LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)

Tactic:
simpa [← Module.finrank_eq_card_basis b.toBasis, Module.finrank_pos_iff]

Premises used: Module.finrank_eq_card_basis, Module.finrank_pos_iff, OrthonormalBasis.toBasis
-- 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
⊢ LT.lt (α := ℝ) 0 (↑(Fintype.card ι) : ℝ)

Tactic:
have h_rank : (0 : ℝ) < Fintype.card ι := by
    simpa [← Module.finrank_eq_card_basis b.toBasis, Module.finrank_pos_iff]
-- 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 ι) : ℝ)
⊢ Nonempty ι

Tactic:
simpa [Fintype.card_pos_iff] using h_rank

Premises used: Fintype.card_pos_iff
-- 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 ι) : ℝ)
⊢ Nonempty ι

Tactic:
have : Nonempty ι := by simpa [Fintype.card_pos_iff] using h_rank
-- 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 : Nonempty ι
⊢ 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
ι : 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
⊢ IsTightMeasureSet S

Tactic:
isTightMeasureSet_of_tendsto_measure_norm_gt ?_

Premises used: MeasureTheory.isTightMeasureSet_of_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
ι : 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
inr : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
⊢ IsTightMeasureSet S

Tactic:
refine isTightMeasureSet_of_tendsto_measure_norm_gt ?_

Premises used: MeasureTheory.isTightMeasureSet_of_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
ι : 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 : ℝ
h₁ :
  ∀ (μ : Measure E) (hμS : μ ∈ S),
    Subset.{u_1} (α := Set E) {x : E | r < ‖x‖}
      (⋃ (i : ι), {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
⊢ 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⟫_𝕜‖}))

Tactic:
gcongr with μ 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
r : ℝ
μ : Measure E
hμS : μ ∈ S
x : E
hx : Membership.mem (γ := Set E) {x : E | r < ‖x‖} x
h₁ : ∃ (i : ι), r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖
⊢ Membership.mem (γ := Set E) (⋃ (i : ι), {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}) x

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_iUnion] at hx ⊢

Premises used: Set.mem_iUnion, Set.mem_setOf_eq
-- 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
x : E
hx : r < ‖x‖
⊢ r < √(↑(Fintype.card ι) : ℝ) * ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖

Tactic:
have hx' : r < √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫_𝕜‖ :=
        hx.trans_le (b.norm_le_card_mul_iSup_norm_inner x)
-- 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
x : E
hx : r < ‖x‖
hx' : r < √(↑(Fintype.card ι) : ℝ) * ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖
⊢ 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
r : ℝ
μ : Measure E
hμS : μ ∈ S
x : E
hx : r < ‖x‖
hx' : r < √(↑(Fintype.card ι) : ℝ) * ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖
⊢ r / √(↑(Fintype.card ι) : ℝ) < ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖

Tactic:
rw [← div_lt_iff₀' (by positivity)] at hx'

Premises used: div_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
ι : 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
x : E
hx : r < ‖x‖
hx' : r / √(↑(Fintype.card ι) : ℝ) < ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖
h₁ : ∀ (h_le : ∀ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖ ≤ r / √(↑(Fintype.card ι) : ℝ)), False
⊢ ∃ (i : ι), r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖

Tactic:
by_contra! 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
ι : 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
x : E
hx : r < ‖x‖
hx' : r / √(↑(Fintype.card ι) : ℝ) < ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖
h_le : ∀ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖ ≤ r / √(↑(Fintype.card ι) : ℝ)
⊢ False

Tactic:
lt_irrefl (r / √(Fintype.card ι)) (hx'.trans_le (ciSup_le h_le))

Premises used: lt_irrefl, Fintype.card, HDiv.hDiv, Nat.cast, LT.lt.trans_le, Real.sqrt, ciSup_le
-- 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
x : E
hx : r < ‖x‖
hx' : r / √(↑(Fintype.card ι) : ℝ) < ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖
h_le : ∀ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖ ≤ r / √(↑(Fintype.card ι) : ℝ)
⊢ False

Tactic:
exact lt_irrefl (r / √(Fintype.card ι)) (hx'.trans_le (ciSup_le h_le))

Premises used: lt_irrefl, Fintype.card, HDiv.hDiv, Nat.cast, LT.lt.trans_le, Real.sqrt, ciSup_le
-- 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 : ℝ
h₁ :
  ∀ (μ : Measure E) (hμS : μ ∈ S),
    LE.le (α := ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ι), {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}) :
        ℝ≥0∞)
      (∑ i : ι, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖} : ℝ≥0∞)
⊢ 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⟫_𝕜‖})

Tactic:
gcongr with μ 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
r : ℝ
μ : Measure E
hμS : μ ∈ S
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ι), {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}) : ℝ≥0∞)
    (∑ i : ι, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖} : ℝ≥0∞)

Tactic:
measure_iUnion_fintype_le μ _

Premises used: MeasureTheory.measure_iUnion_fintype_le
-- 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
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ι), {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}) : ℝ≥0∞)
    (∑ i : ι, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖} : ℝ≥0∞)

Tactic:
exact measure_iUnion_fintype_le μ _

Premises used: MeasureTheory.measure_iUnion_fintype_le
-- 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 : ℝ
⊢ 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⟫_𝕜‖})

Tactic:
iSup_le fun μ ↦ (iSup_le fun hμS ↦ ?_)

Premises used: iSup_le
-- 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 : ℝ
refine :
  ∀ (μ : Measure E) (hμS : μ ∈ S),
    LE.le (α := ℝ≥0∞)
      (∑ 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 (α := ℝ≥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⟫_𝕜‖})

Tactic:
refine iSup_le fun μ ↦ (iSup_le fun hμS ↦ ?_)

Premises used: iSup_le
-- 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
h₁ :
  ∀ (i : ι),
    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∞)
⊢ LE.le (α := ℝ≥0∞)
    (∑ 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⟫_𝕜‖})

Tactic:
gcongr with i