ι : Sort ?u.78581
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
⊢ ∃ y, y ∈ t ∧ dist x y < r
ι : Sort ?u.78581
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
⊢ ∃ y, y ∈ t ∧ dist x y < r
have r0 : 0 < r := lt_of_le_of_lt hausdorffDist_nonneg H
ι : Sort ?u.78581
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
⊢ ∃ y, y ∈ t ∧ dist x y < r
ι : Sort ?u.78581
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
⊢ ∃ y, y ∈ t ∧ dist x y < r
have : hausdorffEdist s t < ENNReal.ofReal r := by
  rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
    ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H
case intro.intro
ι : Sort ?u.78581
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y✝ : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : edist x y < ENNReal.ofReal r
⊢ ∃ y, y ∈ t ∧ dist x y < r
ι : Sort ?u.78581
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
⊢ ∃ y, y ∈ t ∧ dist x y < r
rcases exists_edist_lt_of_hausdorffEdist_lt h this with ⟨y, hy, yr⟩
case intro.intro
ι : Sort ?u.78581
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y✝ : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : dist x y < r
⊢ ∃ y, y ∈ t ∧ dist x y < r
case intro.intro
ι : Sort ?u.78581
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y✝ : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : edist x y < ENNReal.ofReal r
⊢ ∃ y, y ∈ t ∧ dist x y < r
rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff r0] at yr
no goals
case intro.intro
ι : Sort ?u.78581
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y✝ : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : dist x y < r
⊢ ∃ y, y ∈ t ∧ dist x y < r
exact ⟨y, hy, yr⟩
no goals
ι : Sort ?u.78581
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
⊢ hausdorffEdist s t < ENNReal.ofReal r
rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
  ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H