awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
s : Set X
h : LipschitzOnWith K f s
⊢ dimH (f '' s) ≤ dimH s

Tactic:
simpa using h.holderOnWith.dimH_image_le zero_lt_one

Premises used: HolderOnWith.dimH_image_le, zero_lt_one, LipschitzOnWith.holderOnWith
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
h : LipschitzWith K f
s : Set X
⊢ dimH (f '' s) ≤ dimH s

Tactic:
h.lipschitzOnWith.dimH_image_le

Premises used: LipschitzOnWith.dimH_image_le, LipschitzWith.lipschitzOnWith
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
h : LipschitzWith K f
⊢ dimH (range f) ≤ dimH.{u_2} (X := X) univ

Tactic:
@image_univ _ _ f ▸ h.dimH_image_le univ

Premises used: LipschitzWith.dimH_image_le, Set.image_univ, Set.univ, Eq.rec
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
⊢ ∀ x ∈ s, ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t

Tactic:
simpa only [holderOnWith_one] using hf

Premises used: holderOnWith_one
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
⊢ ∀ x ∈ s, ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t

Tactic:
have : ∀ x ∈ s, ∃ C : ℝ≥0, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t := by
    simpa only [holderOnWith_one] using hf
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
this : ∀ x ∈ s, ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t
⊢ dimH (f '' s) ≤ dimH s

Tactic:
simpa only [ENNReal.coe_one, div_one] using dimH_image_le_of_locally_holder_on zero_lt_one this

Premises used: ENNReal.coe_one, zero_lt_one, dimH_image_le_of_locally_holder_on, div_one
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ (C : ℝ≥0), ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
rw : dimH (f '' univ) ≤ dimH.{u_2} (X := X) univ
⊢ dimH (range f) ≤ dimH.{u_2} (X := X) univ

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ (C : ℝ≥0), ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
⊢ dimH (f '' univ) ≤ dimH.{u_2} (X := X) univ

Tactic:
dimH_image_le_of_locally_lipschitzOn fun x _ => ?_

Premises used: dimH_image_le_of_locally_lipschitzOn
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ (C : ℝ≥0), ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
refine : ∀ (x : X), Membership.mem (γ := Set X) univ x → ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[univ] x, LipschitzOnWith C f t
⊢ dimH (f '' univ) ≤ dimH.{u_2} (X := X) univ

Tactic:
refine dimH_image_le_of_locally_lipschitzOn fun x _ => ?_

Premises used: dimH_image_le_of_locally_lipschitzOn
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ (C : ℝ≥0), ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
x : X
h : Membership.mem (γ := Set X) univ x
⊢ ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[univ] x, LipschitzOnWith C f t

Tactic:
simpa only [exists_prop, nhdsWithin_univ] using hf x

Premises used: nhdsWithin_univ, exists_prop
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
⊢ let this := borel X;
  BorelSpace X

Tactic:
borelize X Y
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this :
  let this := borel X;
  BorelSpace X
⊢ let this := borel Y;
  BorelSpace Y

Tactic:
borelize X Y
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
this_2 : MeasurableSpace Y := borel Y
this_3 : BorelSpace Y
⊢ dimH (f ⁻¹' s) ≤ dimH s

Tactic:
dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top ?_

Premises used: le_dimH_of_hausdorffMeasure_eq_top, dimH_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
this_2 : MeasurableSpace Y := borel Y
this_3 : BorelSpace Y
refine :
  ∀ (d : ℝ≥0) (hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ dimH (f ⁻¹' s) ≤ dimH s

Tactic:
refine dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top ?_

Premises used: le_dimH_of_hausdorffMeasure_eq_top, dimH_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
this_2 : MeasurableSpace Y := borel Y
this_3 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ (↑d : ℝ)) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
have := hf.hausdorffMeasure_preimage_le d.coe_nonneg s
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
this_3 : MeasurableSpace Y := borel Y
this_4 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ (↑d : ℝ)) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ (↑d : ℝ)) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) = ∞

Tactic:
rw [hd, top_le_iff] at this

Premises used: top_le_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
this_3 : MeasurableSpace Y := borel Y
this_4 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ (↑d : ℝ)) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) = ∞
contrapose! :
  ∀ (this : Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ (↑d : ℝ)) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) ≠ ∞
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
contrapose! this
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
this_3 : MeasurableSpace Y := borel Y
this_4 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑K : ℝ≥0∞) ^ (↑d : ℝ) ≠ ∞

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
this_3 : MeasurableSpace Y := borel Y
this_4 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ (↑d : ℝ)) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) ≠ ∞

Tactic:
exact ENNReal.mul_ne_top (by simp) this

Premises used: ENNReal.mul_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set X
⊢ dimH s ≤ dimH (f '' s)

Tactic:
calc
    dimH s ≤ dimH (f ⁻¹' f '' s) := dimH_mono (subset_preimage_image _ _)
    _ ≤ dimH (f '' s) := hf.dimH_preimage_le _

Premises used: Trans.trans, dimH_mono, AntilipschitzWith.dimH_preimage_le, Set.subset_preimage_image
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
f : X → Y
hf : Isometry f
s : Set X
⊢ dimH (f '' s) = dimH s

Tactic:
le_antisymm (hf.lipschitz.dimH_image_le _) (hf.antilipschitz.le_dimH_image _)

Premises used: LipschitzWith.dimH_image_le, le_antisymm, AntilipschitzWith.le_dimH_image, Isometry.lipschitz, Isometry.antilipschitz
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
e : X ≃ᵢ Y
s : Set X
⊢ dimH.{u_3} (X := Y) ((⇑e : (a : X) → Y) '' s) = dimH s

Tactic:
e.isometry.dimH_image s

Premises used: IsometryEquiv.isometry, Isometry.dimH_image
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
e : X ≃ᵢ Y
s : Set Y
rw : dimH.{u_2} (X := X) ((⇑e.symm : (a : Y) → X) '' s) = dimH s
rw₁ rw₂ : dimH s = dimH s
⊢ dimH.{u_2} (X := X) ((⇑e : (a : X) → Y) ⁻¹' s) = dimH s

Tactic:
rw [← e.image_symm, e.symm.dimH_image]

Premises used: IsometryEquiv.symm, IsometryEquiv.dimH_image, IsometryEquiv.image_symm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
e : X ≃ᵢ Y
rw : dimH.{u_2} (X := X) univ = dimH.{u_2} (X := X) (preimage.{u_2, u_3} (β := Y) (⇑e : (a : X) → Y) univ)
rw₁ rw₂ : dimH.{u_2} (X := X) univ = dimH.{u_2} (X := X) univ
⊢ dimH.{u_2} (X := X) univ = dimH.{u_3} (X := Y) univ

Tactic:
rw [← e.dimH_preimage univ, preimage_univ]

Premises used: IsometryEquiv.dimH_preimage, Set.univ, Set.preimage_univ
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set E
⊢ dimH s ≤ dimH.{u_6} (X := F) ((⇑e : (a : E) → F) '' s)

Tactic:
simpa only [e.symm_image_image] using e.symm.lipschitz.dimH_image_le (e '' s)

Premises used: LipschitzWith.dimH_image_le, ContinuousLinearEquiv.symm, ContinuousLinearEquiv.lipschitz, ContinuousLinearEquiv.symm_image_image, Set.image, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set F
rw : dimH.{u_5} (X := E) ((⇑e.symm : (a : F) → E) '' s) = dimH s
rw₁ rw₂ : dimH s = dimH s
⊢ dimH.{u_5} (X := E) ((⇑e : (a : E) → F) ⁻¹' s) = dimH s

Tactic:
rw [← e.image_symm_eq_preimage, e.symm.dimH_image]

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.dimH_image, ContinuousLinearEquiv.image_symm_eq_preimage
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
rw : dimH.{u_5} (X := E) univ = dimH.{u_5} (X := E) (preimage.{u_5, u_6} (β := F) (⇑e : (a : E) → F) univ)
rw₁ rw₂ : dimH.{u_5} (X := E) univ = dimH.{u_5} (X := E) univ
⊢ dimH.{u_5} (X := E) univ = dimH.{u_6} (X := F) univ

Tactic:
rw [← e.dimH_preimage, preimage_univ]

Premises used: Set.preimage_univ, ContinuousLinearEquiv.dimH_preimage
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
inl : IsEmpty ι → dimH (Metric.ball x r) = (↑(Fintype.card ι) : ℝ≥0∞)
inr : Nonempty ι → dimH (Metric.ball x r) = (↑(Fintype.card ι) : ℝ≥0∞)
⊢ dimH (Metric.ball x r) = (↑(Fintype.card ι) : ℝ≥0∞)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : IsEmpty ι
inl : (Metric.ball x r).Subsingleton
⊢ dimH (Metric.ball x r) = (↑(Fintype.card ι) : ℝ≥0∞)

Tactic:
rwa [dimH_subsingleton, eq_comm, Nat.cast_eq_zero, Fintype.card_eq_zero_iff]

Premises used: eq_comm, Nat.cast_eq_zero, Fintype.card_eq_zero_iff, dimH_subsingleton
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : IsEmpty ι
⊢ (Metric.ball x r).Subsingleton

Tactic:
fun x _ y _ => Subsingleton.elim x y

Premises used: Set.Subsingleton, Subsingleton.elim
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : IsEmpty ι
⊢ (Metric.ball x r).Subsingleton

Tactic:
exact fun x _ y _ => Subsingleton.elim x y

Premises used: Subsingleton.elim
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : Nonempty ι
rw :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
rw₁ rw₂ : ENNReal.ofReal ((2 * r) ^ Fintype.card ι) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ ((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr]

Premises used: Real.volume_pi_ball, MeasureTheory.hausdorffMeasure_pi_real
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : Nonempty ι
⊢ ((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
have : μH[Fintype.card ι] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) := by
      rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr]
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : Nonempty ι
this :
  ((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ dimH (Metric.ball x r) = (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞)

Tactic:
dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_

Premises used: dimH_of_hausdorffMeasure_ne_zero_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : Nonempty ι
this :
  ((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
inr :
  Ne (α := ℝ≥0∞)
    (((μH[(↑(↑(Fintype.card ι) : ℝ≥0) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞)
    (0 : ℝ≥0∞)
inr₁ :
  Ne (α := ℝ≥0∞)
    (((μH[(↑(↑(Fintype.card ι) : ℝ≥0) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ dimH (Metric.ball x r) = (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞)

Tactic:
refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_

Premises used: dimH_of_hausdorffMeasure_ne_zero_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : Nonempty ι
this :
  ((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
inr : ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ 0
⊢ Ne (α := ℝ≥0∞)
    (((μH[(↑(↑(Fintype.card ι) : ℝ≥0) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [NNReal.coe_natCast, this]

Premises used: NNReal.coe_natCast
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : Nonempty ι
this :
  ((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
inr : ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ ∞
⊢ Ne (α := ℝ≥0∞)
    (((μH[(↑(↑(Fintype.card ι) : ℝ≥0) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [NNReal.coe_natCast, this]

Premises used: NNReal.coe_natCast
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : Nonempty ι
this :
  ((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ 0

Tactic:
simp [pow_pos (mul_pos (zero_lt_two' ℝ) hr)]

Premises used: pow_pos, Real, mul_pos, zero_lt_two'
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : Nonempty ι
this :
  ((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ ∞

Tactic:
ENNReal.ofReal_ne_top

Premises used: ENNReal.ofReal_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : Nonempty ι
this :
  ((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ ∞

Tactic:
exact ENNReal.ofReal_ne_top

Premises used: ENNReal.ofReal_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
n : ℕ
x : Fin n → ℝ
r : ℝ
hr : 0 < r
rw : Eq (α := ℝ≥0∞) (↑(Fintype.card (Fin n)) : ℝ≥0∞) (↑n : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (↑n : ℝ≥0∞)
⊢ dimH (Metric.ball x r) = (↑n : ℝ≥0∞)

Tactic:
rw [dimH_ball_pi x hr, Fintype.card_fin]

Premises used: Fintype.card_fin, Real.dimH_ball_pi
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_5
inst : Fintype ι
⊢ dimH.{u_5} (X := ι → ℝ) univ = (↑(Fintype.card ι) : ℝ≥0∞)

Tactic:
simp only [← Metric.iUnion_ball_nat_succ (0 : ι → ℝ), dimH_iUnion,
    dimH_ball_pi _ (Nat.cast_add_one_pos _), iSup_const]

Premises used: Metric.iUnion_ball_nat_succ, Nat.cast_add_one_pos, Real.dimH_ball_pi, dimH_iUnion, iSup_const, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
n : ℕ
rw : Eq (α := ℝ≥0∞) (↑(Fintype.card (Fin n)) : ℝ≥0∞) (↑n : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (↑n : ℝ≥0∞)
⊢ dimH (X := Fin n → ℝ) univ = (↑n : ℝ≥0∞)

Tactic:
rw [dimH_univ_pi, Fintype.card_fin]

Premises used: Fintype.card_fin, Real.dimH_univ_pi
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
have : ∀ (e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ), dimH s = (↑(finrank ℝ E) : ℝ≥0∞)
⊢ dimH s = (↑(finrank ℝ E) : ℝ≥0∞)

Tactic:
have e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ :=
    ContinuousLinearEquiv.ofFinrankEq (Module.finrank_fin_fun ℝ).symm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
rw : dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s) = (↑(finrank ℝ E) : ℝ≥0∞)
⊢ dimH s = (↑(finrank ℝ E) : ℝ≥0∞)

Tactic:
rw [← e.dimH_image]

Premises used: ContinuousLinearEquiv.dimH_image
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s) = (↑(finrank ℝ E) : ℝ≥0∞)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
refine_1 : dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s) ≤ (↑(finrank ℝ E) : ℝ≥0∞)
refine_2 : (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
⊢ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s) = (↑(finrank ℝ E) : ℝ≥0∞)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s) ≤ (↑(finrank ℝ E) : ℝ≥0∞)

Tactic:
(dimH_mono (subset_univ _)).trans_eq (dimH_univ_pi_fin _)

Premises used: LE.le.trans_eq, Set.subset_univ, Real.dimH_univ_pi_fin, dimH_mono
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s) ≤ (↑(finrank ℝ E) : ℝ≥0∞)

Tactic:
exact (dimH_mono (subset_univ _)).trans_eq (dimH_univ_pi_fin _)

Premises used: LE.le.trans_eq, Set.subset_univ, Real.dimH_univ_pi_fin, dimH_mono
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
rw :
  Membership.mem (γ := Filter (Fin (finrank ℝ E) → ℝ)) (Filter.map (⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) (𝓝 x))
    ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
⊢ Membership.mem (γ := Filter (Fin (finrank ℝ E) → ℝ))
    (𝓝 ((e : (a : E) → Fin (finrank ℝ E) → ℝ) x) : Filter (Fin (finrank ℝ E) → ℝ))
    ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)

Tactic:
rw [← e.map_nhds_eq]

Premises used: ContinuousLinearEquiv.map_nhds_eq