awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⟫_𝕜‖}))
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⟫_𝕜‖})
⊢ 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, ∑ 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: 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 (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
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖x‖}) atTop (𝓝 0)
have 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⟫_𝕜‖}
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
-- 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
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)
have inr : Tendsto (β := ℝ≥0∞)
  (fun (r : ℝ) ↦
    ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
  atTop (𝓝 0)
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ?_ (fun _ ↦ zero_le) 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
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 (𝓝 0)
have inr : Tendsto (β := ℝ≥0∞)
  (fun (r : ℝ) ↦
    ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
  atTop (𝓝 (∑ _x : ι, 0))
Tactic: rw [← Finset.sum_const_zero]
-- 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
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
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      ∑ i : ι, ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r / √(↑(Fintype.card ι) : ℝ) < ‖⟪(b : (a : ι) → E) i, x⟫_𝕜‖})
    atTop (𝓝 0)
have rw₁ : Finset ι
Tactic: rw [← Finset.sum_const_zero]
-- 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
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)
have refine : ∀ (h : 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 𝕜⟩
-- 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
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : IsTightMeasureSet S
y : E
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)
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
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
h : IsTightMeasureSet S
y : E
this : ProperSpace E
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)
have 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)
Tactic: rw [isTightMeasureSet_iff_tendsto_measure_norm_gt] at h
Cleared hypotheses: h, y, this
-- 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
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
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)
have pos : ∀ (hy : y = 0),
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)
have neg : ∀ (hy : ¬y = 0),
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
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)
have pos : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) atTop (𝓝 0)
Tactic: simp only [hy, inner_zero_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
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)
have pos : EventuallyEq (β := ℝ≥0∞) atTop (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0})
  fun (x : ℝ) ↦ 0
Tactic: refine (tendsto_congr' ?_).mpr tendsto_const_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
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
⊢ EventuallyEq (β := ℝ≥0∞) atTop (fun (r : ℝ) ↦ ⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0})
    fun (x : ℝ) ↦ 0
have h₁ : ∀ (r : ℝ) (hr : 0 ≤ r), Eq (α := ℝ≥0∞) (⨆ μ ∈ S, (μ : (a : Set E) → ℝ≥0∞) {x : E | r < norm.{u_2} (E := 𝕜) 0}) 0
Tactic: filter_upwards [eventually_ge_atTop 0] with r hr
-- 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
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)
have h' : 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
-- 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
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)
have 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‖}
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h' (fun _ ↦ zero_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
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∞)
have refine : ∀ (x : E) (hx : Membership.mem (γ := Set E) {x : E | r < ‖⟪y, x⟫_𝕜‖} x),
  Membership.mem (γ := Set E) {x : E | r * ‖y‖⁻¹ < ‖x‖} x
Tactic: refine measure_mono fun x 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
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‖
have rw : r < ‖x‖ * ‖y‖
Tactic: rw [mul_inv_lt_iff₀]
-- 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
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‖
⊢ r * ‖y‖⁻¹ < ‖x‖
have rw₁ : 0 < ‖y‖
Tactic: rw [mul_inv_lt_iff₀]
-- 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
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 < ‖x‖ * ‖y‖
have rw : r < ‖y‖ * ‖x‖
Tactic: rw [mul_comm]
-- 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
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 : ℝ
⊢ 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)
have 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∞)
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
-- 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
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)
have 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∞)
Tactic: refine iSup₂_le_iff.mpr fun μ hμS ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
⊢ IsTightMeasureSet (Set.range μ)
have refine : ∀ (z : E),
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop
    (𝓝 0)
Tactic: refine isTightMeasureSet_of_inner_tendsto 𝕜 fun z ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ μ_1 ∈ Set.range μ, (μ_1 : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop
    (𝓝 0)
have simp_rw : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ (i : ℕ), (μ i : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)
Tactic: simp_rw [iSup_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ⨆ (i : ℕ), (μ i : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)
have refine : ∀ (n : ℕ), Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ (μ n : (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop)
      atTop (𝓝 0)
z : E
n : ℕ
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)
have h_tight : 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