case intro
ι : Sort ?u.77842
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
bs : Bounded s
ht : Set.Nonempty t
bt : Bounded t
x : α
xs : x ∈ s
⊢ hausdorffDist s t ≤ diam (s ∪ t)
ι : Sort ?u.77842
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hs : Set.Nonempty s
bs : Bounded s
ht : Set.Nonempty t
bt : Bounded t
⊢ hausdorffDist s t ≤ diam (s ∪ t)
rcases hs with ⟨x, xs⟩
case intro.intro
ι : Sort ?u.77842
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
bs : Bounded s
bt : Bounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffDist s t ≤ diam (s ∪ t)
case intro
ι : Sort ?u.77842
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
bs : Bounded s
ht : Set.Nonempty t
bt : Bounded t
x : α
xs : x ∈ s
⊢ hausdorffDist s t ≤ diam (s ∪ t)
rcases ht with ⟨y, yt⟩
case intro.intro.refine_1
ι : Sort ?u.77842
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
bs : Bounded s
bt : Bounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ dist x y ≤ diam (s ∪ t)

case intro.intro.refine_2
ι : Sort ?u.77842
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
bs : Bounded s
bt : Bounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ dist x y ≤ diam (s ∪ t)
case intro.intro
ι : Sort ?u.77842
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
bs : Bounded s
bt : Bounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffDist s t ≤ diam (s ∪ t)
refine hausdorffDist_le_of_mem_dist diam_nonneg ?_ ?_
no goals
case intro.intro.refine_1
ι : Sort ?u.77842
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
bs : Bounded s
bt : Bounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ dist x y ≤ diam (s ∪ t)
exact fun z hz => ⟨y, yt,
  dist_le_diam_of_mem (bounded_union.2 ⟨bs, bt⟩) (subset_union_left _ _ hz)
    (subset_union_right _ _ yt)⟩
no goals
case intro.intro.refine_2
ι : Sort ?u.77842
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
bs : Bounded s
bt : Bounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ dist x y ≤ diam (s ∪ t)
exact fun z hz => ⟨x, xs,
  dist_le_diam_of_mem (bounded_union.2 ⟨bs, bt⟩) (subset_union_right _ _ hz)
    (subset_union_left _ _ xs)⟩