awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
ε0 : (↑ε : ℝ≥0∞) / 2 ≠ 0
this : infEDist x s < infEDist x s + (↑ε : ℝ≥0∞) / 2
y : α
ys : y ∈ s
dxy : edist x y < infEDist x s + (↑ε : ℝ≥0∞) / 2
⊢ infEDist x t ≤ infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
have this₁ : hausdorffEDist s t < hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2
Tactic: have : hausdorffEDist s t < hausdorffEDist s t + ε / 2 :=
      ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).2.ne ε0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
ε0 : (↑ε : ℝ≥0∞) / 2 ≠ 0
this_1 : infEDist x s < infEDist x s + (↑ε : ℝ≥0∞) / 2
y : α
ys : y ∈ s
dxy : edist x y < infEDist x s + (↑ε : ℝ≥0∞) / 2
this : hausdorffEDist s t < hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2
⊢ infEDist x t ≤ infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
have obtain : ∀ (z : α) (zt : z ∈ t) (dyz : edist y z < hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2),
  infEDist x t ≤ infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
Tactic: obtain ⟨z : α, zt : z ∈ t, dyz : edist y z < hausdorffEDist s t + ↑ε / 2⟩ :=
      exists_edist_lt_of_hausdorffEDist_lt ys this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
ε0 : (↑ε : ℝ≥0∞) / 2 ≠ 0
this_1 : infEDist x s < infEDist x s + (↑ε : ℝ≥0∞) / 2
y : α
ys : y ∈ s
dxy : edist x y < infEDist x s + (↑ε : ℝ≥0∞) / 2
this : hausdorffEDist s t < hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2
z : α
zt : z ∈ t
dyz : edist y z < hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2
⊢ infEDist x s + (↑ε : ℝ≥0∞) / 2 + (hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2) =
    infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
have rw : infEDist x s + hausdorffEDist s t + ((↑ε : ℝ≥0∞) / 2 + (↑ε : ℝ≥0∞) / 2) =
  infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
Tactic: rw [add_add_add_comm, ENNReal.add_halves]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
ε0 : (↑ε : ℝ≥0∞) / 2 ≠ 0
this_1 : infEDist x s < infEDist x s + (↑ε : ℝ≥0∞) / 2
y : α
ys : y ∈ s
dxy : edist x y < infEDist x s + (↑ε : ℝ≥0∞) / 2
this : hausdorffEDist s t < hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2
z : α
zt : z ∈ t
dyz : edist y z < hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2
rw :
  infEDist x s + hausdorffEDist s t + ((↑ε : ℝ≥0∞) / 2 + (↑ε : ℝ≥0∞) / 2) =
    infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
⊢ infEDist x s + (↑ε : ℝ≥0∞) / 2 + (hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2) =
    infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
have rw₁ : infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞) = infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
Tactic: rw [add_add_add_comm, ENNReal.add_halves]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
ε0 : (↑ε : ℝ≥0∞) / 2 ≠ 0
this_1 : infEDist x s < infEDist x s + (↑ε : ℝ≥0∞) / 2
y : α
ys : y ∈ s
dxy : edist x y < infEDist x s + (↑ε : ℝ≥0∞) / 2
this : hausdorffEDist s t < hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2
z : α
zt : z ∈ t
dyz : edist y z < hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2
⊢ infEDist x t ≤ infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
have infEDist : infEDist x s + (↑ε : ℝ≥0∞) / 2 + (hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2) =
  infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
Tactic: calc
      infEDist x t ≤ edist x z := infEDist_le_edist_of_mem zt
      _ ≤ edist x y + edist y z := edist_triangle _ _ _
      _ ≤ infEDist x s + ε / 2 + (hausdorffEDist s t + ε / 2) := add_le_add dxy.le dyz.le
      _ = infEDist x s + hausdorffEDist s t + ε := by
        rw [add_add_add_comm, ENNReal.add_halves]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ hausdorffEDist s t ≤ ediam (s ∪ t)
have rcases : ∀ (x : α) (xs : x ∈ s), hausdorffEDist s t ≤ ediam (s ∪ t)
Tactic: rcases hs with ⟨x, xs⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
ht : t.Nonempty
x : α
xs : x ∈ s
⊢ hausdorffEDist s t ≤ ediam (s ∪ t)
have rcases : ∀ (y : α) (yt : y ∈ t), hausdorffEDist s t ≤ ediam (s ∪ t)
Tactic: rcases ht with ⟨y, yt⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffEDist s t ≤ ediam (s ∪ t)
have refine_1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ ediam (s ∪ t)
Tactic: refine hausdorffEDist_le_of_mem_edist ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
refine_1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ ediam (s ∪ t)
⊢ hausdorffEDist s t ≤ ediam (s ∪ t)
have refine_2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ediam (s ∪ t)
Tactic: refine hausdorffEDist_le_of_mem_edist ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
⊢ hausdorffEDist s u ≤ hausdorffEDist s t + hausdorffEDist t u
have rw : max (⨆ x ∈ s, infEDist x u) (⨆ y ∈ u, infEDist y s) ≤ hausdorffEDist s t + hausdorffEDist t u
Tactic: rw [hausdorffEDist_def]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
⊢ max (⨆ x ∈ s, infEDist x u) (⨆ y ∈ u, infEDist y s) ≤ hausdorffEDist s t + hausdorffEDist t u
have simp : (∀ (i : α) (i_1 : i ∈ s), infEDist i u ≤ hausdorffEDist s t + hausdorffEDist t u) ∧
  ∀ (i : α) (i_1 : i ∈ u), infEDist i s ≤ hausdorffEDist s t + hausdorffEDist t u
Tactic: simp only [sup_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
⊢ (∀ (i : α) (i_1 : i ∈ s), infEDist i u ≤ hausdorffEDist s t + hausdorffEDist t u) ∧
    ∀ (i : α) (i_1 : i ∈ u), infEDist i s ≤ hausdorffEDist s t + hausdorffEDist t u
have left : ∀ (i : α) (i_1 : i ∈ s), infEDist i u ≤ hausdorffEDist s t + hausdorffEDist t u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
left : ∀ (i : α) (i_1 : i ∈ s), infEDist i u ≤ hausdorffEDist s t + hausdorffEDist t u
⊢ (∀ (i : α) (i_1 : i ∈ s), infEDist i u ≤ hausdorffEDist s t + hausdorffEDist t u) ∧
    ∀ (i : α) (i_1 : i ∈ u), infEDist i s ≤ hausdorffEDist s t + hausdorffEDist t u
have right : ∀ (i : α) (i_1 : i ∈ u), infEDist i s ≤ hausdorffEDist s t + hausdorffEDist t u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
x : α
xs : x ∈ s
⊢ infEDist x t + hausdorffEDist t u ≤ hausdorffEDist s t + hausdorffEDist t u
have grw : hausdorffEDist s t + hausdorffEDist t u ≤ hausdorffEDist s t + hausdorffEDist t u
Tactic: grw [infEDist_le_hausdorffEDist_of_mem xs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
x : α
xu : x ∈ u
⊢ infEDist x t + hausdorffEDist t s ≤ hausdorffEDist u t + hausdorffEDist t s
have grw : hausdorffEDist u t + hausdorffEDist t s ≤ hausdorffEDist u t + hausdorffEDist t s
Tactic: grw [infEDist_le_hausdorffEDist_of_mem xu]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
⊢ hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0
have rw : closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
Tactic: rw [hausdorffEDist_zero_iff_closure_eq_closure, closure_closure]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
rw :
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0
have rw₁ : closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: rw [hausdorffEDist_zero_iff_closure_eq_closure, closure_closure]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t = hausdorffEDist s t
have refine_1 : hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t ≤ hausdorffEDist s t
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
refine_1 : hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t ≤ hausdorffEDist s t
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t = hausdorffEDist s t
have refine_2 : hausdorffEDist s t ≤ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t ≤ hausdorffEDist s t
have _ : hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) s + hausdorffEDist s t =
  hausdorffEDist s t
Tactic: calc
      _ ≤ hausdorffEDist (closure s) s + hausdorffEDist s t := hausdorffEDist_triangle
      _ = hausdorffEDist s t := by simp [hausdorffEDist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist s t ≤ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t
have _ : hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) +
    hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t =
  hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t
Tactic: calc
      _ ≤ hausdorffEDist s (closure s) + hausdorffEDist (closure s) t := hausdorffEDist_triangle
      _ = hausdorffEDist (closure s) t := by simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ hausdorffEDist s t = 0 ↔ s = t
have rw : closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t ↔
  s = t
Tactic: rw [hausdorffEDist_zero_iff_closure_eq_closure, hs.closure_eq, ht.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
rw :
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
      closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t ↔
    s = t
⊢ hausdorffEDist s t = 0 ↔ s = t
have rw₁ : s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t ↔ s = t
Tactic: rw [hausdorffEDist_zero_iff_closure_eq_closure, hs.closure_eq, ht.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
rw :
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
      closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t ↔
    s = t
rw₁ : s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t ↔ s = t
⊢ hausdorffEDist s t = 0 ↔ s = t
have rw₂ : s = t ↔ s = t
Tactic: rw [hausdorffEDist_zero_iff_closure_eq_closure, hs.closure_eq, ht.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ne : s.Nonempty
⊢ hausdorffEDist s ∅ = ∞
have rcases : ∀ (x : α) (xs : x ∈ s), hausdorffEDist s ∅ = ∞
Tactic: rcases ne with ⟨x, xs⟩
Cleared hypotheses: ne
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
x : α
xs : x ∈ s
⊢ hausdorffEDist s ∅ = ∞
have this : infEDist x ∅ ≤ hausdorffEDist s ∅
Tactic: have : infEDist x ∅ ≤ hausdorffEDist s ∅ := infEDist_le_hausdorffEDist_of_mem xs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEDist s t ≠ ∞
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty
have inl : ∀ (fin : hausdorffEDist ∅ t ≠ ∞), Eq.{u + 1} (α := Set α) ∅ ∅ ∧ t = ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ t.Nonempty
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s, fin
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEDist s t ≠ ∞
inl : ∀ (fin : hausdorffEDist ∅ t ≠ ∞), Eq.{u + 1} (α := Set α) ∅ ∅ ∧ t = ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ t.Nonempty
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty
have inr : ∀ (hs : s.Nonempty), s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist ∅ t ≠ ∞
⊢ Eq.{u + 1} (α := Set α) ∅ ∅ ∧ t = ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ t.Nonempty
have inl : ∀ (fin : hausdorffEDist.{u} (α := α) ∅ ∅ ≠ ∞),
  Eq.{u + 1} (α := Set α) ∅ ∅ ∧ Eq.{u + 1} (α := Set α) ∅ ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ Set.Nonempty.{u} (α := α) ∅
Tactic: rcases t.eq_empty_or_nonempty with rfl | ht
Cleared hypotheses: t, fin
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist ∅ t ≠ ∞
inl :
  ∀ (fin : hausdorffEDist.{u} (α := α) ∅ ∅ ≠ ∞),
    Eq.{u + 1} (α := Set α) ∅ ∅ ∧ Eq.{u + 1} (α := Set α) ∅ ∅ ∨
      Set.Nonempty.{u} (α := α) ∅ ∧ Set.Nonempty.{u} (α := α) ∅
⊢ Eq.{u + 1} (α := Set α) ∅ ∅ ∧ t = ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ t.Nonempty
have inl₁ : ∀ (ht : t.Nonempty), Eq.{u + 1} (α := Set α) ∅ ∅ ∧ t = ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ t.Nonempty
Tactic: rcases t.eq_empty_or_nonempty with rfl | ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist ∅ t ≠ ∞
ht : t.Nonempty
⊢ Eq.{u + 1} (α := Set α) ∅ ∅ ∧ t = ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ t.Nonempty
have fin₁ : hausdorffEDist t ∅ ≠ ∞
Tactic: rw [hausdorffEDist_comm] at fin
Cleared hypotheses: fin, ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
⊢ hausdorffEDist (α := α) {x} {y} = edist x y
have simp_rw : max (edist x y) (edist y x) = edist x y
Tactic: simp_rw [hausdorffEDist, iSup_singleton, infEDist_singleton]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
⊢ max (edist x y) (edist y x) = edist x y
have nth_rw : max (edist x y) (edist x y) = edist x y
Tactic: nth_rw 2 [edist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ hausdorffEDist.{u} (α := α) (⋃ (i : ι), s i) (⋃ (i : ι), t i) ≤ ⨆ (i : ι), hausdorffEDist (s i) (t i)
have simp_rw : (∀ (i : ι) (i_1 : α) (i : i_1 ∈ s i),
    LE.le (α := ℝ≥0∞) (⨅ (i : ι), infEDist i_1 (t i))
      (⨆ (i : ι), max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)))) ∧
  ∀ (i : ι) (i_1 : α) (i : i_1 ∈ t i),
    LE.le (α := ℝ≥0∞) (⨅ (i : ι), infEDist i_1 (s i))
      (⨆ (i : ι), max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)))
Tactic: simp_rw [hausdorffEDist, max_le_iff, iSup_iUnion, iSup_le_iff, infEDist_iUnion]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ (∀ (i : ι) (i_1 : α) (i : i_1 ∈ s i),
      LE.le (α := ℝ≥0∞) (⨅ (i : ι), infEDist i_1 (t i))
        (⨆ (i : ι), max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)))) ∧
    ∀ (i : ι) (i_1 : α) (i : i_1 ∈ t i),
      LE.le (α := ℝ≥0∞) (⨅ (i : ι), infEDist i_1 (s i))
        (⨆ (i : ι), max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)))
have left : ∀ (i : ι) (i_1 : α) (i : i_1 ∈ s i),
  LE.le (α := ℝ≥0∞) (⨅ (i : ι), infEDist i_1 (t i))
    (⨆ (i : ι), max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
left :
  ∀ (i : ι) (i_1 : α) (i : i_1 ∈ s i),
    LE.le (α := ℝ≥0∞) (⨅ (i : ι), infEDist i_1 (t i))
      (⨆ (i : ι), max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)))
⊢ (∀ (i : ι) (i_1 : α) (i : i_1 ∈ s i),
      LE.le (α := ℝ≥0∞) (⨅ (i : ι), infEDist i_1 (t i))
        (⨆ (i : ι), max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)))) ∧
    ∀ (i : ι) (i_1 : α) (i : i_1 ∈ t i),
      LE.le (α := ℝ≥0∞) (⨅ (i : ι), infEDist i_1 (s i))
        (⨆ (i : ι), max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)))
have right : ∀ (i : ι) (i_1 : α) (i : i_1 ∈ t i),
  LE.le (α := ℝ≥0∞) (⨅ (i : ι), infEDist i_1 (s i))
    (⨆ (i : ι), max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ ∀ (i : ι) (i_1 : α) (i : i_1 ∈ s i),
    LE.le (α := ℝ≥0∞) (⨅ (i : ι), infEDist i_1 (t i))
      (⨆ (i : ι), max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)))
have left : ∀ (i : ι) (x : α) (hx : x ∈ s i), infEDist x (t i) ≤ max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))
Tactic: refine fun i x hx => (iInf_le _ i).trans <| le_iSup_of_le i ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ ∀ (i : ι) (i_1 : α) (i : i_1 ∈ t i),
    LE.le (α := ℝ≥0∞) (⨅ (i : ι), infEDist i_1 (s i))
      (⨆ (i : ι), max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)))
have right : ∀ (i : ι) (x : α) (hx : x ∈ t i), infEDist x (s i) ≤ max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))
Tactic: refine fun i x hx => (iInf_le _ i).trans <| le_iSup_of_le i ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s₁ s₂ t₁ t₂ : Set α
⊢ hausdorffEDist (s₁ ∪ s₂) (t₁ ∪ t₂) ≤ max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂)
have simp_rw : hausdorffEDist.{u} (α := α) (⋃ (b : Bool), bif b then s₁ else s₂) (⋃ (b : Bool), bif b then t₁ else t₂) ≤
  ⨆ (b : Bool), bif b then hausdorffEDist s₁ t₁ else hausdorffEDist s₂ t₂
Tactic: simp_rw [union_eq_iUnion, sup_eq_iSup]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s₁ t₁ : Set α
s₂ t₂ : Set β
⊢ hausdorffEDist (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) ≤ max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂)
have refine : ∀ (x : ℝ≥0∞), max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂) ≤ x → hausdorffEDist (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) ≤ x
Tactic: refine le_of_forall_ge fun _ _ => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ infDist x s = ⨅ (y : (↑s : Type u)), dist x (↑y : α)
have rw : Eq (α := ℝ) (⨅ (i : Subtype (Membership.mem s)), (edist x (↑i : α)).toReal) (⨅ (y : (↑s : Type u)), dist x (↑y : α))
Tactic: rw [infDist, infEDist, iInf_subtype', ENNReal.toReal_iInf]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
rw :
  Eq (α := ℝ) (⨅ (i : Subtype (Membership.mem s)), (edist x (↑i : α)).toReal) (⨅ (y : (↑s : Type u)), dist x (↑y : α))
⊢ infDist x s = ⨅ (y : (↑s : Type u)), dist x (↑y : α)
have rw₁ : ∀ (i : Subtype (Membership.mem s)), edist x (↑i : α) ≠ ∞
Tactic: rw [infDist, infEDist, iInf_subtype', ENNReal.toReal_iInf]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : s.Nonempty
⊢ infEDist x s ≠ ∞
have rcases : ∀ (y : α) (hy : y ∈ s), infEDist x s ≠ ∞
Tactic: rcases h with ⟨y, hy⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ infEDist x s = ∞ ↔ s = ∅
have inl : infEDist x ∅ = ∞ ↔ Eq.{u + 1} (α := Set α) ∅ ∅
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
inl : infEDist x ∅ = ∞ ↔ Eq.{u + 1} (α := Set α) ∅ ∅
⊢ infEDist x s = ∞ ↔ s = ∅
have inr : ∀ (hs : s.Nonempty), infEDist x s = ∞ ↔ s = ∅
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ infDist x s ≤ dist x y
have rw : (infEDist x s).toReal ≤ (edist x y).toReal
Tactic: rw [dist_edist, infDist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hs : s.Nonempty
⊢ r ≤ infDist x s ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
have simp_rw : r ≤ (infEDist x s).toReal ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
Tactic: simp_rw [infDist, ← ENNReal.ofReal_le_iff_le_toReal (infEDist_ne_top hs), le_infEDist,
    ENNReal.ofReal_le_iff_le_toReal (edist_ne_top _ _), ← dist_edist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hs : s.Nonempty
simp_rw : r ≤ (infEDist x s).toReal ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
⊢ r ≤ infDist x s ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
have simp_rw₁ : ENNReal.ofReal r ≤ infEDist x s ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
Tactic: simp_rw [infDist, ← ENNReal.ofReal_le_iff_le_toReal (infEDist_ne_top hs), le_infEDist,
    ENNReal.ofReal_le_iff_le_toReal (edist_ne_top _ _), ← dist_edist]