awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
f : Cb X Y
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
z : Y
I1 : ⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
I2 :
  LE.le (α := ℝ) (⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z))
    (⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
I : ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z) < r
z' : X
hr' : (fun (x : X) ↦ ((optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z) : ℝ)) z' < r
⊢ ∃ (y : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) y ∧ dist (optimalGHInjr X Y z) y ≤ r

Tactic:
⟨optimalGHInjl X Y z', mem_range_self _, le_of_lt ?_⟩

Premises used: Set.mem_range_self, le_of_lt, GromovHausdorff.optimalGHInjl, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
f : Cb X Y
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
z : Y
I1 : ⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
I2 :
  LE.le (α := ℝ) (⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z))
    (⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
I : ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z) < r
z' : X
hr' : (fun (x : X) ↦ ((optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z) : ℝ)) z' < r
refine_2 : dist (α := OptimalGHCoupling X Y) (optimalGHInjr X Y z) (optimalGHInjl X Y z') < r
⊢ ∃ (y : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) y ∧ dist (optimalGHInjr X Y z) y ≤ r

Tactic:
refine ⟨optimalGHInjl X Y z', mem_range_self _, le_of_lt ?_⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
f : Cb X Y
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
z : Y
I1 : ⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
I2 :
  LE.le (α := ℝ) (⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z))
    (⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
I : ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z) < r
z' : X
hr' : (fun (x : X) ↦ ((optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z) : ℝ)) z' < r
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  dist (α := OptimalGHCoupling X Y) (optimalGHInjl X Y z') (optimalGHInjr X Y z) < r
⊢ dist (α := OptimalGHCoupling X Y) (optimalGHInjr X Y z) (optimalGHInjl X Y z') < r

Tactic:
rwa [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
⊢ Continuous fromBinary

Tactic:
Continuous.subtype_mk (continuous_ofDigits.comp' (Homeomorph.continuous _)) _

Premises used: Continuous.comp', Homeomorph.continuous, Continuous.subtype_mk, Subtype.coind, tsum, Real.fromBinary, Real.ofDigits, Real.continuous_ofDigits
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
⊢ LT.lt (α := ℕ) 1 2

Tactic:
norm_num
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
refine :
  Set.SurjOn (α := ℕ → Bool) (β := ℕ → Fin 2)
    (⇑(Homeomorph.piCongrRight (Y₁ := fun (a : ℕ) ↦ Bool) (Y₂ := fun (a : ℕ) ↦ Fin 2) fun (x : ℕ) ↦
          Homeomorph.symm finTwoEquiv.toHomeomorphOfDiscrete) :
      (a : ℕ → Bool) → ℕ → Fin 2)
    Set.univ Set.univ
⊢ Function.Surjective fromBinary

Tactic:
refine Subtype.coind_surjective _ ((ofDigits_SurjOn (by norm_num)).comp ?_)

Premises used: Real.ofDigits_SurjOn, Set.SurjOn.comp, Subtype.coind_surjective
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
⊢ Set.SurjOn (α := ℕ → Bool) (β := ℕ → Fin 2)
    (⇑(Homeomorph.piCongrRight (Y₁ := fun (a : ℕ) ↦ Bool) (Y₂ := fun (a : ℕ) ↦ Fin 2) fun (x : ℕ) ↦
          Homeomorph.symm finTwoEquiv.toHomeomorphOfDiscrete) :
      (a : ℕ → Bool) → ℕ → Fin 2)
    Set.univ Set.univ

Tactic:
simp only [Set.surjOn_univ, Homeomorph.surjective _]

Premises used: Set.surjOn_univ, Homeomorph.surjective
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
x : ℕ
⊢ Continuous (Y := ℕ → Bool) fun (a : ℕ → Bool) ↦
    (cantorSpaceHomeomorphNatToCantorSpace : (a : ℕ → Bool) → ℕ → ℕ → Bool) a x

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
⊢ Function.Surjective cantorToHilbert

Tactic:
(Function.Surjective.piMap (fun _ ↦ fromBinary_surjective)).comp
    cantorSpaceHomeomorphNatToCantorSpace.surjective

Premises used: cantorToHilbert, Pi.map, Function.Surjective.piMap, Real.fromBinary_surjective, Function.Surjective.comp, Homeomorph.surjective, cantorSpaceHomeomorphNatToCantorSpace
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Set (ℕ → Bool)
h_closed : IsClosed X
h_nonempty : X.Nonempty
obtain :
  ∀ (f : ((n : ℕ) → Bool) → (n : ℕ) → Bool) (fs : ∀ x ∈ X, f x = x) (frange : Set.range f = X) (hf : LipschitzWith 1 f),
    ∃ (f : (ℕ → Bool) → ℕ → Bool), Continuous f ∧ Set.range f = X
⊢ ∃ (f : (ℕ → Bool) → ℕ → Bool), Continuous f ∧ Set.range f = X

Tactic:
obtain ⟨f, fs, frange, hf⟩ := PiNat.exists_lipschitz_retraction_of_isClosed h_closed h_nonempty

Premises used: PiNat.exists_lipschitz_retraction_of_isClosed
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Set (ℕ → Bool)
h_closed : IsClosed X
h_nonempty : X.Nonempty
f : ((n : ℕ) → Bool) → (n : ℕ) → Bool
fs : ∀ x ∈ X, f x = x
frange : Set.range f = X
hf : LipschitzWith 1 f
⊢ ∃ (f : (ℕ → Bool) → ℕ → Bool), Continuous f ∧ Set.range f = X

Tactic:
⟨f, hf.continuous, frange⟩

Premises used: LipschitzWith.continuous, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Set (ℕ → Bool)
h_closed : IsClosed X
h_nonempty : X.Nonempty
f : ((n : ℕ) → Bool) → (n : ℕ) → Bool
fs : ∀ x ∈ X, f x = x
frange : Set.range f = X
hf : LipschitzWith 1 f
⊢ ∃ (f : (ℕ → Bool) → ℕ → Bool), Continuous f ∧ Set.range f = X

Tactic:
exact ⟨f, hf.continuous, frange⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Type u_1
inst : Nonempty X
inst_1 : MetricSpace X
inst_2 : CompactSpace X
this : TopologicalSpace.SeparableSpace X := ⋯
obtain :
  ∀ (emb : X → ℕ → (↑unitInterval : Type)) (h_emb : Topology.IsEmbedding emb),
    ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f
⊢ ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f

Tactic:
obtain ⟨emb, h_emb⟩ := Metric.PiNatEmbed.exists_embedding_to_hilbert_cube (X := X)

Premises used: Metric.PiNatEmbed.exists_embedding_to_hilbert_cube
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Type u_1
inst : Nonempty X
inst_1 : MetricSpace X
inst_2 : CompactSpace X
this : TopologicalSpace.SeparableSpace X := ⋯
emb : X → ℕ → (↑unitInterval : Type)
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → (↑unitInterval : Type)) := Set.range emb
g : X ≃ₜ (↑KH : Type) := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
⊢ IsClosed KC

Tactic:
have hKC_closed : IsClosed KC :=
    IsClosed.preimage cantorToHilbert_continuous (Topology.IsClosedEmbedding.isClosed_range
    <| Continuous.isClosedEmbedding (Topology.IsEmbedding.continuous h_emb) h_emb.injective)
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Type u_1
inst : Nonempty X
inst_1 : MetricSpace X
inst_2 : CompactSpace X
this : TopologicalSpace.SeparableSpace X := ⋯
emb : X → ℕ → (↑unitInterval : Type)
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → (↑unitInterval : Type)) := Set.range emb
g : X ≃ₜ (↑KH : Type) := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
obtain :
  ∀ (f : (ℕ → Bool) → ℕ → Bool) (hf_continuous : Continuous f) (hf_surjective : Set.range f = KC),
    ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f
⊢ ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f

Tactic:
obtain ⟨f, hf_continuous, hf_surjective⟩ := exists_retractionCantorSet hKC_closed
    <| Set.Nonempty.preimage (Set.range_nonempty emb) cantorToHilbert_surjective

Premises used: exists_retractionCantorSet, cantorToHilbert_surjective, Set.range_nonempty, Set.Nonempty.preimage
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Type u_1
inst : Nonempty X
inst_1 : MetricSpace X
inst_2 : CompactSpace X
this : TopologicalSpace.SeparableSpace X := ⋯
emb : X → ℕ → (↑unitInterval : Type)
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → (↑unitInterval : Type)) := Set.range emb
g : X ≃ₜ (↑KH : Type) := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
⊢ ∀ (a : ℕ → Bool), f a ∈ KC

Tactic:
simp [← hf_surjective]
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Type u_1
inst : Nonempty X
inst_1 : MetricSpace X
inst_2 : CompactSpace X
this : TopologicalSpace.SeparableSpace X := ⋯
emb : X → ℕ → (↑unitInterval : Type)
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → (↑unitInterval : Type)) := Set.range emb
g : X ≃ₜ (↑KH : Type) := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
f' : (ℕ → Bool) → (↑KC : Type) := Subtype.coind f (p := fun (x : ℕ → Bool) ↦ x ∈ KC) ⋯
⊢ Set.SurjOn f Set.univ KC

Tactic:
grind [Set.SurjOn]

Premises used: Set.SurjOn
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Type u_1
inst : Nonempty X
inst_1 : MetricSpace X
inst_2 : CompactSpace X
this : TopologicalSpace.SeparableSpace X := ⋯
emb : X → ℕ → (↑unitInterval : Type)
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → (↑unitInterval : Type)) := Set.range emb
g : X ≃ₜ (↑KH : Type) := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
f' : (ℕ → Bool) → (↑KC : Type) := Subtype.coind f (p := fun (x : ℕ → Bool) ↦ x ∈ KC) ⋯
⊢ Function.Surjective f'

Tactic:
have hf'_surjective : Function.Surjective f' := Subtype.coind_surjective _ (by grind [Set.SurjOn])
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Type u_1
inst : Nonempty X
inst_1 : MetricSpace X
inst_2 : CompactSpace X
this : TopologicalSpace.SeparableSpace X := ⋯
emb : X → ℕ → (↑unitInterval : Type)
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → (↑unitInterval : Type)) := Set.range emb
g : X ≃ₜ (↑KH : Type) := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
f' : (ℕ → Bool) → (↑KC : Type) := Subtype.coind f (p := fun (x : ℕ → Bool) ↦ x ∈ KC) ⋯
hf'_surjective : Function.Surjective f'
h : (↑KC : Type) → (↑KH : Type) := KH.restrictPreimage cantorToHilbert
⊢ Continuous h

Tactic:
have hh_continuous : Continuous h := Continuous.restrictPreimage cantorToHilbert_continuous
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Type u_1
inst : Nonempty X
inst_1 : MetricSpace X
inst_2 : CompactSpace X
this : TopologicalSpace.SeparableSpace X := ⋯
emb : X → ℕ → (↑unitInterval : Type)
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → (↑unitInterval : Type)) := Set.range emb
g : X ≃ₜ (↑KH : Type) := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
f' : (ℕ → Bool) → (↑KC : Type) := Subtype.coind f (p := fun (x : ℕ → Bool) ↦ x ∈ KC) ⋯
hf'_surjective : Function.Surjective f'
h : (↑KC : Type) → (↑KH : Type) := KH.restrictPreimage cantorToHilbert
hh_continuous : Continuous h
⊢ Function.Surjective h

Tactic:
have hh_surjective : Function.Surjective h :=
    Set.restrictPreimage_surjective _ cantorToHilbert_surjective
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Type u_1
inst : Nonempty X
inst_1 : MetricSpace X
inst_2 : CompactSpace X
this : TopologicalSpace.SeparableSpace X := ⋯
emb : X → ℕ → (↑unitInterval : Type)
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → (↑unitInterval : Type)) := Set.range emb
g : X ≃ₜ (↑KH : Type) := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
f' : (ℕ → Bool) → (↑KC : Type) := Subtype.coind f (p := fun (x : ℕ → Bool) ↦ x ∈ KC) ⋯
hf'_surjective : Function.Surjective f'
h : (↑KC : Type) → (↑KH : Type) := KH.restrictPreimage cantorToHilbert
hh_continuous : Continuous h
hh_surjective : Function.Surjective h
⊢ Continuous (Y := X) ((⇑g.symm : (a : (↑KH : Type)) → X) ∘ h ∘ f')

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Goal:
X : Type u_1
inst : Nonempty X
inst_1 : MetricSpace X
inst_2 : CompactSpace X
this : TopologicalSpace.SeparableSpace X := ⋯
emb : X → ℕ → (↑unitInterval : Type)
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → (↑unitInterval : Type)) := Set.range emb
g : X ≃ₜ (↑KH : Type) := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
f' : (ℕ → Bool) → (↑KC : Type) := Subtype.coind f (p := fun (x : ℕ → Bool) ↦ x ∈ KC) ⋯
hf'_surjective : Function.Surjective f'
h : (↑KC : Type) → (↑KH : Type) := KH.restrictPreimage cantorToHilbert
hh_continuous : Continuous h
hh_surjective : Function.Surjective h
⊢ ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f

Tactic:
exact ⟨g.symm ∘ h ∘ f', by fun_prop, g.symm.surjective.comp <| hh_surjective.comp hf'_surjective⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
s : Set X
⊢ let this := borel X;
  BorelSpace X

Tactic:
borelize X
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
s : Set X
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ ℝ≥0∞

Tactic:
exact ⨆ (d : ℝ≥0) (_ : @hausdorffMeasure X _ _ ⟨rfl⟩ d s = ∞), d
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
borelize :
  ∀ [inst_3 : BorelSpace X],
    dimH s =
      ⨆ (d : ℝ≥0),
        ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞)
⊢ dimH s =
    ⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞)

Tactic:
borelize X
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
inst_1 : BorelSpace X
this : MeasurableSpace X := borel X
rw rw₁ :
  Eq (α := ℝ≥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∞)), (↑d : ℝ≥0∞))
⊢ dimH s =
    ⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞)

Tactic:
rw [dimH]

Premises used: dimH
-- 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∞) < dimH s
⊢ ∃ (i : ℝ≥0) (_ : Eq (α := ℝ≥0∞) (((μH[(↑i : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (↑d : ℝ≥0∞) < (↑i : ℝ≥0∞)

Tactic:
simp only [dimH_def, lt_iSup_iff] at h

Premises used: dimH_def, lt_iSup_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
d : ℝ≥0
h :
  ∃ (i : ℝ≥0) (_ : Eq (α := ℝ≥0∞) (((μH[(↑i : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (↑d : ℝ≥0∞) < (↑i : ℝ≥0∞)
rcases :
  ∀ (d' : ℝ≥0) (hsd' : Eq (α := ℝ≥0∞) (((μH[(↑d' : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hdd' : (↑d : ℝ≥0∞) < (↑d' : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rcases h with ⟨d', hsd', hdd'⟩
-- 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 d' : ℝ≥0
hsd' : Eq (α := ℝ≥0∞) (((μH[(↑d' : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hdd' : (↑d : ℝ≥0∞) < (↑d' : ℝ≥0∞)
⊢ (↑d : ℝ) < (↑d' : ℝ)

Tactic:
rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hdd'

Premises used: ENNReal.coe_lt_coe, NNReal.coe_lt_coe
-- 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 d' : ℝ≥0
hsd' : Eq (α := ℝ≥0∞) (((μH[(↑d' : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hdd' : (↑d : ℝ) < (↑d' : ℝ)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
top_unique (hsd' ▸ hausdorffMeasure_mono hdd'.le _)

Premises used: MeasureTheory.Measure.hausdorffMeasure_mono, Eq.rec, LT.lt.le, top_unique
-- 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 d' : ℝ≥0
hsd' : Eq (α := ℝ≥0∞) (((μH[(↑d' : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hdd' : (↑d : ℝ) < (↑d' : ℝ)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact top_unique (hsd' ▸ hausdorffMeasure_mono hdd'.le _)

Premises used: top_unique
-- 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
⊢ dimH s ≤ d

Tactic:
(dimH_def s).trans_le <| iSup₂_le H

Premises used: iSup₂_le, Eq.trans_le, 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
d : ℝ≥0
h : Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ dimH s ≤ (↑d : ℝ≥0∞)

Tactic:
le_of_not_gt <| mt hausdorffMeasure_of_lt_dimH h

Premises used: le_of_not_gt, mt, hausdorffMeasure_of_lt_dimH
-- 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 : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  (↑d : ℝ≥0∞) ≤
    ⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞)
⊢ (↑d : ℝ≥0∞) ≤ dimH s

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
d : ℝ≥0
h : 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∞)), (↑d : ℝ≥0∞)

Tactic:
le_iSup₂ (α := ℝ≥0∞) d h

Premises used: le_iSup₂
-- 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 : 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∞)), (↑d : ℝ≥0∞)

Tactic:
exact le_iSup₂ (α := ℝ≥0∞) d h

Premises used: le_iSup₂
-- 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 : dimH s < (↑d : ℝ≥0∞)
⊢ ⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞) <
    (↑d : ℝ≥0∞)

Tactic:
rw [dimH_def] at h

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
d : ℝ≥0
h :
  ⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞) <
    (↑d : ℝ≥0∞)
rcases :
  ∀ (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' : ℝ≥0∞) < (↑d : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hsd', hd'd⟩

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
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' : ℝ≥0∞) < (↑d : ℝ≥0∞)
⊢ (↑d' : ℝ) < (↑d : ℝ)

Tactic:
rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hd'd

Premises used: ENNReal.coe_lt_coe, NNReal.coe_lt_coe
-- 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:
(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