awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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)))
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)))
⊢ (∀ (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:
constructor
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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)))

Tactic:
fun i x hx => (iInf_le _ i).trans <| le_iSup_of_le i ?_

Premises used: Metric.infEDist, le_iSup_of_le, LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
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))
⊢ ∀ (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:
refine fun i x hx => (iInf_le _ i).trans <| le_iSup_of_le i ?_

Premises used: le_iSup_of_le, LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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)))

Tactic:
fun i x hx => (iInf_le _ i).trans <| le_iSup_of_le i ?_

Premises used: Metric.infEDist, le_iSup_of_le, LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
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))
⊢ ∀ (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:
refine fun i x hx => (iInf_le _ i).trans <| le_iSup_of_le i ?_

Premises used: le_iSup_of_le, LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
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:
le_max_of_le_left <| le_iSup₂_of_le x hx le_rfl

Premises used: le_rfl, le_max_of_le_left, le_iSup₂_of_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
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:
exact le_max_of_le_left <| le_iSup₂_of_le x hx le_rfl

Premises used: le_rfl, le_max_of_le_left, le_iSup₂_of_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
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:
le_max_of_le_right <| le_iSup₂_of_le x hx le_rfl

Premises used: le_rfl, le_max_of_le_right, le_iSup₂_of_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
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:
exact le_max_of_le_right <| le_iSup₂_of_le x hx le_rfl

Premises used: le_rfl, le_max_of_le_right, le_iSup₂_of_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s₁ s₂ t₁ t₂ : Set α
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₂
⊢ hausdorffEDist (s₁ ∪ s₂) (t₁ ∪ t₂) ≤ max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂)

Tactic:
simp_rw [union_eq_iUnion, sup_eq_iSup]

Premises used: sup_eq_iSup, Set.union_eq_iUnion
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s₁ s₂ t₁ t₂ : Set α
⊢ hausdorffEDist.{u} (α := α) (⋃ (i : Bool), bif i then s₁ else s₂) (⋃ (i : Bool), bif i then t₁ else t₂) ≤
    ⨆ (i : Bool), hausdorffEDist (bif i then s₁ else s₂) (bif i then t₁ else t₂)

Tactic:
hausdorffEDist_iUnion_le

Premises used: Metric.hausdorffEDist_iUnion_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s₁ s₂ t₁ t₂ : Set α
⊢ 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:
convert! hausdorffEDist_iUnion_le with (_ | _)

Premises used: Metric.hausdorffEDist_iUnion_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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₂)

Tactic:
le_of_forall_ge fun _ _ => ?_

Premises used: le_of_forall_ge
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s₁ t₁ : Set α
s₂ t₂ : Set β
refine : ∀ (x : ℝ≥0∞), max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂) ≤ x → hausdorffEDist (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) ≤ x
⊢ hausdorffEDist (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) ≤ max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂)

Tactic:
refine le_of_forall_ge fun _ _ => ?_

Premises used: le_of_forall_ge
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s₁ t₁ : Set α
s₂ t₂ : Set β
x : ℝ≥0∞
h : max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂) ≤ x
⊢ hausdorffEDist (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) ≤ x

Tactic:
simp_all only [hausdorffEDist, infEDist_prod, max_le_iff, iSup_le_iff, mem_prod, true_and,
    implies_true]

Premises used: max_le_iff, Set.mem_prod, Metric.infEDist_prod, Metric.hausdorffEDist, implies_true, iSup_le_iff, true_and
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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 : α))
rw₁ : ∀ (i : Subtype (Membership.mem s)), edist x (↑i : α) ≠ ∞
⊢ infDist x s = ⨅ (y : (↑s : Type u)), dist x (↑y : α)

Tactic:
rw [infDist, infEDist, iInf_subtype', ENNReal.toReal_iInf]

Premises used: Metric.infDist, iInf_subtype', Metric.infEDist, ENNReal.toReal_iInf
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ Eq (α := ℝ) (⨅ (i : Subtype (Membership.mem s)), (edist x (↑i : α)).toReal) (⨅ (y : (↑s : Type u)), dist x (↑y : α))

Tactic:
simp only [dist_edist]

Premises used: dist_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ ∀ (i : Subtype (Membership.mem s)), edist x (↑i : α) ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ 0 ≤ infDist x s

Tactic:
toReal_nonneg

Premises used: Metric.infDist, ENNReal.toReal_nonneg
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ infDist x ∅ = 0

Tactic:
simp [infDist]

Premises used: Metric.infDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
hs : s.Nonempty
⊢ Membership.mem (γ := Set ℝ) (lowerBounds ((fun (x_1 : α) ↦ dist x x_1) '' s)) 0

Tactic:
simp [lowerBounds]

Premises used: lowerBounds
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
hs : s.Nonempty
⊢ IsGLB ((fun (x_1 : α) ↦ dist x x_1) '' s) (infDist x s)

Tactic:
simpa [infDist_eq_iInf, sInf_image']
    using isGLB_csInf (hs.image _) ⟨0, by simp [lowerBounds]⟩

Premises used: isGLB_csInf, Set.Nonempty.image, Exists.intro, sInf_image', Metric.infDist_eq_iInf, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : s.Nonempty
rcases : ∀ (y : α) (hy : y ∈ s), infEDist x s ≠ ∞
⊢ infEDist x s ≠ ∞

Tactic:
rcases h with ⟨y, hy⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
hy : y ∈ s
⊢ infEDist x s ≠ ∞

Tactic:
ne_top_of_le_ne_top (edist_ne_top _ _) (infEDist_le_edist_of_mem hy)

Premises used: Metric.infEDist_le_edist_of_mem, ne_top_of_le_ne_top, edist_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
hy : y ∈ s
⊢ infEDist x s ≠ ∞

Tactic:
exact ne_top_of_le_ne_top (edist_ne_top _ _) (infEDist_le_edist_of_mem hy)

Premises used: Metric.infEDist_le_edist_of_mem, ne_top_of_le_ne_top, edist_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
inl : infEDist x ∅ = ∞ ↔ Eq.{u + 1} (α := Set α) ∅ ∅
inr : ∀ (hs : s.Nonempty), infEDist x s = ∞ ↔ s = ∅
⊢ infEDist x s = ∞ ↔ s = ∅

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 : PseudoMetricSpace α
x : α
⊢ infEDist x ∅ = ∞ ↔ Eq.{u + 1} (α := Set α) ∅ ∅

Tactic:
simp [*, Nonempty.ne_empty, infEDist_ne_top]

Premises used: Set.Nonempty.ne_empty, Metric.infEDist_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
hs : s.Nonempty
⊢ infEDist x s = ∞ ↔ s = ∅

Tactic:
simp [*, Nonempty.ne_empty, infEDist_ne_top]

Premises used: Set.Nonempty.ne_empty, Metric.infEDist_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : x ∈ s
⊢ infDist x s = 0

Tactic:
simp [infEDist_zero_of_mem h, infDist]

Premises used: Metric.infDist, Metric.infEDist_zero_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ infDist x {y} = dist x y

Tactic:
simp [infDist, dist_edist]

Premises used: Metric.infDist, dist_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
rw : (infEDist x s).toReal ≤ (edist x y).toReal
⊢ infDist x s ≤ dist x y

Tactic:
rw [dist_edist, infDist]

Premises used: Metric.infDist, dist_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ (infEDist x s).toReal ≤ (edist x y).toReal

Tactic:
ENNReal.toReal_mono (edist_ne_top _ _) (infEDist_le_edist_of_mem h)

Premises used: Metric.infEDist_le_edist_of_mem, edist_ne_top, ENNReal.toReal_mono
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ (infEDist x s).toReal ≤ (edist x y).toReal

Tactic:
exact ENNReal.toReal_mono (edist_ne_top _ _) (infEDist_le_edist_of_mem h)

Premises used: Metric.infEDist_le_edist_of_mem, edist_ne_top, ENNReal.toReal_mono
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
h : s ⊆ t
hs : s.Nonempty
⊢ infDist x t ≤ infDist x s

Tactic:
ENNReal.toReal_mono (infEDist_ne_top hs) (infEDist_anti h)

Premises used: Metric.infDist, Metric.infEDist_ne_top, Metric.infEDist_anti, ENNReal.toReal_mono
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
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
simp_rw₁ : ENNReal.ofReal r ≤ infEDist x s ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
simp_rw₂ : (∀ y ∈ s, ENNReal.ofReal r ≤ edist x y) ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
simp_rw₃ : (∀ y ∈ s, r ≤ (edist x y).toReal) ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
⊢ r ≤ infDist 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]

Premises used: ENNReal.ofReal_le_iff_le_toReal, Metric.infDist, Metric.infEDist_ne_top, Metric.le_infEDist, edist_ne_top, dist_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hs : s.Nonempty
⊢ infDist x s < r ↔ ∃ y ∈ s, dist x y < r

Tactic:
simp [← not_le, le_infDist hs]

Premises used: not_le, Metric.le_infDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
rw : (infEDist x s).toReal ≤ (infEDist y s).toReal + (edist x y).toReal
⊢ infDist x s ≤ infDist y s + dist x y

Tactic:
rw [infDist, infDist, dist_edist]

Premises used: Metric.infDist, dist_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
⊢ (infEDist x s).toReal ≤ (infEDist y s).toReal + (edist x y).toReal

Tactic:
ENNReal.toReal_le_add' infEDist_le_infEDist_add_edist ?_ (flip absurd (edist_ne_top _ _))

Premises used: Metric.infEDist_le_infEDist_add_edist, flip, absurd, edist_ne_top, ENNReal.toReal_le_add'
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
refine : infEDist y s = ∞ → infEDist x s = ∞
⊢ (infEDist x s).toReal ≤ (infEDist y s).toReal + (edist x y).toReal

Tactic:
refine ENNReal.toReal_le_add' infEDist_le_infEDist_add_edist ?_ (flip absurd (edist_ne_top _ _))

Premises used: Metric.infEDist_le_infEDist_add_edist, flip, absurd, ENNReal.toReal_le_add'
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
⊢ infEDist y s = ∞ → infEDist x s = ∞

Tactic:
simp only [infEDist_eq_top_iff, imp_self]

Premises used: imp_self, Metric.infEDist_eq_top_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : dist x y < infDist x s
⊢ y ∉ s

Tactic:
fun hy =>
  h.not_ge <| infDist_le_dist_of_mem hy

Premises used: Metric.infDist_le_dist_of_mem, LT.lt.not_ge, Not
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ Disjoint (ball x (infDist x s)) s

Tactic:
disjoint_left.2 fun _y hy => notMem_of_dist_lt_infDist <| mem_ball'.1 hy

Premises used: Iff.mpr, Set.disjoint_left, Metric.notMem_of_dist_lt_infDist, Iff.mp, Metric.mem_ball'
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ ball x (infDist x s) ⊆ sᶜ

Tactic:
(disjoint_ball_infDist (s := s)).subset_compl_right

Premises used: Metric.disjoint_ball_infDist, Disjoint.subset_compl_right
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ ball x (infDist x sᶜ) ⊆ s

Tactic:
ball_infDist_subset_compl.trans_eq (compl_compl s)

Premises used: LE.le.trans_eq, compl_compl, Metric.ball_infDist_subset_compl
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
h : r < infDist x s
⊢ Disjoint (closedBall x r) s

Tactic:
disjoint_ball_infDist.mono_left <| closedBall_subset_ball h

Premises used: Metric.disjoint_ball_infDist, Metric.closedBall_subset_ball, Disjoint.mono_left
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
hs : Bornology.IsBounded s
hy : y ∈ s
rw : (edist x y).toReal ≤ (infEDist x s).toReal + (ediam s).toReal
⊢ dist x y ≤ infDist x s + diam s

Tactic:
rw [infDist, diam, dist_edist]

Premises used: Metric.infDist, Metric.diam, dist_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
hs : Bornology.IsBounded s
hy : y ∈ s
⊢ (edist x y).toReal ≤ (infEDist x s).toReal + (ediam s).toReal

Tactic:
toReal_le_add (edist_le_infEDist_add_ediam hy) (infEDist_ne_top ⟨y, hy⟩) hs.ediam_ne_top

Premises used: Metric.infEDist_ne_top, Metric.edist_le_infEDist_add_ediam, Bornology.IsBounded.ediam_ne_top, Exists.intro, ENNReal.toReal_le_add
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
hs : Bornology.IsBounded s
hy : y ∈ s
⊢ (edist x y).toReal ≤ (infEDist x s).toReal + (ediam s).toReal

Tactic:
exact toReal_le_add (edist_le_infEDist_add_ediam hy) (infEDist_ne_top ⟨y, hy⟩) hs.ediam_ne_top

Premises used: Metric.infEDist_ne_top, Metric.edist_le_infEDist_add_ediam, Bornology.IsBounded.ediam_ne_top, Exists.intro, ENNReal.toReal_le_add
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ LipschitzWith (β := ℝ) 1 fun (x : α) ↦ infDist x s

Tactic:
LipschitzWith.of_le_add fun _ _ => infDist_le_infDist_add_dist

Premises used: LipschitzWith.of_le_add, Metric.infDist_le_infDist_add_dist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ UniformContinuous (β := ℝ) fun (x : α) ↦ infDist x s

Tactic:
(lipschitz_infDist_pt s).uniformContinuous

Premises used: LipschitzWith.uniformContinuous, Metric.lipschitz_infDist_pt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : α) ↦ infDist x s

Tactic:
(uniformContinuous_infDist_pt s).continuous

Premises used: UniformContinuous.continuous, Metric.uniformContinuous_infDist_pt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) = infDist x s

Tactic:
simp [infDist, infEDist_closure]

Premises used: Metric.infDist, Metric.infEDist_closure
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rw : infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0
⊢ infDist x s = 0

Tactic:
rw [← infDist_closure]

Premises used: Metric.infDist_closure
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0

Tactic:
infDist_zero_of_mem hx

Premises used: Metric.infDist_zero_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0

Tactic:
exact infDist_zero_of_mem hx

Premises used: Metric.infDist_zero_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : s.Nonempty
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ infDist x s = 0

Tactic:
simp [mem_closure_iff_infEDist_zero, infDist, ENNReal.toReal_eq_zero_iff, infEDist_ne_top h]

Premises used: Metric.infDist, Metric.infEDist_ne_top, Metric.mem_closure_iff_infEDist_zero, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
hs : s.Nonempty
⊢ x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ 0 < infDist x s

Tactic:
(mem_closure_iff_infDist_zero hs).not.trans infDist_nonneg.lt_iff_ne'.symm

Premises used: Metric.mem_closure_iff_infDist_zero, Iff.not, Iff.trans, LE.le.lt_iff_ne', Iff.symm, Metric.infDist_nonneg
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
rw : x ∈ s ↔ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rw₁ rw₂ : x ∈ s ↔ x ∈ s
⊢ x ∈ s ↔ infDist x s = 0

Tactic:
rw [← mem_closure_iff_infDist_zero hs, h.closure_eq]

Premises used: Metric.mem_closure_iff_infDist_zero, IsClosed.closure_eq
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ x ∉ s ↔ 0 < infDist x s

Tactic:
simp [h.mem_iff_infDist_zero hs, infDist_nonneg.lt_iff_ne']

Premises used: IsClosed.mem_iff_infDist_zero, LE.le.lt_iff_ne', Metric.infDist_nonneg
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
inl :
  ∀ (h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅),
    ContinuousAt (Y := ℝ) (fun (x : α) ↦ (infDist x ∅)⁻¹) x
inr : ∀ (hs : s.Nonempty), ContinuousAt (Y := ℝ) (fun (x : α) ↦ (infDist x s)⁻¹) x
⊢ ContinuousAt (Y := ℝ) (fun (x : α) ↦ (infDist x s)⁻¹) x

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 : PseudoMetricSpace α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
⊢ ContinuousAt (Y := ℝ) (fun (x : α) ↦ (infDist x ∅)⁻¹) x

Tactic:
simp only [infDist_empty, continuousAt_const]

Premises used: Metric.infDist_empty, continuousAt_const
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ ContinuousAt (Y := ℝ) (fun (x : α) ↦ (infDist x s)⁻¹) x

Tactic:
(continuous_infDist_pt s).continuousAt.inv₀ ?_

Premises used: Continuous.continuousAt, ContinuousAt.inv₀, Metric.continuous_infDist_pt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
inr : infDist x s ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : α) ↦ (infDist x s)⁻¹) x

Tactic:
refine (continuous_infDist_pt s).continuousAt.inv₀ ?_

Premises used: Continuous.continuousAt, ContinuousAt.inv₀, Metric.continuous_infDist_pt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
inr : ¬infDist x s = 0
inr₁ inr₂ inr₃ inr₄ : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ infDist x s ≠ 0

Tactic:
rwa [Ne, ← mem_closure_iff_infDist_zero hs]

Premises used: Metric.mem_closure_iff_infDist_zero, Ne
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
t : Set α
x : α
Φ : α → β
hΦ : Isometry Φ
⊢ infDist (Φ x) (Φ '' t) = infDist x t

Tactic:
simp [infDist, infEDist_image hΦ]

Premises used: Metric.infDist, Metric.infEDist_image