awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty.{u_4 + 1} (↑s : Type u_4)
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(AffineSubspace.direction (affineSpan ℝ s)) :=
  AffineIsometryEquiv.constVSub ℝ
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) (hne.some (s := s)) ⋯)
hs_eq :
  s =
    image (α := ↥(affineSpan ℝ s))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s)
⊢ Set.Nonempty (α := ↥(AffineSubspace.direction (affineSpan ℝ s)))
    (interior
      (image (α := ↥(affineSpan ℝ s)) (⇑φ : (a : ↥(affineSpan ℝ s)) → ↥(affineSpan ℝ s).direction)
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s)))
have simp_rw : Set.Nonempty (α := ↥(affineSpan ℝ s))
  (interior (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s))
Tactic: simp_rw [← AffineIsometryEquiv.coe_toHomeomorph, ← φ.toHomeomorph.image_interior, image_nonempty]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
⊢ dimH (X := ℝ) univ = 1
have rw : Eq (α := ℝ≥0∞) (↑(finrank ℝ ℝ) : ℝ≥0∞) 1
Tactic: rw [dimH_univ_eq_finrank ℝ, Module.finrank_self, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
rw : Eq (α := ℝ≥0∞) (↑(finrank ℝ ℝ) : ℝ≥0∞) 1
⊢ dimH (X := ℝ) univ = 1
have rw₁ : Eq (α := ℝ≥0∞) (↑1 : ℝ≥0∞) 1
Tactic: rw [dimH_univ_eq_finrank ℝ, Module.finrank_self, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
rw : Eq (α := ℝ≥0∞) (↑(finrank ℝ ℝ) : ℝ≥0∞) 1
rw₁ : Eq (α := ℝ≥0∞) (↑1 : ℝ≥0∞) 1
⊢ dimH (X := ℝ) univ = 1
have rw₂ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [dimH_univ_eq_finrank ℝ, Module.finrank_self, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
⊢ dimH s < ∞
have dimH : LT.lt (α := ℝ≥0∞) (↑(finrank ℝ E) : ℝ≥0∞) ∞
Tactic: calc
  dimH s ≤ dimH (univ : Set E) := dimH_mono (subset_univ s)
  _ = finrank ℝ E := dimH_univ_eq_finrank E
  _ < ⊤ := by simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
d : ℝ
hd : (↑(finrank ℝ E) : ℝ) < d
⊢ Eq.{u_4 + 1} (α := Measure E) μH[d] 0
have lift : ∀ (d : ℝ≥0) (hd : (↑(finrank ℝ E) : ℝ) < (↑d : ℝ)), Eq.{u_4 + 1} (α := Measure E) μH[(↑d : ℝ)] 0
Tactic: lift d to ℝ≥0 using (Nat.cast_nonneg _).trans hd.le
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
d : ℝ≥0
hd : (↑(finrank ℝ E) : ℝ) < (↑d : ℝ)
⊢ Eq.{u_4 + 1} (α := Measure E) μH[(↑d : ℝ)] 0
have rw : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_univ_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
d : ℝ≥0
hd : (↑(finrank ℝ E) : ℝ) < (↑d : ℝ)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have h : dimH.{u_4} (X := E) univ < (↑d : ℝ≥0∞)
Tactic: apply hausdorffMeasure_of_dimH_lt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
d : ℝ≥0
hd : (↑(finrank ℝ E) : ℝ) < (↑d : ℝ)
⊢ dimH.{u_4} (X := E) univ < (↑d : ℝ≥0∞)
have h : (↑(finrank ℝ E) : ℝ≥0∞) < (↑d : ℝ≥0∞)
Tactic: rw [dimH_univ_eq_finrank]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x y : E
h : x ≠ y
⊢ dimH (segment ℝ x y) = 1
have rw : Eq (α := ℝ≥0∞) (↑(finrank.{0, u_4} ℝ ↥(ℝ ∙ (y -ᵥ x))) : ℝ≥0∞) 1
Tactic: rw [Convex.dimH_eq_finrank_vectorSpan (convex_segment x y) ⟨x, left_mem_segment ℝ x y⟩,
      vectorSpan_segment]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : dimH s < (↑(finrank ℝ E) : ℝ≥0∞)
⊢ Dense sᶜ
have refine : ∀ (x : E) (t : Set E) (ht : t ∈ 𝓝 x) (he : t ∩ sᶜ = ∅), (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH s
Tactic: refine fun x => mem_closure_iff_nhds.2 fun t ht => nonempty_iff_ne_empty.2 fun he => hs.not_ge ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : dimH s < (↑(finrank ℝ E) : ℝ≥0∞)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ∩ sᶜ = ∅
⊢ (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH s
have he₁ : t ⊆ s
Tactic: rw [← diff_eq, diff_eq_empty] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : dimH s < (↑(finrank ℝ E) : ℝ≥0∞)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ⊆ s
⊢ (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH s
have rw : dimH t ≤ dimH s
Tactic: rw [← Real.dimH_of_mem_nhds ht]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
h : ContDiff ℝ 1 f
⊢ dimH (range f) = dimH (f '' univ)
have rw : dimH (range f) = dimH (range f)
Tactic: rw [image_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
⊢ infEDist x s < r ↔ ∃ y ∈ s, edist x y < r
have simp_rw : ⨅ y ∈ s, edist x y < r ↔ ∃ y ∈ s, edist x y < r
Tactic: simp_rw [infEDist, iInf_lt_iff, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
simp_rw : ⨅ y ∈ s, edist x y < r ↔ ∃ y ∈ s, edist x y < r
⊢ infEDist x s < r ↔ ∃ y ∈ s, edist x y < r
have simp_rw₁ : (∃ (i : α) (_ : i ∈ s), edist x i < r) ↔ ∃ y ∈ s, edist x y < r
Tactic: simp_rw [infEDist, iInf_lt_iff, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
⊢ infEDist x s ≤ edist x y + infEDist y s
have rw : infEDist x s ≤ infEDist y s + edist x y
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ infEDist x s + ediam s
have simp_rw : edist x y ≤ ⨅ i ∈ s, edist x i + ediam s
Tactic: simp_rw [infEDist, ENNReal.iInf_add]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ ⨅ i ∈ s, edist x i + ediam s
have refine : ∀ (i : α) (hi : i ∈ s), edist x y ≤ edist x i + ediam s
Tactic: refine le_iInf₂ fun i hi => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = infEDist x s
have refine : infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
Tactic: refine le_antisymm (infEDist_anti subset_closure) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
have refine : ∀ (ε : ℝ≥0) (εpos : 0 < ε) (h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞),
  infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
Tactic: refine ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
have ε0 : 0 < (↑ε : ℝ≥0∞) / 2
Tactic: have ε0 : 0 < (ε / 2 : ℝ≥0∞) := by simpa [pos_iff_ne_zero] using εpos
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
have this : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
Tactic: have : infEDist x (closure s) < infEDist x (closure s) + ε / 2 :=
    ENNReal.lt_add_right h.ne ε0.ne'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
have obtain : ∀ (y : α) (ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
  (hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2),
  infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
Tactic: obtain ⟨y : α, ycs : y ∈ closure s, hy : edist x y < infEDist x (closure s) + ↑ε / 2⟩ :=
    infEDist_lt_iff.mp this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
y : α
ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
have obtain : ∀ (z : α) (zs : z ∈ s) (dyz : edist y z < (↑ε : ℝ≥0∞) / 2),
  infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
Tactic: obtain ⟨z : α, zs : z ∈ s, dyz : edist y z < ↑ε / 2⟩ := EMetric.mem_closure_iff.1 ycs (ε / 2) ε0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
y : α
ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
z : α
zs : z ∈ s
dyz : edist y z < (↑ε : ℝ≥0∞) / 2
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2 + (↑ε : ℝ≥0∞) / 2 =
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
have rw : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + ((↑ε : ℝ≥0∞) / 2 + (↑ε : ℝ≥0∞) / 2) =
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
Tactic: rw [add_assoc, ENNReal.add_halves]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
y : α
ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
z : α
zs : z ∈ s
dyz : edist y z < (↑ε : ℝ≥0∞) / 2
rw :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + ((↑ε : ℝ≥0∞) / 2 + (↑ε : ℝ≥0∞) / 2) =
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2 + (↑ε : ℝ≥0∞) / 2 =
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
have rw₁ : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) =
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
Tactic: rw [add_assoc, ENNReal.add_halves]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
y : α
ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
z : α
zs : z ∈ s
dyz : edist y z < (↑ε : ℝ≥0∞) / 2
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
have infEDist : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2 + (↑ε : ℝ≥0∞) / 2 =
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
Tactic: calc
    infEDist x s ≤ edist x z := infEDist_le_edist_of_mem zs
    _ ≤ edist x y + edist y z := edist_triangle _ _ _
    _ ≤ infEDist x (closure s) + ε / 2 + ε / 2 := add_le_add (le_of_lt hy) (le_of_lt dyz)
    _ = infEDist x (closure s) + ↑ε := by rw [add_assoc, ENNReal.add_halves]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
h : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ infEDist x s = 0
have rw : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0
Tactic: rw [← infEDist_closure]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
h : infEDist x s = 0
ε : ℝ≥0∞
εpos : ε > 0
⊢ infEDist x s < ε
have rwa : 0 < ε
Tactic: rwa [h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
h : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ x ∈ s ↔ infEDist x s = 0
have rw : x ∈ s ↔ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: rw [← mem_closure_iff_infEDist_zero, h.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
h : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
rw : x ∈ s ↔ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ x ∈ s ↔ infEDist x s = 0
have rw₁ : x ∈ s ↔ x ∈ s
Tactic: rw [← mem_closure_iff_infEDist_zero, h.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
⊢ 0 < infEDist x E ↔ x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
have rw : 0 < infEDist x E ↔ ¬infEDist x E = 0
Tactic: rw [mem_closure_iff_infEDist_zero, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
rw : 0 < infEDist x E ↔ ¬infEDist x E = 0
⊢ 0 < infEDist x E ↔ x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
have rw₁ : infEDist x E ≠ 0 ↔ ¬infEDist x E = 0
Tactic: rw [mem_closure_iff_infEDist_zero, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
⊢ 0 < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) ↔
    x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
have rw : 0 < infEDist x E ↔ x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
Tactic: rw [infEDist_closure, infEDist_pos_iff_notMem_closure]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
rw : 0 < infEDist x E ↔ x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ 0 < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) ↔
    x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
have rw₁ : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ↔
  x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
Tactic: rw [infEDist_closure, infEDist_pos_iff_notMem_closure]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∃ (ε : ℝ), 0 < ε ∧ ENNReal.ofReal ε < infEDist x E
have h₁ : ∃ (r : ℝ), 0 ≤ r ∧ 0 < ENNReal.ofReal r ∧ ENNReal.ofReal r < infEDist x E
Tactic: rw [← infEDist_pos_iff_notMem_closure, ENNReal.lt_iff_exists_real_btwn] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
h : ∃ (r : ℝ), 0 ≤ r ∧ 0 < ENNReal.ofReal r ∧ ENNReal.ofReal r < infEDist x E
⊢ ∃ (ε : ℝ), 0 < ε ∧ ENNReal.ofReal ε < infEDist x E
have rcases : ∀ (ε : ℝ),
  0 ≤ ε →
    ∀ (ε_pos : 0 < ENNReal.ofReal ε) (ε_lt : ENNReal.ofReal ε < infEDist x E),
      ∃ (ε : ℝ), 0 < ε ∧ ENNReal.ofReal ε < infEDist x E
Tactic: rcases h with ⟨ε, ⟨_, ⟨ε_pos, ε_lt⟩⟩⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
⊢ Disjoint (closedEBall x r) s
have rw : ∀ ⦃a : α⦄, a ∈ closedEBall x r → a ∉ s
Tactic: rw [disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
y : α
hy : y ∈ closedEBall x r
h'y : y ∈ s
⊢ False
have apply : infEDist x s < infEDist x s
Tactic: apply lt_irrefl (infEDist x s)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
y : α
hy : y ∈ closedEBall x r
h'y : y ∈ s
⊢ edist x y ≤ r
have rwa : ∀ (hy : edist y x ≤ r) (h'y : y ∈ s), edist x y ≤ r
Tactic: rwa [Metric.mem_closedEBall, edist_comm] at hy
Cleared hypotheses: hy, h'y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
y : α
hy : y ∈ closedEBall x r
h'y : y ∈ s
rwa : ∀ (hy : edist y x ≤ r) (h'y : y ∈ s), edist x y ≤ r
⊢ edist x y ≤ r
have rwa₁ : ∀ (hy : edist x y ≤ r) (h'y : y ∈ s), edist x y ≤ r
Tactic: rwa [Metric.mem_closedEBall, edist_comm] at hy
Cleared hypotheses: hy, h'y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
y : α
hy : y ∈ closedEBall x r
h'y : y ∈ s
⊢ infEDist x s < infEDist x s
have infEDist : edist x y ≤ r
Tactic: calc
    infEDist x s ≤ edist x y := infEDist_le_edist_of_mem h'y
    _ ≤ r := by rwa [Metric.mem_closedEBall, edist_comm] at hy
    _ < infEDist x s := h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ∃ (F : ℕ → Set α),
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F
have obtain : ∀ (a : ℝ≥0∞) (a_pos : 0 < a) (a_lt_one : a < 1),
  ∃ (F : ℕ → Set α),
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F
Tactic: obtain ⟨a, a_pos, a_lt_one⟩ : ∃ a : ℝ≥0∞, 0 < a ∧ a < 1 := exists_between zero_lt_one
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
⊢ x ∈ U
have by_contra : ∀ (h : x ∉ U), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
h : x ∉ U
⊢ False
have this : infEDist x Uᶜ ≠ 0
Tactic: have : infEDist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
⊢ ∃ (F : ℕ → Set α),
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F
have F_subset : ∀ (n : ℕ), F n ⊆ U
Tactic: have F_subset : ∀ n, F n ⊆ U := fun n x hx ↦ by
    by_contra h
    have : infEDist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
    exact this (infEDist_zero_of_mem h)