awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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
obtain :
  ∀ (z : α) (zt : z ∈ t) (dyz : edist y z < hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2),
    infEDist x t ≤ infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
⊢ 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

Premises used: Metric.hausdorffEDist, Metric.exists_edist_lt_of_hausdorffEDist_lt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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 ≤ edist x z

Tactic:
infEDist_le_edist_of_mem zt

Premises used: Metric.infEDist_le_edist_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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
⊢ edist x z ≤ edist x y + edist y z

Tactic:
edist_triangle _ _ _

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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
⊢ edist x y + edist y z ≤ infEDist x s + (↑ε : ℝ≥0∞) / 2 + (hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2)

Tactic:
add_le_add dxy.le dyz.le

Premises used: add_le_add, LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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∞)
rw₁ rw₂ : infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞) = infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
⊢ infEDist x s + (↑ε : ℝ≥0∞) / 2 + (hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2) =
    infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)

Tactic:
rw [add_add_add_comm, ENNReal.add_halves]

Premises used: ENNReal.add_halves, add_add_add_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : Metric.infEDist x s + hausdorffEDist s t < ∞
ε0 : (↑ε : ℝ≥0∞) / 2 ≠ 0
this_1 : Metric.infEDist x s < Metric.infEDist x s + (↑ε : ℝ≥0∞) / 2
y : α
ys : y ∈ s
dxy : edist x y < Metric.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 :
  Metric.infEDist x s + (↑ε : ℝ≥0∞) / 2 + (hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2) =
    Metric.infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
⊢ Metric.infEDist x t ≤ Metric.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]

Premises used: ENNReal.ofNNReal, Metric.infEDist_le_edist_of_mem, add_le_add, HDiv.hDiv, LT.lt.le, Metric.infEDist, HAdd.hAdd, Metric.hausdorffEDist, EDist.edist, OfNat.ofNat, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s t : Set α
Φ : α → β
h : Isometry Φ
⊢ hausdorffEDist (Φ '' s) (Φ '' t) = hausdorffEDist s t

Tactic:
simp only [hausdorffEDist_def, iSup_image, infEDist_image h]

Premises used: Metric.hausdorffEDist_def, iSup_image, Metric.infEDist_image
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
rcases : ∀ (x : α) (xs : x ∈ s), hausdorffEDist s t ≤ ediam (s ∪ t)
⊢ hausdorffEDist s t ≤ ediam (s ∪ t)

Tactic:
rcases hs with ⟨x, xs⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
ht : t.Nonempty
x : α
xs : x ∈ s
rcases : ∀ (y : α) (yt : y ∈ t), hausdorffEDist s t ≤ ediam (s ∪ t)
⊢ hausdorffEDist s t ≤ ediam (s ∪ t)

Tactic:
rcases ht with ⟨y, yt⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffEDist s t ≤ ediam (s ∪ t)

Tactic:
hausdorffEDist_le_of_mem_edist ?_ ?_

Premises used: Metric.hausdorffEDist_le_of_mem_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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)
refine_2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ediam (s ∪ t)
⊢ hausdorffEDist s t ≤ ediam (s ∪ t)

Tactic:
refine hausdorffEDist_le_of_mem_edist ?_ ?_

Premises used: Metric.hausdorffEDist_le_of_mem_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ s
⊢ ∃ y ∈ t, edist z y ≤ ediam (s ∪ t)

Tactic:
⟨y, yt, Metric.edist_le_ediam_of_mem (subset_union_left hz) (subset_union_right yt)⟩

Premises used: Set.subset_union_right, Metric.edist_le_ediam_of_mem, Set.subset_union_left, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ s
⊢ ∃ y ∈ t, edist z y ≤ ediam (s ∪ t)

Tactic:
exact ⟨y, yt, Metric.edist_le_ediam_of_mem (subset_union_left hz) (subset_union_right yt)⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ t
⊢ ∃ y ∈ s, edist z y ≤ ediam (s ∪ t)

Tactic:
⟨x, xs, Metric.edist_le_ediam_of_mem (subset_union_right hz) (subset_union_left xs)⟩

Premises used: Set.subset_union_right, Metric.edist_le_ediam_of_mem, Set.subset_union_left, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ t
⊢ ∃ y ∈ s, edist z y ≤ ediam (s ∪ t)

Tactic:
exact ⟨x, xs, Metric.edist_le_ediam_of_mem (subset_union_right hz) (subset_union_left xs)⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
rw : max (⨆ x ∈ s, infEDist x u) (⨆ y ∈ u, infEDist y s) ≤ hausdorffEDist s t + hausdorffEDist t u
⊢ hausdorffEDist s u ≤ hausdorffEDist s t + hausdorffEDist t u

Tactic:
rw [hausdorffEDist_def]

Premises used: Metric.hausdorffEDist_def
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
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
⊢ max (⨆ x ∈ s, infEDist x u) (⨆ y ∈ u, infEDist y s) ≤ hausdorffEDist s t + hausdorffEDist t u

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Premises used: sup_le_iff, iSup_le_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
left : ∀ (i : α) (i_1 : i ∈ s), infEDist i u ≤ hausdorffEDist s t + hausdorffEDist t u
right : ∀ (i : α) (i_1 : i ∈ u), infEDist i s ≤ 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

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
x : α
xs : x ∈ s
grw grw₁ : hausdorffEDist s t + hausdorffEDist t u ≤ hausdorffEDist s t + hausdorffEDist t u
⊢ infEDist x t + hausdorffEDist t u ≤ hausdorffEDist s t + hausdorffEDist t u

Tactic:
grw [infEDist_le_hausdorffEDist_of_mem xs]

Premises used: Metric.infEDist_le_hausdorffEDist_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
⊢ ∀ x ∈ s, infEDist x u ≤ hausdorffEDist s t + hausdorffEDist t u

Tactic:
exact fun x xs =>
      calc
        infEDist x u ≤ infEDist x t + hausdorffEDist t u :=
          infEDist_le_infEDist_add_hausdorffEDist
        _ ≤ hausdorffEDist s t + hausdorffEDist t u := by grw [infEDist_le_hausdorffEDist_of_mem xs]

Premises used: Trans.trans, Metric.infEDist_le_infEDist_add_hausdorffEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
x : α
xu : x ∈ u
grw grw₁ : hausdorffEDist u t + hausdorffEDist t s ≤ hausdorffEDist u t + hausdorffEDist t s
⊢ infEDist x t + hausdorffEDist t s ≤ hausdorffEDist u t + hausdorffEDist t s

Tactic:
grw [infEDist_le_hausdorffEDist_of_mem xu]

Premises used: Metric.infEDist_le_hausdorffEDist_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
x : α
xu : x ∈ u
⊢ hausdorffEDist u t + hausdorffEDist t s = hausdorffEDist s t + hausdorffEDist t u

Tactic:
simp [hausdorffEDist_comm, add_comm]

Premises used: add_comm, Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t u : Set α
⊢ ∀ x ∈ u, infEDist x s ≤ hausdorffEDist s t + hausdorffEDist t u

Tactic:
exact fun x xu =>
      calc
        infEDist x s ≤ infEDist x t + hausdorffEDist t s :=
          infEDist_le_infEDist_add_hausdorffEDist
        _ ≤ hausdorffEDist u t + hausdorffEDist t s := by grw [infEDist_le_hausdorffEDist_of_mem xu]
        _ = hausdorffEDist s t + hausdorffEDist t u := by simp [hausdorffEDist_comm, add_comm]

Premises used: Trans.trans, Metric.infEDist_le_infEDist_add_hausdorffEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist s t = 0 ↔
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
      closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
simp [hausdorffEDist_def, ← subset_def, ← mem_closure_iff_infEDist_zero,
    subset_antisymm_iff, isClosed_closure.closure_subset_iff]

Premises used: Metric.hausdorffEDist_def, Set.subset_def, Metric.mem_closure_iff_infEDist_zero, IsClosed.closure_subset_iff, subset_antisymm_iff, isClosed_closure
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
rw :
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
rw₁ rw₂ :
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0

Tactic:
rw [hausdorffEDist_zero_iff_closure_eq_closure, closure_closure]

Premises used: Metric.hausdorffEDist_zero_iff_closure_eq_closure, closure_closure
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t = hausdorffEDist s t

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
refine_1 : hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t ≤ hausdorffEDist s t
refine_2 : hausdorffEDist s t ≤ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t = hausdorffEDist s t

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t ≤
    hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) s + hausdorffEDist s t

Tactic:
hausdorffEDist_triangle

Premises used: Metric.hausdorffEDist_triangle
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) s + hausdorffEDist s t =
    hausdorffEDist s t

Tactic:
simp [hausdorffEDist_comm]

Premises used: Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
_ :
  hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) s + hausdorffEDist s t =
    hausdorffEDist s t
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t ≤ hausdorffEDist s t

Tactic:
calc
      _ ≤ hausdorffEDist (closure s) s + hausdorffEDist s t := hausdorffEDist_triangle
      _ = hausdorffEDist s t := by simp [hausdorffEDist_comm]

Premises used: closure, Metric.hausdorffEDist, Metric.hausdorffEDist_triangle
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist s t ≤
    hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) +
      hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t

Tactic:
hausdorffEDist_triangle

Premises used: Metric.hausdorffEDist_triangle
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) +
      hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t =
    hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
_ :
  hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) +
      hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t =
    hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t
⊢ hausdorffEDist 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

Premises used: closure, Metric.hausdorffEDist, Metric.hausdorffEDist_triangle
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t) = hausdorffEDist s t

Tactic:
simp [@hausdorffEDist_comm _ _ s _]

Premises used: Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t) =
    hausdorffEDist s t

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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
rw₂ rw₃ : s = t ↔ s = t
⊢ hausdorffEDist s t = 0 ↔ s = t

Tactic:
rw [hausdorffEDist_zero_iff_closure_eq_closure, hs.closure_eq, ht.closure_eq]

Premises used: IsClosed.closure_eq, Metric.hausdorffEDist_zero_iff_closure_eq_closure
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ne : s.Nonempty
rcases : ∀ (x : α) (xs : x ∈ s), hausdorffEDist s ∅ = ∞
⊢ hausdorffEDist s ∅ = ∞

Tactic:
rcases ne with ⟨x, xs⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
x : α
xs : x ∈ s
⊢ infEDist x ∅ ≤ hausdorffEDist s ∅

Tactic:
have : infEDist x ∅ ≤ hausdorffEDist s ∅ := infEDist_le_hausdorffEDist_of_mem xs
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
x : α
xs : x ∈ s
this : infEDist x ∅ ≤ hausdorffEDist s ∅
⊢ hausdorffEDist s ∅ = ∞

Tactic:
simpa using this
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : s.Nonempty
fin : hausdorffEDist s t ≠ ∞
⊢ t.Nonempty

Tactic:
t.eq_empty_or_nonempty.resolve_left fun ht ↦ fin (ht.symm ▸ hausdorffEDist_empty hs)

Premises used: Eq.rec, Or.resolve_left, Metric.hausdorffEDist_empty, Set.eq_empty_or_nonempty, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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
inr : ∀ (hs : s.Nonempty), s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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} (α := α) ∅
inl₁ : ∀ (ht : t.Nonempty), Eq.{u + 1} (α := Set α) ∅ ∅ ∧ t = ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ t.Nonempty
⊢ Eq.{u + 1} (α := Set α) ∅ ∅ ∧ t = ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ t.Nonempty

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
fin : hausdorffEDist.{u} (α := α) ∅ ∅ ≠ ∞
⊢ Eq.{u + 1} (α := Set α) ∅ ∅ ∧ Eq.{u + 1} (α := Set α) ∅ ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ Set.Nonempty.{u} (α := α) ∅

Tactic:
Or.inl ⟨rfl, rfl⟩

Premises used: And.intro, Or.inl, rfl
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
fin : hausdorffEDist.{u} (α := α) ∅ ∅ ≠ ∞
⊢ Eq.{u + 1} (α := Set α) ∅ ∅ ∧ Eq.{u + 1} (α := Set α) ∅ ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ Set.Nonempty.{u} (α := α) ∅

Tactic:
exact Or.inl ⟨rfl, rfl⟩

Premises used: Or.inl
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist ∅ t ≠ ∞
ht : t.Nonempty
⊢ hausdorffEDist t ∅ ≠ ∞

Tactic:
rw [hausdorffEDist_comm] at fin

Premises used: Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist ∅ t ≠ ∞
ht : t.Nonempty
fin₁ : hausdorffEDist t ∅ ≠ ∞
⊢ t.Nonempty

Tactic:
rw [hausdorffEDist_comm] at fin

Premises used: Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist t ∅ ≠ ∞
ht : t.Nonempty
⊢ Eq.{u + 1} (α := Set α) ∅ ∅ ∧ t = ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ t.Nonempty

Tactic:
Or.inr ⟨nonempty_of_hausdorffEDist_ne_top ht fin, ht⟩

Premises used: Metric.nonempty_of_hausdorffEDist_ne_top, And.intro, Or.inr
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist t ∅ ≠ ∞
ht : t.Nonempty
⊢ Eq.{u + 1} (α := Set α) ∅ ∅ ∧ t = ∅ ∨ Set.Nonempty.{u} (α := α) ∅ ∧ t.Nonempty

Tactic:
exact Or.inr ⟨nonempty_of_hausdorffEDist_ne_top ht fin, ht⟩

Premises used: Or.inr
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEDist s t ≠ ∞
hs : s.Nonempty
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Tactic:
Or.inr ⟨hs, nonempty_of_hausdorffEDist_ne_top hs fin⟩

Premises used: Metric.nonempty_of_hausdorffEDist_ne_top, And.intro, Or.inr
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEDist s t ≠ ∞
hs : s.Nonempty
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Tactic:
exact Or.inr ⟨hs, nonempty_of_hausdorffEDist_ne_top hs fin⟩

Premises used: Or.inr
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
simp_rw : max (edist x y) (edist y x) = edist x y
⊢ hausdorffEDist (α := α) {x} {y} = edist x y

Tactic:
simp_rw [hausdorffEDist, iSup_singleton, infEDist_singleton]

Premises used: iSup_singleton, Metric.infEDist_singleton, Metric.hausdorffEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
nth_rw : max (edist x y) (edist x y) = edist x y
⊢ max (edist x y) (edist y x) = edist x y

Tactic:
nth_rw 2 [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
⊢ max (edist x y) (edist x y) = edist x y

Tactic:
max_self _

Premises used: max_self
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
⊢ max (edist x y) (edist x y) = edist x y

Tactic:
exact max_self _

Premises used: max_self
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
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)))
⊢ hausdorffEDist.{u} (α := α) (⋃ (i : ι), s i) (⋃ (i : ι), t i) ≤ ⨆ (i : ι), hausdorffEDist (s i) (t i)

Tactic:
simp_rw [hausdorffEDist, max_le_iff, iSup_iUnion, iSup_le_iff, infEDist_iUnion]

Premises used: max_le_iff, iSup_iUnion, Metric.infEDist_iUnion, Metric.hausdorffEDist, iSup_le_iff