awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
d : ℝ≥0
h :
  ⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞) <
    (↑d : ℝ≥0∞)
d' : ℝ≥0
hsd' :
  ⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞) <
    (↑d' : ℝ≥0∞)
hd'd : (↑d' : ℝ) < (↑d : ℝ)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact (hausdorffMeasure_zero_or_top hd'd s).resolve_right fun h₂ => hsd'.not_ge <|
    le_iSup₂ (α := ℝ≥0∞) d' h₂

Premises used: le_iSup₂, MeasureTheory.Measure.hausdorffMeasure_zero_or_top, Or.resolve_right, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
μ : Measure X
d : ℝ≥0
h : μ ≪ μH[(↑d : ℝ)]
s : Set X
hd : dimH s < (↑d : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
h <| hausdorffMeasure_of_dimH_lt hd

Premises used: hausdorffMeasure_of_dimH_lt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
d : ℝ≥0
h : Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (↑d : ℝ≥0∞) ≤ dimH s

Tactic:
le_of_not_gt <| mt hausdorffMeasure_of_dimH_lt h

Premises used: le_of_not_gt, mt, hausdorffMeasure_of_dimH_lt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ≥0
s : Set X
h : Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ dimH s = (↑d : ℝ≥0∞)

Tactic:
le_antisymm (dimH_le_of_hausdorffMeasure_ne_top h') (le_dimH_of_hausdorffMeasure_ne_zero h)

Premises used: le_dimH_of_hausdorffMeasure_ne_zero, dimH_le_of_hausdorffMeasure_ne_top, le_antisymm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
a :
  dimH s ≤
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
a₁ :
  ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞) ≤
    dimH s
⊢ dimH s =
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
a :
  LE.le (α := ℝ≥0∞)
    (⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞))
    (⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞))
⊢ dimH s ≤
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)

Tactic:
rw [dimH_def]

Premises used: dimH_def
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
a :
  ∀ (i : ℝ≥0) (i_1 : Eq (α := ℝ≥0∞) (((μH[(↑i : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)) (i_2 : ℝ≥0)
    (i_3 : Eq (α := ℝ≥0∞) (((μH[(↑i_2 : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), i_2 ≤ i
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞))
    (⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞))

Tactic:
simp only [le_iInf_iff, iSup_le_iff, ENNReal.coe_le_coe]

Premises used: le_iInf_iff, ENNReal.coe_le_coe, iSup_le_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
i : ℝ≥0
hi : Eq (α := ℝ≥0∞) (((μH[(↑i : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
j : ℝ≥0
hj : Eq (α := ℝ≥0∞) (((μH[(↑j : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : ∀ (hij : i < j), False
⊢ j ≤ i

Tactic:
by_contra! hij
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
i : ℝ≥0
hi : Eq (α := ℝ≥0∞) (((μH[(↑i : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
j : ℝ≥0
hj : Eq (α := ℝ≥0∞) (((μH[(↑j : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hij : i < j
⊢ False

Tactic:
simpa [hi, hj] using hausdorffMeasure_mono hij.le s

Premises used: MeasureTheory.Measure.hausdorffMeasure_mono, LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
a :
  ∀
    (h :
      dimH s <
        ⨅ (d : ℝ≥0),
          ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)),
    False
⊢ ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞) ≤
    dimH s

Tactic:
by_contra! h
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
h :
  dimH s <
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
a :
  ∀ (d' : ℝ≥0) (hdim_lt : dimH s < (↑d' : ℝ≥0∞))
    (hlt :
      (↑d' : ℝ≥0∞) <
        ⨅ (d : ℝ≥0),
          ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)),
    False
⊢ False

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hdim_lt, hlt⟩

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
h :
  dimH s <
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
d' : ℝ≥0
hdim_lt : dimH s < (↑d' : ℝ≥0∞)
hlt :
  (↑d' : ℝ≥0∞) <
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d' : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have h0 : μH[d'] s = 0 := hausdorffMeasure_of_dimH_lt hdim_lt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
h :
  dimH s <
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
d' : ℝ≥0
hdim_lt : dimH s < (↑d' : ℝ≥0∞)
hlt :
  (↑d' : ℝ≥0∞) <
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
h0 : Eq (α := ℝ≥0∞) (((μH[(↑d' : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
hlt.not_ge (iInf₂_le d' h0)

Premises used: iInf₂_le, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
h :
  dimH s <
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
d' : ℝ≥0
hdim_lt : dimH s < (↑d' : ℝ≥0∞)
hlt :
  (↑d' : ℝ≥0∞) <
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
h0 : Eq (α := ℝ≥0∞) (((μH[(↑d' : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
exact hlt.not_ge (iInf₂_le d' h0)

Premises used: iInf₂_le, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s t : Set X
h : s ⊆ t
⊢ let this := borel X;
  BorelSpace X

Tactic:
borelize X
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s t : Set X
h : s ⊆ t
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ dimH s ≤ dimH t

Tactic:
dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top <| top_unique <| hd ▸ measure_mono h

Premises used: le_dimH_of_hausdorffMeasure_eq_top, dimH_le, top_unique
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s t : Set X
h : s ⊆ t
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ dimH s ≤ dimH t

Tactic:
exact dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top <| top_unique <| hd ▸ measure_mono h

Premises used: le_dimH_of_hausdorffMeasure_eq_top, dimH_le, top_unique
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
h : s.Subsingleton
⊢ let this := borel X;
  BorelSpace X

Tactic:
borelize X
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
h : s.Subsingleton
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
rw : dimH s ≤ 0
⊢ dimH s = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
h : s.Subsingleton
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
h₁ : Ne (α := ℝ≥0∞) (((μH[(↑0 : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ dimH s ≤ 0

Tactic:
apply dimH_le_of_hausdorffMeasure_ne_top

Premises used: dimH_le_of_hausdorffMeasure_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
h : s.Subsingleton
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ Ne (α := ℝ≥0∞) (((μH[(↑0 : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
((hausdorffMeasure_le_one_of_subsingleton h le_rfl).trans_lt ENNReal.one_lt_top).ne

Premises used: le_rfl, Set.Mem, ENNReal.one_lt_top, MeasureTheory.Measure.hausdorffMeasure_le_one_of_subsingleton, LE.le.trans_lt, NNReal.toReal, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
h : s.Subsingleton
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ Ne (α := ℝ≥0∞) (((μH[(↑0 : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ((hausdorffMeasure_le_one_of_subsingleton h le_rfl).trans_lt ENNReal.one_lt_top).ne

Premises used: le_rfl, ENNReal.one_lt_top, MeasureTheory.Measure.hausdorffMeasure_le_one_of_subsingleton, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
⊢ dimH.{u_2} (X := X) ∅ = 0

Tactic:
subsingleton_empty.dimH_zero

Premises used: Set.subsingleton_empty, Set.Subsingleton.dimH_zero
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
x : X
⊢ dimH (X := X) {x} = 0

Tactic:
subsingleton_singleton.dimH_zero

Premises used: Set.subsingleton_singleton, Set.Subsingleton.dimH_zero
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
⊢ let this := borel X;
  BorelSpace X

Tactic:
borelize X
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ dimH.{u_2} (X := X) (⋃ (i : ι), s i) = ⨆ (i : ι), dimH (s i)

Tactic:
le_antisymm (dimH_le fun d hd => ?_) (iSup_le fun i => dimH_mono <| subset_iUnion _ _)

Premises used: dimH_le, Set.subset_iUnion, dimH_mono, le_antisymm, iSup_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
refine :
  ∀ (d : ℝ≥0)
    (hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (↑d : ℝ≥0∞) ≤ ⨆ (i : ι), dimH (s i)
⊢ dimH.{u_2} (X := X) (⋃ (i : ι), s i) = ⨆ (i : ι), dimH (s i)

Tactic:
refine le_antisymm (dimH_le fun d hd => ?_) (iSup_le fun i => dimH_mono <| subset_iUnion _ _)

Premises used: dimH_le, Set.subset_iUnion, dimH_mono, le_antisymm, iSup_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
contrapose! :
  ∀ (hd : ⨆ (i : ι), dimH (s i) < (↑d : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑d : ℝ≥0∞) ≤ ⨆ (i : ι), dimH (s i)

Tactic:
contrapose! hd
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
d : ℝ≥0
hd : ⨆ (i : ι), dimH (s i) < (↑d : ℝ≥0∞)
⊢ ∀ (i : ι), Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have : ∀ i, μH[d] (s i) = 0 := fun i =>
    hausdorffMeasure_of_dimH_lt ((le_iSup (fun i => dimH (s i)) i).trans_lt hd)
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
d : ℝ≥0
hd : ⨆ (i : ι), dimH (s i) < (↑d : ℝ≥0∞)
this : ∀ (i : ι), Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Ne (α := ℝ≥0∞) 0 ∞
⊢ Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [measure_iUnion_null this]

Premises used: MeasureTheory.measure_iUnion_null
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
d : ℝ≥0
hd : ⨆ (i : ι), dimH (s i) < (↑d : ℝ≥0∞)
this : ∀ (i : ι), Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) 0 ∞

Tactic:
ENNReal.zero_ne_top

Premises used: ENNReal.zero_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
d : ℝ≥0
hd : ⨆ (i : ι), dimH (s i) < (↑d : ℝ≥0∞)
this : ∀ (i : ι), Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) 0 ∞

Tactic:
exact ENNReal.zero_ne_top

Premises used: ENNReal.zero_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
haveI : ∀ (this : Encodable (↑s : Type u_1)), dimH.{u_2} (X := X) (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)
⊢ dimH.{u_2} (X := X) (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)

Tactic:
haveI := hs.toEncodable
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
this : Encodable (↑s : Type u_1)
rw : dimH.{u_2} (X := X) (⋃ (x : (↑s : Type u_1)), t (↑x : ι)) = ⨆ i ∈ s, dimH (t i)
rw₁ : Eq (α := ℝ≥0∞) (⨆ (i : (↑s : Type u_1)), dimH (t (↑i : ι))) (⨆ i ∈ s, dimH (t i))
rw₂ rw₃ : Eq (α := ℝ≥0∞) (⨆ (i : (↑s : Type u_1)), dimH (t (↑i : ι))) (⨆ (i : (↑s : Type u_1)), dimH (t (↑i : ι)))
⊢ dimH.{u_2} (X := X) (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)

Tactic:
rw [biUnion_eq_iUnion, dimH_iUnion, ← iSup_subtype'']

Premises used: iSup_subtype'', Set.biUnion_eq_iUnion, dimH_iUnion
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
S : Set (Set X)
hS : S.Countable
rw : dimH.{u_2} (X := X) (⋃ i ∈ S, i) = ⨆ s ∈ S, dimH s
rw₁ rw₂ : Eq (α := ℝ≥0∞) (⨆ i ∈ S, dimH i) (⨆ s ∈ S, dimH s)
⊢ dimH (⋃₀ S) = ⨆ s ∈ S, dimH s

Tactic:
rw [sUnion_eq_biUnion, dimH_bUnion hS]

Premises used: Set.sUnion_eq_biUnion, dimH_bUnion
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s t : Set X
rw : dimH.{u_2} (X := X) (⋃ (b : Bool), bif b then s else t) = max (dimH s) (dimH t)
rw₁ : ⨆ (i : Bool), dimH (bif i then s else t) = max (dimH s) (dimH t)
rw₂ : max (dimH (bif true then s else t)) (dimH (bif false then s else t)) = max (dimH s) (dimH t)
rw₃ : max (dimH s) (dimH (bif false then s else t)) = max (dimH s) (dimH t)
rw₄ rw₅ : max (dimH s) (dimH t) = max (dimH s) (dimH t)
⊢ dimH (s ∪ t) = max (dimH s) (dimH t)

Tactic:
rw [union_eq_iUnion, dimH_iUnion, iSup_bool_eq, cond, cond]

Premises used: cond, iSup_bool_eq, dimH_iUnion, Set.union_eq_iUnion
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
hs : s.Countable
⊢ dimH.{u_2} (X := X) (⋃ x ∈ s, {x}) = 0

Tactic:
simp only [dimH_bUnion hs, dimH_singleton, ENNReal.iSup_zero]

Premises used: dimH_bUnion, ENNReal.iSup_zero, dimH_singleton
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
hs : s.Finite
⊢ dimH s = 0

Tactic:
hs.countable.dimH_zero

Premises used: Set.Countable.dimH_zero, Set.Finite.countable
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s : Finset X
⊢ dimH (↑s : Set X) = 0

Tactic:
s.finite_toSet.dimH_zero

Premises used: Finset.finite_toSet, Set.Finite.dimH_zero
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : r < dimH s
contrapose! : ∀ (h : ∀ (x : X) (_ : x ∈ s), ∃ t ∈ 𝓝[s] x, dimH t ≤ r), dimH s ≤ r
⊢ ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t

Tactic:
contrapose! h
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : ∀ (x : X) (_ : x ∈ s), ∃ t ∈ 𝓝[s] x, dimH t ≤ r
choose! :
  ∀ (t : (x : X) → Set X) (htx : ∀ (x : X) (_ : x ∈ s), t x ∈ 𝓝[s] x) (htr : ∀ (x : X) (_ : x ∈ s), dimH (t x) ≤ r),
    dimH s ≤ r
⊢ dimH s ≤ r

Tactic:
choose! t htx htr using h
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : (x : X) → Set X
htx : ∀ (x : X) (_ : x ∈ s), t x ∈ 𝓝[s] x
htr : ∀ (x : X) (_ : x ∈ s), dimH (t x) ≤ r
rcases : ∀ (S : Set X) (hSs : S ⊆ s) (hSc : S.Countable) (hSU : s ⊆ ⋃ x ∈ S, t x), dimH s ≤ r
⊢ dimH s ≤ r

Tactic:
rcases countable_cover_nhdsWithin htx with ⟨S, hSs, hSc, hSU⟩

Premises used: TopologicalSpace.countable_cover_nhdsWithin
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : (x : X) → Set X
htx : ∀ (x : X) (_ : x ∈ s), t x ∈ 𝓝[s] x
htr : ∀ (x : X) (_ : x ∈ s), dimH (t x) ≤ r
S : Set X
hSs : S ⊆ s
hSc : S.Countable
hSU : s ⊆ ⋃ x ∈ S, t x
⊢ dimH s ≤ dimH.{u_2} (X := X) (⋃ x ∈ S, t x)

Tactic:
dimH_mono hSU

Premises used: dimH_mono
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : (x : X) → Set X
htx : ∀ (x : X) (_ : x ∈ s), t x ∈ 𝓝[s] x
htr : ∀ (x : X) (_ : x ∈ s), dimH (t x) ≤ r
S : Set X
hSs : S ⊆ s
hSc : S.Countable
hSU : s ⊆ ⋃ x ∈ S, t x
⊢ dimH.{u_2} (X := X) (⋃ x ∈ S, t x) = ⨆ x ∈ S, dimH (t x)

Tactic:
dimH_bUnion hSc _

Premises used: dimH_bUnion
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : (x : X) → Set X
htx : ∀ (x : X) (_ : x ∈ s), t x ∈ 𝓝[s] x
htr : ∀ (x : X) (_ : x ∈ s), dimH (t x) ≤ r
S : Set X
hSs : S ⊆ s
hSc : S.Countable
hSU : s ⊆ ⋃ x ∈ S, t x
⊢ ⨆ x ∈ S, dimH (t x) ≤ r

Tactic:
iSup₂_le fun x hx => htr x <| hSs hx

Premises used: iSup₂_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : (x : X) → Set X
htx : ∀ (x : X) (_ : x ∈ s), t x ∈ 𝓝[s] x
htr : ∀ (x : X) (_ : x ∈ s), dimH (t x) ≤ r
S : Set X
hSs : S ⊆ s
hSc : S.Countable
hSU : s ⊆ ⋃ x ∈ S, t x
⊢ dimH s ≤ r

Tactic:
calc
    dimH s ≤ dimH (⋃ x ∈ S, t x) := dimH_mono hSU
    _ = ⨆ x ∈ S, dimH (t x) := dimH_bUnion hSc _
    _ ≤ r := iSup₂_le fun x hx => htr x <| hSs hx

Premises used: iSup₂_le, dimH_bUnion, dimH_mono, Set.iUnion, dimH
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
⊢ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets = dimH s

Tactic:
le_antisymm (iSup₂_le fun x _ => ?_) ?_

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

Tactic:
refine le_antisymm (iSup₂_le fun x _ => ?_) ?_

Premises used: iSup₂_le, le_antisymm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
x : X
h : x ∈ s
⊢ 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
h : x ∈ s
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
h : x ∈ s
⊢ ∀ᶠ (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
h : x ∈ s
⊢ ∀ᶠ (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
⊢ dimH s ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets

Tactic:
le_of_forall_lt_imp_le_of_dense fun r hr => ?_

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

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_

Premises used: le_of_forall_lt_imp_le_of_dense