case refine_1
ι : Sort ?u.36912
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xs : x ∈ s
⊢ infEdist x t ≤ r

case refine_2
ι : Sort ?u.36912
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xt : x ∈ t
⊢ infEdist x s ≤ r
ι : Sort ?u.36912
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
⊢ hausdorffEdist s t ≤ r
refine hausdorffEdist_le_of_infEdist (fun x xs ↦ ?_) (fun x xt ↦ ?_)
case refine_1.intro.intro
ι : Sort ?u.36912
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : edist x y ≤ r
⊢ infEdist x t ≤ r
case refine_1
ι : Sort ?u.36912
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xs : x ∈ s
⊢ infEdist x t ≤ r
rcases H1 x xs with ⟨y, yt, hy⟩
no goals
case refine_1.intro.intro
ι : Sort ?u.36912
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : edist x y ≤ r
⊢ infEdist x t ≤ r
exact le_trans (infEdist_le_edist_of_mem yt) hy
case refine_2.intro.intro
ι : Sort ?u.36912
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : edist x y ≤ r
⊢ infEdist x s ≤ r
case refine_2
ι : Sort ?u.36912
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xt : x ∈ t
⊢ infEdist x s ≤ r
rcases H2 x xt with ⟨y, ys, hy⟩
no goals
case refine_2.intro.intro
ι : Sort ?u.36912
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : edist x y ≤ r
⊢ infEdist x s ≤ r
exact le_trans (infEdist_le_edist_of_mem ys) hy