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
inst_1 : BorelSpace E
inst_2 : ProperSpace E
μ : ℕ → Measure E
inst_3 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
    (𝓝 0)
n : ℕ
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
have h_tight : IsTightMeasureSet (𝓧 := E) (m𝓧 := mE) {μ n}
Tactic: have h_tight : IsTightMeasureSet {μ n} := isTightMeasureSet_singleton
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
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 :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
    (𝓝 0)
n : ℕ
h_tight : IsTightMeasureSet (𝓧 := E) (m𝓧 := mE) {μ n}
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
have h_tight₁ : Tendsto (β := ℝ≥0∞)
  (fun (r : ℝ) ↦
    ⨆ (μ_1 : Measure E),
      ⨆ (_ : Membership.mem (γ := Set (Measure E)) {μ n} μ_1), (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | 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
inst_1 : BorelSpace E
inst_2 : ProperSpace E
μ : ℕ → Measure E
inst_3 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
⊢ IsTightMeasureSet (Set.range μ) ↔
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
      (𝓝 0)
have refine : ∀ (h : IsTightMeasureSet (Set.range μ)),
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
    (𝓝 0)
Tactic: refine ⟨fun h ↦ ?_, isTightMeasureSet_range_of_tendsto_limsup_measure_norm_gt⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
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 μ)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
    (𝓝 0)
have h_sup : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
Tactic: have h_sup := tendsto_measure_norm_gt_of_isTightMeasureSet h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop) atTop
    (𝓝 0)
have refine : LE.le (α := ℝ → ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop)
  fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h_sup (fun _ ↦ zero_le) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 (α := (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)
have 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‖})
Tactic: simp_rw [iSup_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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)
⊢ IsTightMeasureSet S
have inl : ∀ (hE : Subsingleton E), IsTightMeasureSet S
Tactic: rcases subsingleton_or_nontrivial E with hE | hE
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
⊢ IsTightMeasureSet S
have inr : ∀ (hE : Nontrivial E), IsTightMeasureSet S
Tactic: rcases subsingleton_or_nontrivial E with hE | hE
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
⊢ IsTightMeasureSet S
have inl : Tendsto.{u_1, 0} (α := Set E) (β := ℝ≥0∞) (⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) (pure ∅) (𝓝 0)
Tactic: simp only [IsTightMeasureSet, cocompact_eq_bot, smallSets_bot]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 ∅) (𝓝 0)
have h₁ : Eq (α := ℝ≥0∞) 0 ((⨆ μ ∈ S, (⇑μ : (a : Set E) → ℝ≥0∞)) ∅)
Tactic: convert! tendsto_pure_nhds (a := ∅) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
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
⊢ IsTightMeasureSet S
have h_rank : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
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 ι) : ℝ)
⊢ IsTightMeasureSet S
have this : Nonempty ι
Tactic: have : Nonempty ι := by simpa [Fintype.card_pos_iff] using h_rank
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
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 ι
⊢ IsTightMeasureSet S
have this₁ : ProperSpace E
Tactic: have : ProperSpace E := FiniteDimensional.proper 𝕜 E
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
have inr : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
Tactic: refine isTightMeasureSet_of_tendsto_measure_norm_gt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖})
    (⨆ μ ∈ S,
      (μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ι), {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}))
have 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⟫_𝕜‖})
Tactic: gcongr with μ hμS
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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
⊢ Membership.mem (γ := Set E) (⋃ (i : ι), {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖}) x
have h₁ : ∃ (i : ι), r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖
Tactic: simp only [Set.mem_setOf_eq, Set.mem_iUnion] at hx ⊢
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
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‖
⊢ ∃ (i : ι), r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖
have hx' : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
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⟫_𝕜‖
⊢ ∃ (i : ι), r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖
have hx'₁ : r / √(↑(Fintype.card ι) : ℝ) < ⨆ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖
Tactic: rw [← div_lt_iff₀' (by positivity)] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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⟫_𝕜‖
⊢ ∃ (i : ι), r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖
have h₁ : ∀ (h_le : ∀ (i : ι), ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖ ≤ r / √(↑(Fintype.card ι) : ℝ)), False
Tactic: by_contra! h_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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,
      (μ : (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⟫_𝕜‖})
have 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∞)
Tactic: gcongr with μ hμS
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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⟫_𝕜‖})
have 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⟫_𝕜‖})
Tactic: refine iSup_le fun μ ↦ (iSup_le fun hμS ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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∞)
    (∑ 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⟫_𝕜‖})
have 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∞)
Tactic: gcongr with i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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 (α := (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)
have 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⟫_𝕜‖}))
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
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⟫_𝕜‖}))
⊢ 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)
have 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⟫_𝕜‖})
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