awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
refine_2 : ∀ (x : X) (hxs : x ∈ s) (hxr : ∀ t ∈ 𝓝[s] x, r < dimH t), r ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets
⊢ r ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets

Tactic:
rcases exists_mem_nhdsWithin_lt_dimH_of_lt_dimH hr with ⟨x, hxs, hxr⟩

Premises used: exists_mem_nhdsWithin_lt_dimH_of_lt_dimH
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets

Tactic:
le_iSup₂_of_le x hxs ?_

Premises used: le_iSup₂_of_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
refine_2 : r ≤ limsup dimH (𝓝[s] x).smallSets
⊢ r ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets

Tactic:
refine le_iSup₂_of_le x hxs ?_

Premises used: le_iSup₂_of_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
refine_2 : r ≤ sInf {a : ℝ≥0∞ | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}
⊢ r ≤ limsup dimH (𝓝[s] x).smallSets

Tactic:
rw [limsup_eq]

Premises used: Filter.limsup_eq
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ sInf {a : ℝ≥0∞ | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}

Tactic:
le_sInf fun b hb => ?_

Premises used: le_sInf
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
refine_2 :
  ∀ (b : ℝ≥0∞) (hb : Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a} b),
    r ≤ b
⊢ r ≤ sInf {a : ℝ≥0∞ | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}

Tactic:
refine le_sInf fun b hb => ?_

Premises used: le_sInf
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
b : ℝ≥0∞
hb : Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a} b
refine_2 : ∀ (t : Set X) (htx : t ∈ 𝓝[s] x) (ht : ∀ t_1 ⊆ t, dimH t_1 ≤ b), r ≤ b
⊢ r ≤ b

Tactic:
rcases eventually_smallSets.1 hb with ⟨t, htx, ht⟩

Premises used: Filter.eventually_smallSets, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
b : ℝ≥0∞
hb : Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a} b
t : Set X
htx : t ∈ 𝓝[s] x
ht : ∀ t_1 ⊆ t, dimH t_1 ≤ b
⊢ r ≤ b

Tactic:
(hxr t htx).le.trans (ht t Subset.rfl)

Premises used: LT.lt.le, Set.Subset.rfl, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
b : ℝ≥0∞
hb : Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a} b
t : Set X
htx : t ∈ 𝓝[s] x
ht : ∀ t_1 ⊆ t, dimH t_1 ≤ b
⊢ r ≤ b

Tactic:
exact (hxr t htx).le.trans (ht t Subset.rfl)

Premises used: LT.lt.le, Set.Subset.rfl, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
⊢ ⨆ (x : X), limsup dimH (𝓝[s] x).smallSets = dimH s

Tactic:
le_antisymm (iSup_le fun x => ?_) ?_

Premises used: le_antisymm, iSup_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
refine_1 : ∀ (x : X), limsup dimH (𝓝[s] x).smallSets ≤ dimH s
refine_2 : dimH s ≤ ⨆ (x : X), limsup dimH (𝓝[s] x).smallSets
⊢ ⨆ (x : X), limsup dimH (𝓝[s] x).smallSets = dimH s

Tactic:
refine le_antisymm (iSup_le fun x => ?_) ?_

Premises used: le_antisymm, iSup_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
x : X
⊢ limsup dimH (𝓝[s] x).smallSets ≤ dimH s

Tactic:
limsup_le_of_le isCobounded_le_of_bot ?_

Premises used: Filter.limsup_le_of_le, Filter.isCobounded_le_of_bot
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
x : X
refine_1 : ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ dimH s
⊢ limsup dimH (𝓝[s] x).smallSets ≤ dimH s

Tactic:
refine limsup_le_of_le isCobounded_le_of_bot ?_

Premises used: Filter.limsup_le_of_le, Filter.isCobounded_le_of_bot
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
x : X
⊢ ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ dimH s

Tactic:
eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩

Premises used: Iff.mpr, Filter.eventually_smallSets, dimH_mono, self_mem_nhdsWithin, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
x : X
⊢ ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ dimH s

Tactic:
exact eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩

Premises used: Iff.mpr, Filter.eventually_smallSets, dimH_mono, self_mem_nhdsWithin, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
refine_2 : LE.le (α := ℝ≥0∞) (⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets) (⨆ (x : X), limsup dimH (𝓝[s] x).smallSets)
⊢ dimH s ≤ ⨆ (x : X), limsup dimH (𝓝[s] x).smallSets

Tactic:
rw [← bsupr_limsup_dimH]

Premises used: bsupr_limsup_dimH
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
⊢ LE.le (α := ℝ≥0∞) (⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets) (⨆ (x : X), limsup dimH (𝓝[s] x).smallSets)

Tactic:
iSup₂_le_iSup _ _

Premises used: iSup₂_le_iSup
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
⊢ LE.le (α := ℝ≥0∞) (⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets) (⨆ (x : X), limsup dimH (𝓝[s] x).smallSets)

Tactic:
exact iSup₂_le_iSup _ _

Premises used: iSup₂_le_iSup
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
⊢ 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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
this_2 : MeasurableSpace Y := borel Y
this_3 : BorelSpace Y
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)

Tactic:
dimH_le fun d hd => ?_

Premises used: dimH_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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 Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (↑d : ℝ≥0∞) ≤ dimH s / (↑r : ℝ≥0∞)
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)

Tactic:
refine dimH_le fun d hd => ?_

Premises used: dimH_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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 Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (↑d : ℝ))
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
have := h.hausdorffMeasure_image_le hr d.coe_nonneg
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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 Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (↑d : ℝ))
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞

Tactic:
rw [hd, ← ENNReal.coe_rpow_of_nonneg _ d.coe_nonneg, top_le_iff] at this

Premises used: ENNReal.coe_rpow_of_nonneg, NNReal.coe_nonneg, top_le_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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 Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
contrapose :
  ∀ (this : ¬Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ¬HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
          (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
        ∞
⊢ Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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 Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this : ¬Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ¬HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
        (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
      ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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 Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
⊢ Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have Hrd : μH[(r * d : ℝ≥0)] s = ⊤ := by
    contrapose this
    finiteness
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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 Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
Hrd : Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : (↑(r * d) : ℝ≥0∞) ≤ dimH s
h0 : (↑r : ℝ≥0∞) ≠ 0 ∨ dimH s ≠ 0
ht : (↑r : ℝ≥0∞) ≠ ∞ ∨ dimH s ≠ ∞
⊢ (↑d : ℝ≥0∞) ≤ dimH s / (↑r : ℝ≥0∞)

Tactic:
rw [ENNReal.le_div_iff_mul_le, mul_comm, ← ENNReal.coe_mul]

Premises used: ENNReal.le_div_iff_mul_le, ENNReal.coe_mul, mul_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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 Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
Hrd : Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑(r * d) : ℝ≥0∞) ≤ dimH s

Tactic:
le_dimH_of_hausdorffMeasure_eq_top Hrd

Premises used: le_dimH_of_hausdorffMeasure_eq_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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 Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
Hrd : Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ≠ 0 ∨ dimH s ≠ 0

Tactic:
Or.inl (mt ENNReal.coe_eq_zero.1 hr.ne')

Premises used: mt, ENNReal.coe_eq_zero, LT.lt.ne', Iff.mp, Or.inl
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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 Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
Hrd : Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ≠ ∞ ∨ dimH s ≠ ∞

Tactic:
Or.inl ENNReal.coe_ne_top

Premises used: Or.inl, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
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 Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
Hrd : Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑(r * d) : ℝ≥0∞) ≤ dimH s

Tactic:
exacts [le_dimH_of_hausdorffMeasure_eq_top Hrd, Or.inl (mt ENNReal.coe_eq_zero.1 hr.ne'),
    Or.inl ENNReal.coe_ne_top]

Premises used: le_dimH_of_hausdorffMeasure_eq_top, mt, ENNReal.coe_eq_zero, LT.lt.ne', Iff.mp, Or.inl, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
h : HolderWith C r f
hr : 0 < r
s : Set X
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)

Tactic:
(h.holderOnWith s).dimH_image_le hr

Premises used: HolderOnWith.dimH_image_le, HolderWith.holderOnWith
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
h : HolderWith C r f
hr : 0 < r
⊢ dimH (range f) ≤ dimH.{u_2} (X := X) univ / (↑r : ℝ≥0∞)

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

Premises used: Set.image_univ, Set.univ, Eq.rec, HolderWith.dimH_image_le
-- 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
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
hf : ∀ x ∈ s, ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[s] x, HolderOnWith C r f t
choose! :
  ∀ (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)), dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)

Tactic:
choose! C t htn hC 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
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)
rcases : ∀ (u : Set X) (hus : u ⊆ s) (huc : u.Countable) (huU : s ⊆ ⋃ x ∈ u, t x), dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)

Tactic:
rcases countable_cover_nhdsWithin htn with ⟨u, hus, huc, huU⟩

Premises used: TopologicalSpace.countable_cover_nhdsWithin
-- 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
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 : s ⊆ ⋃ x ∈ u, t x
⊢ s ∩ ⋃ x ∈ u, t x = s

Tactic:
replace huU := inter_eq_self_of_subset_left huU
-- 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
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 : s ∩ ⋃ x ∈ u, t x = s
⊢ ⋃ i ∈ u, s ∩ t i = s

Tactic:
rw [inter_iUnion₂] at huU

Premises used: Set.inter_iUnion₂
-- 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
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
rw : ⨆ i ∈ u, dimH (f '' (s ∩ t i)) ≤ (⨆ i ∈ u, dimH (s ∩ t i)) / (↑r : ℝ≥0∞)
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)

Tactic:
rw [← huU, image_iUnion₂, dimH_bUnion huc, dimH_bUnion huc]

Premises used: Set.image_iUnion₂, dimH_bUnion
-- 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
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
simp : LE.le (α := ℝ≥0∞) (⨆ i ∈ u, dimH (f '' (s ∩ t i))) (⨆ i ∈ u, dimH (s ∩ t i) / (↑r : ℝ≥0∞))
⊢ ⨆ i ∈ u, dimH (f '' (s ∩ t i)) ≤ (⨆ i ∈ u, dimH (s ∩ t i)) / (↑r : ℝ≥0∞)

Tactic:
simp only [ENNReal.iSup_div]

Premises used: ENNReal.iSup_div
-- 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
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
⊢ LE.le (α := ℝ≥0∞) (⨆ i ∈ u, dimH (f '' (s ∩ t i))) (⨆ i ∈ u, dimH (s ∩ t i) / (↑r : ℝ≥0∞))

Tactic:
iSup₂_mono fun x hx => ((hC x (hus hx)).mono inter_subset_right).dimH_image_le hr

Premises used: iSup₂_mono, HolderOnWith.dimH_image_le, Set.inter_subset_right, HolderOnWith.mono
-- 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
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
⊢ LE.le (α := ℝ≥0∞) (⨆ i ∈ u, dimH (f '' (s ∩ t i))) (⨆ i ∈ u, dimH (s ∩ t i) / (↑r : ℝ≥0∞))

Tactic:
exact iSup₂_mono fun x hx => ((hC x (hus hx)).mono inter_subset_right).dimH_image_le hr

Premises used: iSup₂_mono, HolderOnWith.dimH_image_le, Set.inter_subset_right, HolderOnWith.mono
-- 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
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ (C : ℝ≥0), ∃ s ∈ 𝓝 x, HolderOnWith C r f s
rw : dimH (f '' univ) ≤ dimH.{u_2} (X := X) univ / (↑r : ℝ≥0∞)
⊢ dimH (range f) ≤ dimH.{u_2} (X := X) univ / (↑r : ℝ≥0∞)

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
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∞)

Tactic:
dimH_image_le_of_locally_holder_on hr fun x _ => ?_

Premises used: dimH_image_le_of_locally_holder_on
-- 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
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ (C : ℝ≥0), ∃ s ∈ 𝓝 x, HolderOnWith C r f s
refine : ∀ (x : X), Membership.mem (γ := Set X) univ x → ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[univ] x, HolderOnWith C r f t
⊢ dimH (f '' univ) ≤ dimH.{u_2} (X := X) univ / (↑r : ℝ≥0∞)

Tactic:
refine dimH_image_le_of_locally_holder_on hr fun x _ => ?_

Premises used: dimH_image_le_of_locally_holder_on
-- 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
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ (C : ℝ≥0), ∃ s ∈ 𝓝 x, HolderOnWith C r f s
x : X
h : Membership.mem (γ := Set X) univ x
⊢ ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[univ] x, HolderOnWith C r f t

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

Premises used: nhdsWithin_univ, exists_prop