awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
simp_rw₁ : ENNReal.ofReal r ≤ infEDist x s ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
⊢ r ≤ infDist x s ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
have simp_rw₂ : (∀ y ∈ s, ENNReal.ofReal r ≤ edist x y) ↔ ∀ ⦃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
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
⊢ r ≤ infDist x s ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
have simp_rw₃ : (∀ y ∈ s, r ≤ (edist x y).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 y : α
⊢ infDist x s ≤ infDist y s + dist x y
have rw : (infEDist x s).toReal ≤ (infEDist y s).toReal + (edist x y).toReal
Tactic: rw [infDist, infDist, dist_edist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
⊢ (infEDist x s).toReal ≤ (infEDist y s).toReal + (edist x y).toReal
have refine : infEDist y s = ∞ → infEDist x s = ∞
Tactic: refine ENNReal.toReal_le_add' infEDist_le_infEDist_add_edist ?_ (flip absurd (edist_ne_top _ _))
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
hs : Bornology.IsBounded s
hy : y ∈ s
⊢ dist x y ≤ infDist x s + diam s
have rw : (edist x y).toReal ≤ (infEDist x s).toReal + (ediam s).toReal
Tactic: rw [infDist, diam, dist_edist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ infDist x s = 0
have rw : infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0
Tactic: rw [← infDist_closure]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ x ∈ s ↔ infDist x s = 0
have rw : x ∈ s ↔ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: rw [← mem_closure_iff_infDist_zero hs, h.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ x ∈ s ↔ infDist x s = 0
have rw₁ : x ∈ s ↔ x ∈ s
Tactic: rw [← mem_closure_iff_infDist_zero hs, h.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContinuousAt (Y := ℝ) (fun (x : α) ↦ (infDist x s)⁻¹) x
have inl : ∀ (h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅),
  ContinuousAt (Y := ℝ) (fun (x : α) ↦ (infDist x ∅)⁻¹) x
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ ContinuousAt (Y := ℝ) (fun (x : α) ↦ (infDist x s)⁻¹) x
have inr : ∀ (hs : s.Nonempty), ContinuousAt (Y := ℝ) (fun (x : α) ↦ (infDist x s)⁻¹) x
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 : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ ContinuousAt (Y := ℝ) (fun (x : α) ↦ (infDist x s)⁻¹) x
have inr : infDist x s ≠ 0
Tactic: refine (continuous_infDist_pt s).continuousAt.inv₀ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ infDist x s ≠ 0
have inr : ¬infDist x s = 0
Tactic: rwa [Ne, ← mem_closure_iff_infDist_zero hs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ infDist x (s ∩ closedBall x (dist y x)) = infDist x s
have h₁ : y ∈ s ∩ closedBall x (dist y x)
Tactic: replace h : y ∈ s ∩ closedBall x (dist y x) := ⟨h, mem_closedBall.2 le_rfl⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
have refine : 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⟩)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
have refine : ∀ (hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))), False
Tactic: refine not_lt.1 fun hlt => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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))
⊢ False
have rcases : ∀ (z : α) (hzs : z ∈ s) (hz : dist x z < infDist x (s ∩ closedBall x (dist y x))), False
Tactic: rcases (infDist_lt_iff ⟨y, h.1⟩).mp hlt with ⟨z, hzs, hz⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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))
⊢ False
have inl : ∀ (hle : dist z x ≤ dist y x), False
Tactic: rcases le_or_gt (dist z x) (dist y x) with hle | hlt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ False
have inr : ∀ (hlt : dist y x < dist z x), False
Tactic: rcases le_or_gt (dist z x) (dist y x) with hle | hlt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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
⊢ False
have hlt₁ : dist x y < dist x z
Tactic: rw [dist_comm z, dist_comm y] at hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ infDist x s = dist x y
have rw : (infEDist x s).toReal = dist x y
Tactic: rw [infDist, dist_edist, hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ infDist x s = dist x y
have rw₁ : (infEDist x s).toReal = (edist x y).toReal
Tactic: rw [infDist, dist_edist, hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ infDist x s = dist x y
have rw₂ : (edist x y).toReal = (edist x y).toReal
Tactic: rw [infDist, dist_edist, hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hne : s.Nonempty
x : α
⊢ ∃ y ∈ s, infDist x s = dist x y
have rcases : ∀ (z : α) (hz : z ∈ s), ∃ y ∈ s, infDist x s = dist x y
Tactic: rcases hne with ⟨z, hz⟩
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inst_1 : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
⊢ ∃ y ∈ s, infDist x s = dist x y
have rw : ∃ y ∈ s, infDist x (s ∩ closedBall x (dist z x)) = dist x y
Tactic: rw [← infDist_inter_closedBall_of_mem hz]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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)
⊢ ∃ y ∈ s, infDist x t = dist x y
have htc : IsCompact t
Tactic: have htc : IsCompact t := (isCompact_closedBall x (dist z x)).inter_left h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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
⊢ ∃ y ∈ s, infDist x t = dist x y
have htne : t.Nonempty
Tactic: have htne : t.Nonempty := ⟨z, hz, mem_closedBall.2 le_rfl⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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 ∈ s, infDist x t = dist x y
have obtain : ∀ (y : α) (hyd : infDist x t = dist x y) (hys : y ∈ s), ∃ 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
⊢ hausdorffEDist s t ≠ ∞
have rcases : ∀ (cs : α) (hcs : cs ∈ s), hausdorffEDist s t ≠ ∞
Tactic: rcases hs with ⟨cs, hcs⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
ht : t.Nonempty
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
⊢ hausdorffEDist s t ≠ ∞
have rcases : ∀ (ct : α) (hct : ct ∈ t), hausdorffEDist s t ≠ ∞
Tactic: rcases ht with ⟨ct, hct⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
⊢ hausdorffEDist s t ≠ ∞
have rcases : ∀ (rs : ℝ) (hrs : s ⊆ closedBall ct rs), hausdorffEDist s t ≠ ∞
Tactic: rcases bs.subset_closedBall ct with ⟨rs, hrs⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ hausdorffEDist s t ≠ ∞
have rcases : ∀ (rt : ℝ) (hrt : t ⊆ closedBall cs rt), hausdorffEDist s t ≠ ∞
Tactic: rcases bt.subset_closedBall cs with ⟨rt, hrt⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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)
have H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ ENNReal.ofReal (max rs rt)
Tactic: apply hausdorffEDist_le_of_mem_edist
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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)
⊢ hausdorffEDist s t ≤ ENNReal.ofReal (max rs rt)
have H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ENNReal.ofReal (max rs rt)
Tactic: apply hausdorffEDist_le_of_mem_edist
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ ∃ y ∈ t, edist x y ≤ ENNReal.ofReal (max rs rt)
have H1 : edist x ct ≤ ENNReal.ofReal (max rs rt)
Tactic: exists ct, hct
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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
⊢ edist x ct ≤ ENNReal.ofReal (max rs rt)
have this : dist x ct ≤ max rs rt
Tactic: have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ edist x ct ≤ ENNReal.ofReal (max rs rt)
have H1 : 0 ≤ max rs rt
Tactic: rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ ∃ y ∈ s, edist x y ≤ ENNReal.ofReal (max rs rt)
have H2 : edist x cs ≤ ENNReal.ofReal (max rs rt)
Tactic: exists cs, hcs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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
⊢ edist x cs ≤ ENNReal.ofReal (max rs rt)
have this : dist x cs ≤ max rs rt
Tactic: have : dist x cs ≤ max rs rt := le_trans (hrt xt) (le_max_right _ _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ edist x cs ≤ ENNReal.ofReal (max rs rt)
have H2 : 0 ≤ max rs rt
Tactic: rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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 ≠ ∞
have this : 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ hausdorffDist s ∅ = 0
have inl : ∀ (h : s = ∅), hausdorffDist s ∅ = 0
Tactic: rcases s.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
inl : ∀ (h : s = ∅), hausdorffDist s ∅ = 0
⊢ hausdorffDist s ∅ = 0
have inr : ∀ (h : s.Nonempty), hausdorffDist s ∅ = 0
Tactic: rcases s.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ hausdorffDist s t ≤ r
have inl : ∀ (H1 : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → infDist x t ≤ r) (H2 : ∀ x ∈ t, infDist x ∅ ≤ r),
  hausdorffDist ∅ t ≤ r
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s, H1, H2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ hausdorffDist s t ≤ r
have inr : ∀ (hs : s.Nonempty), hausdorffDist s t ≤ r
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 t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
⊢ hausdorffDist s t ≤ r
have inr : ∀ (H1 : ∀ x ∈ s, infDist x ∅ ≤ r) (H2 : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → infDist x s ≤ r),
  hausdorffDist s ∅ ≤ r
Tactic: rcases t.eq_empty_or_nonempty with rfl | ht
Cleared hypotheses: t, H1, H2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ hausdorffDist s t ≤ r
have inr₁ : ∀ (ht : t.Nonempty), hausdorffDist s t ≤ r
Tactic: rcases t.eq_empty_or_nonempty with rfl | ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
have apply : ∀ x ∈ s, infEDist x t ≤ ENNReal.ofReal r
Tactic: apply hausdorffEDist_le_of_infEDist _ _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ hausdorffEDist s t ≤ ENNReal.ofReal r
have apply₁ : ∀ x ∈ t, infEDist x s ≤ ENNReal.ofReal r
Tactic: apply hausdorffEDist_le_of_infEDist _ _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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
⊢ hausdorffDist s t ≤ r
have this : 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
⊢ hausdorffDist s t ≤ r
have H1₁ : ∀ x ∈ s, infDist x t ≤ r
Tactic: apply hausdorffDist_le_of_infDist hr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
H1₁ : ∀ x ∈ s, infDist x t ≤ r
⊢ hausdorffDist s t ≤ r
have H2₁ : ∀ x ∈ t, infDist x s ≤ r
Tactic: apply hausdorffDist_le_of_infDist hr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xs : x ∈ s
⊢ infDist x t ≤ r
have H1₁ : ∀ (y : α) (yt : y ∈ t) (hy : dist x y ≤ r), infDist x t ≤ r
Tactic: rcases H1 x xs with ⟨y, yt, hy⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xt : x ∈ t
⊢ infDist x s ≤ r
have H2₁ : ∀ (y : α) (ys : y ∈ s) (hy : dist x y ≤ r), infDist x s ≤ r
Tactic: rcases H2 x xt with ⟨y, ys, hy⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
hs : s.Nonempty
bs : Bornology.IsBounded s
ht : t.Nonempty
bt : Bornology.IsBounded t
⊢ hausdorffDist s t ≤ diam (s ∪ t)
have rcases : ∀ (x : α) (xs : x ∈ s), hausdorffDist s t ≤ diam (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 : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
ht : t.Nonempty
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
⊢ hausdorffDist s t ≤ diam (s ∪ t)
have rcases : ∀ (y : α) (yt : y ∈ t), hausdorffDist s t ≤ diam (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 : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffDist s t ≤ diam (s ∪ t)
have refine_1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ diam (s ∪ t)
Tactic: refine hausdorffDist_le_of_mem_dist diam_nonneg ?_ ?_