awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (hypothesis)
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
⊢ ∃ (y : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) y ∧ dist (optimalGHInjr X Y z) y ≤ r
have 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))
Tactic: have I2 :
        ⨅ x, optimalGHDist X Y (inl x, inr z) ≤ ⨆ y, ⨅ x, optimalGHDist X Y (inl x, inr y) :=
      le_csSup (by simpa using HD_bound_aux2 _ 0) (mem_range_self _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (hypothesis)
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))
⊢ ∃ (y : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) y ∧ dist (optimalGHInjr X Y z) y ≤ r
have I : ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z) < r
Tactic: have I : ⨅ x, optimalGHDist X Y (inl x, inr z) < r := lt_of_le_of_lt I2 I1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
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
⊢ ∃ (y : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) y ∧ dist (optimalGHInjr X Y z) y ≤ r
have refine_2 : ∀ (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: rcases exists_lt_of_csInf_lt (range_nonempty _) I with ⟨r', ⟨z', rfl⟩, hr'⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
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
have refine_2 : dist (α := OptimalGHCoupling X Y) (optimalGHInjr X Y z) (optimalGHInjl X Y z') < r
Tactic: refine ⟨optimalGHInjl X Y z', mem_range_self _, le_of_lt ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
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
⊢ dist (α := OptimalGHCoupling X Y) (optimalGHInjr X Y z) (optimalGHInjl X Y z') < r
have refine_2 : dist (α := OptimalGHCoupling X Y) (optimalGHInjl X Y z') (optimalGHInjr X Y z) < r
Tactic: rwa [dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffAlexandroff (goal)
Goal:
⊢ Function.Surjective fromBinary
have 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
Tactic: refine Subtype.coind_surjective _ ((ofDigits_SurjOn (by norm_num)).comp ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffAlexandroff (goal)
Goal:
X : Set (ℕ → Bool)
h_closed : IsClosed X
h_nonempty : X.Nonempty
⊢ ∃ (f : (ℕ → Bool) → ℕ → Bool), Continuous f ∧ Set.range f = X
have 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
Tactic: obtain ⟨f, fs, frange, hf⟩ := PiNat.exists_lipschitz_retraction_of_isClosed h_closed h_nonempty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffAlexandroff (goal)
Goal:
X : Type u_1
inst : Nonempty X
inst_1 : MetricSpace X
inst_2 : CompactSpace X
this : TopologicalSpace.SeparableSpace X := ⋯
⊢ ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f
have obtain : ∀ (emb : X → ℕ → (↑unitInterval : Type)) (h_emb : Topology.IsEmbedding emb),
  ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f
Tactic: obtain ⟨emb, h_emb⟩ := Metric.PiNatEmbed.exists_embedding_to_hilbert_cube (X := X)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffAlexandroff (hypothesis)
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
⊢ ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f
have hKC_closed : 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)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffAlexandroff (goal)
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) → X), Continuous f ∧ Function.Surjective f
have obtain : ∀ (f : (ℕ → Bool) → ℕ → Bool) (hf_continuous : Continuous f) (hf_surjective : Set.range f = KC),
  ∃ (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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffAlexandroff (hypothesis)
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) ⋯
⊢ ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f
have hf'_surjective : Function.Surjective f'
Tactic: have hf'_surjective : Function.Surjective f' := Subtype.coind_surjective _ (by grind [Set.SurjOn])
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffAlexandroff (hypothesis)
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
⊢ ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f
have hh_continuous : Continuous h
Tactic: have hh_continuous : Continuous h := Continuous.restrictPreimage cantorToHilbert_continuous
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffAlexandroff (hypothesis)
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
⊢ ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f
have hh_surjective : Function.Surjective h
Tactic: have hh_surjective : Function.Surjective h :=
    Set.restrictPreimage_surjective _ cantorToHilbert_surjective
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
s : Set X
⊢ ℝ≥0∞
have this : let this := borel X;
BorelSpace X
Tactic: borelize X
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
⊢ dimH s =
    ⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞)
have borelize : ∀ [inst_3 : BorelSpace X],
  dimH s =
    ⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞)
Tactic: borelize X
Cleared hypotheses: inst_1, inst_2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
inst_1 : BorelSpace X
this : MeasurableSpace X := borel X
⊢ dimH s =
    ⨆ (d : ℝ≥0),
      ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞)
have 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∞))
Tactic: rw [dimH]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have h₁ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have 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∞)
Tactic: rcases h with ⟨d', hsd', hdd'⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have hdd'₁ : (↑d : ℝ) < (↑d' : ℝ)
Tactic: rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hdd'
Cleared hypotheses: hdd'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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∞) ≤ dimH s
have rw : (↑d : ℝ≥0∞) ≤
  ⨆ (d : ℝ≥0),
    ⨆ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), (↑d : ℝ≥0∞)
Tactic: rw [dimH_def]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have h₁ : ⨆ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hsd', hd'd⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have hd'd₁ : (↑d' : ℝ) < (↑d : ℝ)
Tactic: rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hd'd
Cleared hypotheses: hd'd
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
⊢ dimH s =
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
have a : dimH s ≤
  ⨅ (d : ℝ≥0),
    ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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∞)
⊢ dimH s =
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
have a₁ : ⨅ (d : ℝ≥0),
    ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞) ≤
  dimH s
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
⊢ dimH s ≤
    ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)
have 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∞))
Tactic: rw [dimH_def]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
⊢ 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∞))
have 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
Tactic: simp only [le_iInf_iff, iSup_le_iff, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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∞)
⊢ j ≤ i
have a : ∀ (hij : i < j), False
Tactic: by_contra! hij
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
⊢ ⨅ (d : ℝ≥0),
      ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞) ≤
    dimH s
have a : ∀
  (h :
    dimH s <
      ⨅ (d : ℝ≥0),
        ⨅ (_ : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), (↑d : ℝ≥0∞)),
  False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
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∞)
⊢ False
have 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
Tactic: rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hdim_lt, hlt⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
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∞)
⊢ False
have h0 : 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
s t : Set X
h : s ⊆ t
⊢ dimH s ≤ dimH t
have this : let this := borel X;
BorelSpace X
Tactic: borelize X
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
h : s.Subsingleton
⊢ dimH s = 0
have this : let this := borel X;
BorelSpace X
Tactic: borelize X
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
h : s.Subsingleton
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ dimH s = 0
have rw : dimH s ≤ 0
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
s : Set X
h : s.Subsingleton
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ dimH s ≤ 0
have h₁ : Ne (α := ℝ≥0∞) (((μH[(↑0 : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply dimH_le_of_hausdorffMeasure_ne_top