case intro.intro.intro.intro
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x y : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
⊢ IsMetricSeparated (s ∪ s') t
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x y : X
s' : Set X
h : IsMetricSeparated s t
h' : IsMetricSeparated s' t
⊢ IsMetricSeparated (s ∪ s') t
rcases h, h' with ⟨⟨r, r0, hr⟩, ⟨r', r0', hr'⟩⟩
case intro.intro.intro.intro.refine'_1
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x y : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
⊢ min r r' ≠ 0

case intro.intro.intro.intro.refine'_2
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x✝ y✝ : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s → min r r' ≤ edist x y

case intro.intro.intro.intro.refine'_3
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x✝ y✝ : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s' → min r r' ≤ edist x y
case intro.intro.intro.intro
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x y : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
⊢ IsMetricSeparated (s ∪ s') t
refine' ⟨min r r', _, fun x hx y hy => hx.elim _ _⟩
case intro.intro.intro.intro.refine'_1
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x y : X
s' : Set X
r : ENNReal
r0 : 0 < r
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : 0 < r'
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
⊢ 0 < min r r'
case intro.intro.intro.intro.refine'_1
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x y : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
⊢ min r r' ≠ 0
rw [← pos_iff_ne_zero] at r0 r0'⊢
no goals
case intro.intro.intro.intro.refine'_1
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x y : X
s' : Set X
r : ENNReal
r0 : 0 < r
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : 0 < r'
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
⊢ 0 < min r r'
exact lt_min r0 r0'
no goals
case intro.intro.intro.intro.refine'_2
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x✝ y✝ : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s → min r r' ≤ edist x y
exact fun hx => (min_le_left _ _).trans (hr _ hx _ hy)
no goals
case intro.intro.intro.intro.refine'_3
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x✝ y✝ : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s' → min r r' ≤ edist x y
exact fun hx => (min_le_right _ _).trans (hr' _ hx _ hy)