awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
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∞)
⊢ 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:
apply
          Tendsto.congr' _
            ((ENNReal.continuous_ofReal.tendsto _).comp
              ((tendsto_nat_ceil_mul_div_atTop (I i)).comp tendsto_natCast_atTop_atTop))

Premises used: ENNReal.continuous_ofReal, Continuous.tendsto, tendsto_natCast_atTop_atTop, tendsto_nat_ceil_mul_div_atTop, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
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
⊢ 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 eventually_atTop.2 ⟨1, fun n hn => _⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
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:
simp only [ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr hn), comp_apply,
          ENNReal.ofReal_natCast]

Premises used: Iff.mpr, Nat.cast_pos, ENNReal.ofReal_div_of_pos, Function.comp_apply, ENNReal.ofReal_natCast
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 (HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)) ≠ ∞

Tactic:
simp only [ENNReal.ofReal_ne_top, Ne, not_false_iff]

Premises used: Ne, ENNReal.ofReal_ne_top, not_false_iff
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ finrank ℝ E = finrank ℝ (Fin (finrank ℝ E) → ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
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∞)
⊢ LT.lt (α := ℝ≥0∞) (((μH[(↑(finrank ℝ E) : ℝ)] : Measure E) : (a : Set E) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← e.symm_image_image K]

Premises used: ContinuousLinearEquiv.symm_image_image
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
⊢ LE.le (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
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∞) <
    ∞
⊢ 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:
apply lt_of_le_of_lt <| e.symm.lipschitz.hausdorffMeasure_image_le (by simp) (e '' K)

Premises used: ContinuousLinearEquiv.symm, lt_of_le_of_lt, ContinuousLinearEquiv.lipschitz, Set.image, LipschitzWith.hausdorffMeasure_image_le, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
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∞) <
    ∞
⊢ 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:
rw [ENNReal.rpow_natCast]

Premises used: ENNReal.rpow_natCast
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞) ((↑‖(↑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:
ENNReal.mul_lt_top (ENNReal.pow_lt_top ENNReal.coe_lt_top) this

Premises used: ENNReal.pow_lt_top, ENNReal.mul_lt_top, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞) ((↑‖(↑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:
exact ENNReal.mul_lt_top (ENNReal.pow_lt_top ENNReal.coe_lt_top) this

Premises used: ENNReal.pow_lt_top, ENNReal.mul_lt_top, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 ⋯
suffices :
  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∞)

Tactic:
suffices μH[finrank ℝ E] (e '' K) < ⊤ by
      rw [← e.symm_image_image K]
      apply lt_of_le_of_lt <| e.symm.lipschitz.hausdorffMeasure_image_le (by simp) (e '' K)
      rw [ENNReal.rpow_natCast]
      exact ENNReal.mul_lt_top (ENNReal.pow_lt_top ENNReal.coe_lt_top) this
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 ⋯
a : μH[(↑(finrank ℝ E) : ℝ)]
| ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
    ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 ⋯
a : (↑(finrank ℝ E) : ℝ)
| μH[(↑(finrank ℝ E) : ℝ)]

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 ⋯
a : (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)
| (↑(finrank ℝ E) : ℝ)

Tactic:
rw [← Fintype.card_fin (finrank ℝ E)]

Premises used: Real, Fintype.card_fin, Module.finrank
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 ⋯
a : (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)
| ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
    ℝ≥0∞)

Tactic:
congr; congr; rw [← Fintype.card_fin (finrank ℝ E)]

Premises used: Real, Fintype.card_fin, Module.finrank
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 ⋯
conv_lhs :
  LT.lt (α := ℝ≥0∞)
    ((μH[(↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
conv_lhs => congr; congr; rw [← Fintype.card_fin (finrank ℝ E)]

Premises used: Real, Fintype.card_fin, Module.finrank
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 ⋯
rw :
  LT.lt (α := ℝ≥0∞)
    ((volume : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μH[(↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [hausdorffMeasure_pi_real]

Premises used: MeasureTheory.hausdorffMeasure_pi_real
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 ⋯
⊢ LT.lt (α := ℝ≥0∞)
    ((volume : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
(hK.image e.continuous).measure_lt_top

Premises used: IsCompact.measure_lt_top, ContinuousLinearEquiv.continuous, IsCompact.image
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 ⋯
⊢ LT.lt (α := ℝ≥0∞)
    ((volume : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact (hK.image e.continuous).measure_lt_top

Premises used: IsCompact.measure_lt_top, ContinuousLinearEquiv.continuous, IsCompact.image
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
⊢ finrank ℝ E = finrank ℝ (Fin (finrank ℝ E) → ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
      ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
suffices :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
      ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (((μH[(↑(finrank ℝ E) : ℝ)] : Measure E) : (a : Set E) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
suffices 0 < μH[finrank ℝ E] (e '' U) from
      (ENNReal.mul_pos_iff.mp (lt_of_lt_of_le this <|
        e.lipschitz.hausdorffMeasure_image_le (by simp) _)).2.ne'
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
a : μH[(↑(finrank ℝ E) : ℝ)]
| ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
    ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
a : (↑(finrank ℝ E) : ℝ)
| μH[(↑(finrank ℝ E) : ℝ)]

Tactic:
congr