awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ y ∈ s ∩ closedBall x (dist y x)

Tactic:
replace h : y ∈ s ∩ closedBall x (dist y x) := ⟨h, mem_closedBall.2 le_rfl⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
⊢ infDist x (s ∩ closedBall x (dist y x)) = infDist x s

Tactic:
le_antisymm ?_ (infDist_le_infDist_of_subset inter_subset_left ⟨y, h⟩)

Premises used: Set.inter_subset_left, Metric.infDist_le_infDist_of_subset, le_antisymm, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
refine : infDist x (s ∩ closedBall x (dist y x)) ≤ infDist x s
⊢ infDist x (s ∩ closedBall x (dist y x)) = infDist x s

Tactic:
refine le_antisymm ?_ (infDist_le_infDist_of_subset inter_subset_left ⟨y, h⟩)

Premises used: Set.inter_subset_left, Metric.infDist_le_infDist_of_subset, le_antisymm, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
⊢ infDist x (s ∩ closedBall x (dist y x)) ≤ infDist x s

Tactic:
not_lt.1 fun hlt => ?_

Premises used: not_lt, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
refine : ∀ (hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))), False
⊢ infDist x (s ∩ closedBall x (dist y x)) ≤ infDist x s

Tactic:
refine not_lt.1 fun hlt => ?_

Premises used: not_lt, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))
rcases : ∀ (z : α) (hzs : z ∈ s) (hz : dist x z < infDist x (s ∩ closedBall x (dist y x))), False
⊢ False

Tactic:
rcases (infDist_lt_iff ⟨y, h.1⟩).mp hlt with ⟨z, hzs, hz⟩

Premises used: Metric.infDist_lt_iff, And.left, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
inl : ∀ (hle : dist z x ≤ dist y x), False
inr : ∀ (hlt : dist y x < dist z x), False
⊢ False

Tactic:
rcases le_or_gt (dist z x) (dist y x) with hle | hlt

Premises used: le_or_gt, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hle : dist z x ≤ dist y x
⊢ False

Tactic:
hz.not_ge (infDist_le_dist_of_mem ⟨hzs, hle⟩)

Premises used: Metric.infDist_le_dist_of_mem, And.intro, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hle : dist z x ≤ dist y x
⊢ False

Tactic:
exact hz.not_ge (infDist_le_dist_of_mem ⟨hzs, hle⟩)

Premises used: Metric.infDist_le_dist_of_mem, And.intro, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt_1 : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hlt : dist y x < dist z x
⊢ dist x y < dist x z

Tactic:
rw [dist_comm z, dist_comm y] at hlt

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt_1 : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hlt : dist x y < dist x z
⊢ False

Tactic:
(hlt.trans hz).not_ge (infDist_le_dist_of_mem h)

Premises used: Metric.infDist_le_dist_of_mem, LT.lt.trans, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt_1 : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hlt : dist x y < dist x z
⊢ False

Tactic:
exact (hlt.trans hz).not_ge (infDist_le_dist_of_mem h)

Premises used: Metric.infDist_le_dist_of_mem, LT.lt.trans, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
h : IsCompact s
hne : s.Nonempty
x y : α
hys : y ∈ s
hy : infEDist x s = edist x y
rw : (infEDist x s).toReal = dist x y
rw₁ : (infEDist x s).toReal = (edist x y).toReal
rw₂ rw₃ : (edist x y).toReal = (edist x y).toReal
⊢ infDist x s = dist x y

Tactic:
rw [infDist, dist_edist, hy]

Premises used: Metric.infDist, dist_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hne : s.Nonempty
x : α
rcases : ∀ (z : α) (hz : z ∈ s), ∃ y ∈ s, infDist x s = dist x y
⊢ ∃ y ∈ s, infDist x s = dist x y

Tactic:
rcases hne with ⟨z, hz⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
rw : ∃ y ∈ s, infDist x (s ∩ closedBall x (dist z x)) = dist x y
⊢ ∃ y ∈ s, infDist x s = dist x y

Tactic:
rw [← infDist_inter_closedBall_of_mem hz]

Premises used: Metric.infDist_inter_closedBall_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
set :
  let t := s ∩ closedBall x (dist z x);
  ∃ y ∈ s, infDist x t = dist x y
⊢ ∃ y ∈ s, infDist x (s ∩ closedBall x (dist z x)) = dist x y

Tactic:
set t := s ∩ closedBall x (dist z x)

Premises used: Dist.dist, Metric.closedBall
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
⊢ IsCompact t

Tactic:
have htc : IsCompact t := (isCompact_closedBall x (dist z x)).inter_left h
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
⊢ t.Nonempty

Tactic:
have htne : t.Nonempty := ⟨z, hz, mem_closedBall.2 le_rfl⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : t.Nonempty
⊢ ∃ y ∈ t, infDist x t = dist x y

Tactic:
htc.exists_infDist_eq_dist htne x

Premises used: IsCompact.exists_infDist_eq_dist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : t.Nonempty
obtain : ∀ (y : α) (hyd : infDist x t = dist x y) (hys : y ∈ s), ∃ y ∈ s, infDist x t = dist x y
⊢ ∃ y ∈ s, infDist x t = dist x y

Tactic:
obtain ⟨y, ⟨hys, -⟩, hyd⟩ : ∃ y ∈ t, infDist x t = dist x y := htc.exists_infDist_eq_dist htne x

Premises used: IsCompact.exists_infDist_eq_dist, Metric.infDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : t.Nonempty
y : α
hyd : infDist x t = dist x y
hys : y ∈ s
⊢ ∃ y ∈ s, infDist x t = dist x y

Tactic:
⟨y, hys, hyd⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : t.Nonempty
y : α
hyd : infDist x t = dist x y
hys : y ∈ s
⊢ ∃ y ∈ s, infDist x t = dist x y

Tactic:
exact ⟨y, hys, hyd⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
hne : s.Nonempty
x : α
⊢ ∃ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, infDist x s = dist x y

Tactic:
simpa only [infDist_closure] using isClosed_closure.exists_infDist_eq_dist hne.closure x

Premises used: Metric.infDist_closure, Set.Nonempty.closure, IsClosed.exists_infDist_eq_dist, isClosed_closure
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ (↑(infNndist x s) : ℝ) = infDist x s

Tactic:
rfl

Premises used: Metric.infDist, ENNReal.toReal, Metric.infNndist, rfl
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ LipschitzWith (β := ℝ≥0) 1 fun (x : α) ↦ infNndist x s

Tactic:
LipschitzWith.of_le_add fun _ _ => infDist_le_infDist_add_dist

Premises used: LipschitzWith, LipschitzWith.of_le_add, ENNReal.toNNReal, Metric.infDist_le_infDist_add_dist, Metric.infNndist, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ UniformContinuous (β := ℝ≥0) fun (x : α) ↦ infNndist x s

Tactic:
(lipschitz_infNndist_pt s).uniformContinuous

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

Tactic:
(uniformContinuous_infNndist_pt s).continuous

Premises used: Metric.uniformContinuous_infNndist_pt, UniformContinuous.continuous
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
⊢ 0 ≤ hausdorffDist s t

Tactic:
simp [hausdorffDist]

Premises used: Metric.hausdorffDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
rcases : ∀ (cs : α) (hcs : cs ∈ s), hausdorffEDist s t ≠ ∞
⊢ hausdorffEDist s t ≠ ∞

Tactic:
rcases hs with ⟨cs, hcs⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
ht : t.Nonempty
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
rcases : ∀ (ct : α) (hct : ct ∈ t), hausdorffEDist s t ≠ ∞
⊢ hausdorffEDist s t ≠ ∞

Tactic:
rcases ht with ⟨ct, hct⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rcases : ∀ (rs : ℝ) (hrs : s ⊆ closedBall ct rs), hausdorffEDist s t ≠ ∞
⊢ hausdorffEDist s t ≠ ∞

Tactic:
rcases bs.subset_closedBall ct with ⟨rs, hrs⟩

Premises used: Bornology.IsBounded.subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rcases : ∀ (rt : ℝ) (hrt : t ⊆ closedBall cs rt), hausdorffEDist s t ≠ ∞
⊢ hausdorffEDist s t ≠ ∞

Tactic:
rcases bt.subset_closedBall cs with ⟨rt, hrt⟩

Premises used: Bornology.IsBounded.subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ ENNReal.ofReal (max rs rt)
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ENNReal.ofReal (max rs rt)
⊢ hausdorffEDist s t ≤ ENNReal.ofReal (max rs rt)

Tactic:
apply hausdorffEDist_le_of_mem_edist

Premises used: Metric.hausdorffEDist_le_of_mem_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
H1 : edist x ct ≤ ENNReal.ofReal (max rs rt)
⊢ ∃ y ∈ t, edist x y ≤ ENNReal.ofReal (max rs rt)

Tactic:
exists ct, hct
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
⊢ dist x ct ≤ max rs rt

Tactic:
have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _)
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
this : dist x ct ≤ max rs rt
H1 : 0 ≤ max rs rt
⊢ edist x ct ≤ ENNReal.ofReal (max rs rt)

Tactic:
rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]

Premises used: ENNReal.ofReal_le_ofReal_iff, edist_dist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
this : dist x ct ≤ max rs rt
⊢ 0 ≤ max rs rt

Tactic:
le_trans dist_nonneg this

Premises used: dist_nonneg, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
this : dist x ct ≤ max rs rt
⊢ 0 ≤ max rs rt

Tactic:
exact le_trans dist_nonneg this

Premises used: dist_nonneg, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
H2 : edist x cs ≤ ENNReal.ofReal (max rs rt)
⊢ ∃ y ∈ s, edist x y ≤ ENNReal.ofReal (max rs rt)

Tactic:
exists cs, hcs
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
⊢ dist x cs ≤ max rs rt

Tactic:
have : dist x cs ≤ max rs rt := le_trans (hrt xt) (le_max_right _ _)
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
this : dist x cs ≤ max rs rt
H2 : 0 ≤ max rs rt
⊢ edist x cs ≤ ENNReal.ofReal (max rs rt)

Tactic:
rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]

Premises used: ENNReal.ofReal_le_ofReal_iff, edist_dist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
this : dist x cs ≤ max rs rt
⊢ 0 ≤ max rs rt

Tactic:
le_trans dist_nonneg this

Premises used: dist_nonneg, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
this : dist x cs ≤ max rs rt
⊢ 0 ≤ max rs rt

Tactic:
exact le_trans dist_nonneg this

Premises used: dist_nonneg, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ hausdorffEDist s t ≤ ENNReal.ofReal (max rs rt)

Tactic:
have : hausdorffEDist s t ≤ ENNReal.ofReal (max rs rt) := by
    apply hausdorffEDist_le_of_mem_edist
    · intro x xs
      exists ct, hct
      have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _)
      rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
      exact le_trans dist_nonneg this
    · intro x xt
      exists cs, hcs
      have : dist x cs ≤ max rs rt := le_trans (hrt xt) (le_max_right _ _)
      rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
      exact le_trans dist_nonneg this
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
this : hausdorffEDist s t ≤ ENNReal.ofReal (max rs rt)
⊢ hausdorffEDist s t ≠ ∞

Tactic:
ne_top_of_le_ne_top ENNReal.ofReal_ne_top this

Premises used: ne_top_of_le_ne_top, ENNReal.ofReal_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
this : hausdorffEDist s t ≤ ENNReal.ofReal (max rs rt)
⊢ hausdorffEDist s t ≠ ∞

Tactic:
exact ne_top_of_le_ne_top ENNReal.ofReal_ne_top this

Premises used: ne_top_of_le_ne_top, ENNReal.ofReal_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ hausdorffDist s s = 0

Tactic:
simp [hausdorffDist]

Premises used: Metric.hausdorffDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
⊢ hausdorffDist s t = hausdorffDist t s

Tactic:
simp [hausdorffDist, hausdorffEDist_comm]

Premises used: Metric.hausdorffDist, Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inl : ∀ (h : s = ∅), hausdorffDist s ∅ = 0
inr : ∀ (h : s.Nonempty), hausdorffDist s ∅ = 0
⊢ hausdorffDist s ∅ = 0

Tactic:
rcases s.eq_empty_or_nonempty with h | h

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
h : s = ∅
⊢ hausdorffDist s ∅ = 0

Tactic:
simp [h]
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
h : s.Nonempty
⊢ hausdorffDist s ∅ = 0

Tactic:
simp [hausdorffDist, hausdorffEDist_empty h]

Premises used: Metric.hausdorffDist, Metric.hausdorffEDist_empty
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ hausdorffDist ∅ s = 0

Tactic:
simp [hausdorffDist_comm]

Premises used: Metric.hausdorffDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
inl :
  ∀ (H1 : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → infDist x t ≤ r) (H2 : ∀ x ∈ t, infDist x ∅ ≤ r),
    hausdorffDist ∅ t ≤ r
inr : ∀ (hs : s.Nonempty), hausdorffDist s t ≤ r
⊢ hausdorffDist s t ≤ r

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 α
t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x ∅ ≤ r
inl inl₁ inl₂ inl₃ : 0 ≤ r
⊢ hausdorffDist ∅ t ≤ r

Tactic:
rwa [hausdorffDist_empty']

Premises used: Metric.hausdorffDist_empty'
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
inr :
  ∀ (H1 : ∀ x ∈ s, infDist x ∅ ≤ r) (H2 : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → infDist x s ≤ r),
    hausdorffDist s ∅ ≤ r
inr₁ : ∀ (ht : t.Nonempty), hausdorffDist s t ≤ r
⊢ hausdorffDist s t ≤ r

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 : PseudoMetricSpace α
s : Set α
r : ℝ
hr : 0 ≤ r
hs : s.Nonempty
H1 : ∀ x ∈ s, infDist x ∅ ≤ r
H2 : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → infDist x s ≤ r
inr inr₁ inr₂ inr₃ : 0 ≤ r
⊢ hausdorffDist s ∅ ≤ r

Tactic:
rwa [hausdorffDist_empty]

Premises used: Metric.hausdorffDist_empty
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
apply : ∀ x ∈ s, infEDist x t ≤ ENNReal.ofReal r
apply₁ : ∀ x ∈ t, infEDist x s ≤ ENNReal.ofReal r
⊢ hausdorffEDist s t ≤ ENNReal.ofReal r

Tactic:
apply hausdorffEDist_le_of_infEDist _ _

Premises used: Metric.hausdorffEDist_le_of_infEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ s, infEDist x t ≤ ENNReal.ofReal r

Tactic:
simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEDist_ne_top ht) hr] using H1

Premises used: Metric.infDist, Metric.infEDist_ne_top, ENNReal.le_ofReal_iff_toReal_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ t, infEDist x s ≤ ENNReal.ofReal r

Tactic:
simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEDist_ne_top hs) hr] using H2

Premises used: Metric.infDist, Metric.infEDist_ne_top, ENNReal.le_ofReal_iff_toReal_le
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ hausdorffEDist s t ≤ ENNReal.ofReal r

Tactic:
have : hausdorffEDist s t ≤ ENNReal.ofReal r := by
    apply hausdorffEDist_le_of_infEDist _ _
    · simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEDist_ne_top ht) hr] using H1
    · simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEDist_ne_top hs) hr] using H2