awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : (x : X) → ℝ≥0
t : (x : X) → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : u.Countable
huU : ⋃ i ∈ u, s ∩ t i = s
⊢ ⨆ i ∈ u, dimH (f '' (s ∩ t i)) ≤ (⨆ i ∈ u, dimH (s ∩ t i)) / (↑r : ℝ≥0∞)
have simp : LE.le (α := ℝ≥0∞) (⨆ i ∈ u, dimH (f '' (s ∩ t i))) (⨆ i ∈ u, dimH (s ∩ t i) / (↑r : ℝ≥0∞))
Tactic: simp only [ENNReal.iSup_div]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ (C : ℝ≥0), ∃ s ∈ 𝓝 x, HolderOnWith C r f s
⊢ dimH (range f) ≤ dimH.{u_2} (X := X) univ / (↑r : ℝ≥0∞)
have rw : dimH (f '' univ) ≤ dimH.{u_2} (X := X) univ / (↑r : ℝ≥0∞)
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ (C : ℝ≥0), ∃ s ∈ 𝓝 x, HolderOnWith C r f s
⊢ dimH (f '' univ) ≤ dimH.{u_2} (X := X) univ / (↑r : ℝ≥0∞)
have refine : ∀ (x : X), Membership.mem (γ := Set X) univ x → ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[univ] x, HolderOnWith C r f t
Tactic: refine dimH_image_le_of_locally_holder_on hr fun x _ => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
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
⊢ dimH (f '' s) ≤ dimH s
have this : ∀ 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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 (range f) ≤ dimH.{u_2} (X := X) univ
have rw : dimH (f '' univ) ≤ dimH.{u_2} (X := X) univ
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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
have refine : ∀ (x : X), Membership.mem (γ := Set X) univ x → ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[univ] x, LipschitzOnWith C f t
Tactic: refine dimH_image_le_of_locally_lipschitzOn fun x _ => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
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
⊢ dimH (f ⁻¹' s) ≤ dimH s
have this : let this := borel X;
BorelSpace X
Tactic: borelize X Y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
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
⊢ dimH (f ⁻¹' s) ≤ dimH s
have this₁ : let this := borel Y;
BorelSpace Y
Tactic: borelize X Y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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
have 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∞)
Tactic: refine dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have 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∞)
Tactic: have := hf.hausdorffMeasure_preimage_le d.coe_nonneg s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have this₁ : HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ (↑d : ℝ)) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) = ∞
Tactic: rw [hd, top_le_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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∞) = ∞
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have 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∞) ≠ ∞
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
e : X ≃ᵢ Y
s : Set Y
⊢ dimH.{u_2} (X := X) ((⇑e : (a : X) → Y) ⁻¹' s) = dimH s
have rw : dimH.{u_2} (X := X) ((⇑e.symm : (a : Y) → X) '' s) = dimH s
Tactic: rw [← e.image_symm, e.symm.dimH_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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
⊢ dimH.{u_2} (X := X) ((⇑e : (a : X) → Y) ⁻¹' s) = dimH s
have rw₁ : dimH s = dimH s
Tactic: rw [← e.image_symm, e.symm.dimH_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
e : X ≃ᵢ Y
⊢ dimH.{u_2} (X := X) univ = dimH.{u_3} (X := Y) univ
have rw : dimH.{u_2} (X := X) univ = dimH.{u_2} (X := X) (preimage.{u_2, u_3} (β := Y) (⇑e : (a : X) → Y) univ)
Tactic: rw [← e.dimH_preimage univ, preimage_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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)
⊢ dimH.{u_2} (X := X) univ = dimH.{u_3} (X := Y) univ
have rw₁ : dimH.{u_2} (X := X) univ = dimH.{u_2} (X := X) univ
Tactic: rw [← e.dimH_preimage univ, preimage_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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
⊢ dimH.{u_5} (X := E) ((⇑e : (a : E) → F) ⁻¹' s) = dimH s
have rw : dimH.{u_5} (X := E) ((⇑e.symm : (a : F) → E) '' s) = dimH s
Tactic: rw [← e.image_symm_eq_preimage, e.symm.dimH_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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
⊢ dimH.{u_5} (X := E) ((⇑e : (a : E) → F) ⁻¹' s) = dimH s
have rw₁ : dimH s = dimH s
Tactic: rw [← e.image_symm_eq_preimage, e.symm.dimH_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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
⊢ dimH.{u_5} (X := E) univ = dimH.{u_6} (X := F) univ
have rw : dimH.{u_5} (X := E) univ = dimH.{u_5} (X := E) (preimage.{u_5, u_6} (β := F) (⇑e : (a : E) → F) univ)
Tactic: rw [← e.dimH_preimage, preimage_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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)
⊢ dimH.{u_5} (X := E) univ = dimH.{u_6} (X := F) univ
have rw₁ : dimH.{u_5} (X := E) univ = dimH.{u_5} (X := E) univ
Tactic: rw [← e.dimH_preimage, preimage_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
⊢ dimH (Metric.ball x r) = (↑(Fintype.card ι) : ℝ≥0∞)
have inl : IsEmpty ι → dimH (Metric.ball x r) = (↑(Fintype.card ι) : ℝ≥0∞)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
inl : IsEmpty ι → dimH (Metric.ball x r) = (↑(Fintype.card ι) : ℝ≥0∞)
⊢ dimH (Metric.ball x r) = (↑(Fintype.card ι) : ℝ≥0∞)
have inr : Nonempty ι → dimH (Metric.ball x r) = (↑(Fintype.card ι) : ℝ≥0∞)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : IsEmpty ι
⊢ dimH (Metric.ball x r) = (↑(Fintype.card ι) : ℝ≥0∞)
have inl : (Metric.ball x r).Subsingleton
Tactic: rwa [dimH_subsingleton, eq_comm, Nat.cast_eq_zero, Fintype.card_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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 ι)
have rw : ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
Tactic: rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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 ι)
⊢ ((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
have rw₁ : ENNReal.ofReal ((2 * r) ^ Fintype.card ι) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
Tactic: rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h : Nonempty ι
⊢ dimH (Metric.ball x r) = (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞)
have this : ((μ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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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∞)
have inr : Ne (α := ℝ≥0∞)
  (((μH[(↑(↑(Fintype.card ι) : ℝ≥0) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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∞)
⊢ dimH (Metric.ball x r) = (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞)
have inr₁ : Ne (α := ℝ≥0∞)
  (((μH[(↑(↑(Fintype.card ι) : ℝ≥0) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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 ι)
⊢ Ne (α := ℝ≥0∞)
    (((μH[(↑(↑(Fintype.card ι) : ℝ≥0) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have inr : ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ 0
Tactic: rw [NNReal.coe_natCast, this]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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 ι)
⊢ Ne (α := ℝ≥0∞)
    (((μH[(↑(↑(Fintype.card ι) : ℝ≥0) : ℝ)] : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have inr : ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ ∞
Tactic: rw [NNReal.coe_natCast, this]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
n : ℕ
x : Fin n → ℝ
r : ℝ
hr : 0 < r
⊢ dimH (Metric.ball x r) = (↑n : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (↑(Fintype.card (Fin n)) : ℝ≥0∞) (↑n : ℝ≥0∞)
Tactic: rw [dimH_ball_pi x hr, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
n : ℕ
x : Fin n → ℝ
r : ℝ
hr : 0 < r
rw : Eq (α := ℝ≥0∞) (↑(Fintype.card (Fin n)) : ℝ≥0∞) (↑n : ℝ≥0∞)
⊢ dimH (Metric.ball x r) = (↑n : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (↑n : ℝ≥0∞)
Tactic: rw [dimH_ball_pi x hr, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
n : ℕ
⊢ dimH (X := Fin n → ℝ) univ = (↑n : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (↑(Fintype.card (Fin n)) : ℝ≥0∞) (↑n : ℝ≥0∞)
Tactic: rw [dimH_univ_pi, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
n : ℕ
rw : Eq (α := ℝ≥0∞) (↑(Fintype.card (Fin n)) : ℝ≥0∞) (↑n : ℝ≥0∞)
⊢ dimH (X := Fin n → ℝ) univ = (↑n : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (↑n : ℝ≥0∞)
Tactic: rw [dimH_univ_pi, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ dimH s = (↑(finrank ℝ E) : ℝ≥0∞)
have have : ∀ (e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ), dimH s = (↑(finrank ℝ E) : ℝ≥0∞)
Tactic: have e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ :=
    ContinuousLinearEquiv.ofFinrankEq (Module.finrank_fin_fun ℝ).symm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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 s = (↑(finrank ℝ E) : ℝ≥0∞)
have rw : dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s) = (↑(finrank ℝ E) : ℝ≥0∞)
Tactic: rw [← e.dimH_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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∞)
have refine_1 : dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s) ≤ (↑(finrank ℝ E) : ℝ≥0∞)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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∞)
⊢ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s) = (↑(finrank ℝ E) : ℝ≥0∞)
have refine_2 : (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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) → ℝ
⊢ Membership.mem (γ := Filter (Fin (finrank ℝ E) → ℝ))
    (𝓝 ((e : (a : E) → Fin (finrank ℝ E) → ℝ) x) : Filter (Fin (finrank ℝ E) → ℝ))
    ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
have rw : Membership.mem (γ := Filter (Fin (finrank ℝ E) → ℝ)) (Filter.map (⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) (𝓝 x))
  ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
Tactic: rw [← e.map_nhds_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
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) → ℝ
⊢ (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
have this : 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: have : e '' s ∈ 𝓝 (e x) := by rw [← e.map_nhds_eq]; exact image_mem_map h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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) → ℝ
this :
  Membership.mem (γ := Filter (Fin (finrank ℝ E) → ℝ))
    (𝓝 ((e : (a : E) → Fin (finrank ℝ E) → ℝ) x) : Filter (Fin (finrank ℝ E) → ℝ))
    ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
⊢ (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
have refine_2 : ∀ (r : ℝ) (hr0 : 0 < r)
  (hr :
    Subset (α := Set (Fin (finrank ℝ E) → ℝ))
      (Metric.ball ((e : (a : E) → Fin (finrank ℝ E) → ℝ) x) r : Set (Fin (finrank ℝ E) → ℝ))
      ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s : Set (Fin (finrank ℝ E) → ℝ))),
  (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
Tactic: rcases Metric.nhds_basis_ball.mem_iff.1 this with ⟨r, hr0, hr⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
⊢ dimH s = (↑(finrank.{0, u_4} ℝ ↥(vectorSpan ℝ s)) : ℝ≥0∞)
have this : Nonempty.{u_4 + 1} (↑s : Type u_4)
Tactic: have := hne.to_subtype
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty.{u_4 + 1} (↑s : Type u_4)
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(AffineSubspace.direction (affineSpan ℝ s)) :=
  AffineIsometryEquiv.constVSub ℝ
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) (hne.some (s := s)) ⋯)
⊢ dimH s = (↑(finrank.{0, u_4} ℝ ↥(vectorSpan ℝ s)) : ℝ≥0∞)
have hs_eq : s =
  image (α := ↥(affineSpan ℝ s))
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x))
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s)
Tactic: have hs_eq : s = (↑) '' ((↑) ⁻¹' s : Set (affineSpan ℝ s)) :=
    (image_preimage_eq_of_subset <| (subset_affineSpan ℝ s).trans Subtype.range_coe.superset).symm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty.{u_4 + 1} (↑s : Type u_4)
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(AffineSubspace.direction (affineSpan ℝ s)) :=
  AffineIsometryEquiv.constVSub ℝ
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) (hne.some (s := s)) ⋯)
hs_eq :
  s =
    image (α := ↥(affineSpan ℝ s))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s)
⊢ dimH s = (↑(finrank.{0, u_4} ℝ ↥(vectorSpan ℝ s)) : ℝ≥0∞)
have rw : Set.Nonempty (α := ↥(AffineSubspace.direction (affineSpan ℝ s)))
  (interior
    (image (α := ↥(affineSpan ℝ s)) (⇑φ : (a : ↥(affineSpan ℝ s)) → ↥(affineSpan ℝ s).direction)
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s)))
Tactic: rw [hs_eq, isometry_subtype_coe.dimH_image, ← φ.isometry.dimH_image,
      Real.dimH_of_nonempty_interior, direction_affineSpan ℝ s, ← hs_eq]