awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
⊢ LE.le (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i : γ n, HPow.hPow (β := ℝ) (ediam (t n i)) (↑(Fintype.card ι) : ℝ)) atTop)
    (liminf (fun (n : ℕ) ↦ ∑ i : γ n, HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ^ Fintype.card ι) atTop)
have refine_1 : ∀ᶠ (a_1 : ℕ) in atTop,
  LE.le (α := ℝ≥0∞) (∑ i : γ a_1, HPow.hPow (β := ℝ) (ediam (t a_1 i)) (↑(Fintype.card ι) : ℝ))
    (∑ i : γ a_1, HDiv.hDiv (α := ℝ≥0∞) 1 (↑a_1 : ℝ≥0∞) ^ Fintype.card ι)
Tactic: refine liminf_le_liminf ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
refine_1 :
  ∀ᶠ (a_1 : ℕ) in atTop,
    LE.le (α := ℝ≥0∞) (∑ i : γ a_1, HPow.hPow (β := ℝ) (ediam (t a_1 i)) (↑(Fintype.card ι) : ℝ))
      (∑ i : γ a_1, HDiv.hDiv (α := ℝ≥0∞) 1 (↑a_1 : ℝ≥0∞) ^ Fintype.card ι)
⊢ LE.le (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i : γ n, HPow.hPow (β := ℝ) (ediam (t n i)) (↑(Fintype.card ι) : ℝ)) atTop)
    (liminf (fun (n : ℕ) ↦ ∑ i : γ n, HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ^ Fintype.card ι) atTop)
have refine_2 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦
  ∑ i : γ n, HPow.hPow (β := ℝ) (ediam (t n i)) (↑(Fintype.card ι) : ℝ)
Tactic: refine liminf_le_liminf ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
⊢ ∀ᶠ (a_1 : ℕ) in atTop,
    LE.le (α := ℝ≥0∞) (∑ i : γ a_1, HPow.hPow (β := ℝ) (ediam (t a_1 i)) (↑(Fintype.card ι) : ℝ))
      (∑ i : γ a_1, HDiv.hDiv (α := ℝ≥0∞) 1 (↑a_1 : ℝ≥0∞) ^ Fintype.card ι)
have h : ∀ (a_1 : ℕ) (hn : ∀ (i : γ a_1), ediam (t a_1 i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑a_1 : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) (∑ i : γ a_1, HPow.hPow (β := ℝ) (ediam (t a_1 i)) (↑(Fintype.card ι) : ℝ))
    (∑ i : γ a_1, HDiv.hDiv (α := ℝ≥0∞) 1 (↑a_1 : ℝ≥0∞) ^ Fintype.card ι)
Tactic: filter_upwards [B] with _ hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
a_1 : ℕ
hn : ∀ (i : γ a_1), ediam (t a_1 i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑a_1 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ i : γ a_1, HPow.hPow (β := ℝ) (ediam (t a_1 i)) (↑(Fintype.card ι) : ℝ))
    (∑ i : γ a_1, HDiv.hDiv (α := ℝ≥0∞) 1 (↑a_1 : ℝ≥0∞) ^ Fintype.card ι)
have apply : ∀ (i : γ a_1),
  Membership.mem (γ := Finset (γ a_1)) Finset.univ i →
    HPow.hPow (β := ℝ) (ediam (t a_1 i)) (↑(Fintype.card ι) : ℝ) ≤
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑a_1 : ℝ≥0∞) ^ Fintype.card ι
Tactic: apply Finset.sum_le_sum fun i _ => _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
a_1 : ℕ
hn : ∀ (i : γ a_1), ediam (t a_1 i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑a_1 : ℝ≥0∞)
⊢ ∀ (i : γ a_1),
    Membership.mem (γ := Finset (γ a_1)) Finset.univ i →
      HPow.hPow (β := ℝ) (ediam (t a_1 i)) (↑(Fintype.card ι) : ℝ) ≤
        HDiv.hDiv (α := ℝ≥0∞) 1 (↑a_1 : ℝ≥0∞) ^ Fintype.card ι
have simp : ∀ (i : γ a_1),
  Membership.mem (γ := Finset (γ a_1)) Finset.univ i →
    ediam (t a_1 i) ^ Fintype.card ι ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑a_1 : ℝ≥0∞) ^ Fintype.card ι
Tactic: simp only [ENNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
⊢ Eq (α := ℝ≥0∞)
    (liminf
      (fun (n : ℕ) ↦
        ∏ i : ι, HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞))
      atTop)
    (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)))
have simp : Eq (α := ℝ≥0∞)
  (liminf
    (fun (n : ℕ) ↦
      ∏ i : ι, HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞))
    atTop)
  (∏ x : ι, ENNReal.ofReal (HSub.hSub (α := ℝ) (↑(b x) : ℝ) (↑(a x) : ℝ)))
Tactic: simp only [Real.volume_Ioo]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
⊢ Eq (α := ℝ≥0∞)
    (liminf
      (fun (n : ℕ) ↦
        ∏ i : ι, HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞))
      atTop)
    (∏ x : ι, ENNReal.ofReal (HSub.hSub (α := ℝ) (↑(b x) : ℝ) (↑(a x) : ℝ)))
have h : Tendsto (β := ℝ≥0∞)
  (fun (n : ℕ) ↦
    ∏ i : ι, HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞))
  atTop (𝓝 (∏ x : ι, ENNReal.ofReal (HSub.hSub (α := ℝ) (↑(b x) : ℝ) (↑(a x) : ℝ))))
Tactic: apply Tendsto.liminf_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∏ i : ι, HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞))
    atTop (𝓝 (∏ x : ι, ENNReal.ofReal (HSub.hSub (α := ℝ) (↑(b x) : ℝ) (↑(a x) : ℝ))))
have h : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    Tendsto
      (fun (n : ℕ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞))
      atTop (𝓝 (ENNReal.ofReal (HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ))))
Tactic: refine ENNReal.tendsto_finsetProd_of_ne_top _ (fun i _ => ?_) fun i _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
h :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      Tendsto
        (fun (n : ℕ) ↦
          HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞))
        atTop (𝓝 (ENNReal.ofReal (HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ))))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∏ i : ι, HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞))
    atTop (𝓝 (∏ x : ι, ENNReal.ofReal (HSub.hSub (α := ℝ) (↑(b x) : ℝ) (↑(a x) : ℝ))))
have h₁ : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i → ENNReal.ofReal (HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)) ≠ ∞
Tactic: refine ENNReal.tendsto_finsetProd_of_ne_top _ (fun i _ => ?_) fun i _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Tendsto
    (fun (n : ℕ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞))
    atTop (𝓝 (ENNReal.ofReal (HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ))))
have this : ENNReal.ofReal ∘ (fun (x : ℝ) ↦ (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * x⌉₊ : ℝ) / x) ∘ Nat.cast =ᶠ[atTop]
  fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞)
Tactic: apply
          Tendsto.congr' _
            ((ENNReal.continuous_ofReal.tendsto _).comp
              ((tendsto_nat_ceil_mul_div_atTop (I i)).comp tendsto_natCast_atTop_atTop))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ENNReal.ofReal ∘ (fun (x : ℝ) ↦ (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * x⌉₊ : ℝ) / x) ∘ Nat.cast =ᶠ[atTop]
    fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞)
have apply : ∀ (n : ℕ) (hn : n ≥ 1),
  (ENNReal.ofReal ∘ (fun (x : ℝ) ↦ (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * x⌉₊ : ℝ) / x) ∘ Nat.cast) n =
    (fun (n : ℕ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞))
      n
Tactic: apply eventually_atTop.2 ⟨1, fun n hn => _⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
      Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
        ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ))
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
C :
  ∀ᶠ (n : ℕ) in atTop,
    Subset.{u_4} (α := Set ((i : ι) → ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
⊢ LE.le (α := ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
      ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
have univ : LE.le (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i : γ n, HPow.hPow (β := ℝ) (ediam (t n i)) (↑(Fintype.card ι) : ℝ)) atTop)
  (liminf (fun (n : ℕ) ↦ ∑ i : γ n, HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ^ Fintype.card ι) atTop)
Tactic: calc
    μH[Fintype.card ι] (Set.pi univ fun i : ι => Ioo (a i : ℝ) (b i)) ≤
        liminf (fun n : ℕ => ∑ i : γ n, ediam (t n i) ^ ((Fintype.card ι) : ℝ)) atTop :=
      hausdorffMeasure_le_liminf_sum _ (Set.pi univ fun i => Ioo (a i : ℝ) (b i))
        (fun n : ℕ => 1 / (n : ℝ≥0∞)) A t B C
    _ ≤ liminf (fun n : ℕ => ∑ i : γ n, (1 / (n : ℝ≥0∞)) ^ Fintype.card ι) atTop := by
      refine liminf_le_liminf ?_ ?_
      · filter_upwards [B] with _ hn
        apply Finset.sum_le_sum fun i _ => _
        simp only [ENNReal.rpow_natCast]
        intro i _
        exact pow_le_pow_left' (hn i) _
      · isBoundedDefault
    _ = liminf (fun n : ℕ => ∏ i : ι, (⌈((b i : ℝ) - a i) * n⌉₊ : ℝ≥0∞) / n) atTop := by
      simp only [γ, Finset.card_univ, Nat.cast_prod, one_mul, Fintype.card_fin, Finset.sum_const,
        nsmul_eq_mul, Fintype.card_pi, div_eq_mul_inv, Finset.prod_mul_distrib, Finset.prod_const]
    _ = ∏ i : ι, volume (Ioo (a i : ℝ) (b i)) := by
      simp only [Real.volume_Ioo]
      apply Tendsto.liminf_eq
      refine ENNReal.tendsto_finsetProd_of_ne_top _ (fun i _ => ?_) fun i _ => ?_
      · apply
          Tendsto.congr' _
            ((ENNReal.continuous_ofReal.tendsto _).comp
              ((tendsto_nat_ceil_mul_div_atTop (I i)).comp tendsto_natCast_atTop_atTop))
        apply eventually_atTop.2 ⟨1, fun n hn => _⟩
        intro n hn
        simp only [ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr hn), comp_apply,
          ENNReal.ofReal_natCast]
      · simp only [ENNReal.ofReal_ne_top, Ne, not_false_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
this :
  LT.lt (α := ℝ≥0∞)
    ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((μH[(↑(finrank ℝ E) : ℝ)] : Measure E) : (a : Set E) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞)
  (((μH[(↑(finrank ℝ E) : ℝ)] : Measure E) : (a : Set E) → ℝ≥0∞)
      (image (α := Fin (finrank ℝ E) → ℝ) (⇑e.symm : (a : Fin (finrank ℝ E) → ℝ) → E)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K)) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [← e.symm_image_image K]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
this :
  LT.lt (α := ℝ≥0∞)
    ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    (((μH[(↑(finrank ℝ E) : ℝ)] : Measure E) : (a : Set E) → ℝ≥0∞)
        (image (α := Fin (finrank ℝ E) → ℝ) (⇑e.symm : (a : Fin (finrank ℝ E) → ℝ) → E)
          ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
have apply : HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) (↑‖(↑e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊ : ℝ≥0∞) (↑(finrank ℝ E) : ℝ))
    ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
      ℝ≥0∞) <
  ∞
Tactic: apply lt_of_le_of_lt <| e.symm.lipschitz.hausdorffMeasure_image_le (by simp) (e '' K)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
this :
  LT.lt (α := ℝ≥0∞)
    ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞)
      (HPow.hPow (β := ℝ) (↑‖(↑e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊ : ℝ≥0∞) (↑(finrank ℝ E) : ℝ))
      ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
          ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
        ℝ≥0∞) <
    ∞
have rw : HMul.hMul (β := ℝ≥0∞) ((↑‖(↑e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊ : ℝ≥0∞) ^ finrank ℝ E)
    ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
      ℝ≥0∞) <
  ∞
Tactic: rw [ENNReal.rpow_natCast]