-- Mathlib/Topology/MetricSpace/MetricSeparated.lean
theorem union_left {s'} (h : AreSeparated s t) (h' : AreSeparated s' t) :
    AreSeparated (s ∪ s') t

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝ : EMetricSpace X
s t s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ AreSeparated (s ∪ s') t

Tactic:
refine ⟨min r r', ?_, fun x hx y hy => hx.elim ?_ ?_⟩

Result:
case intro.intro.intro.intro.refine_1
X : Type u_1
inst✝ : EMetricSpace X
s t s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ r ⊓ r' ≠ 0

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

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

Proof state:
case intro.intro.intro.intro.refine_1
X : Type u_1
inst✝ : EMetricSpace X
s t s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ r ⊓ r' ≠ 0

Tactic:
rw [← pos_iff_ne_zero] at r0 r0' ⊢

Result:
case intro.intro.intro.intro.refine_1
X : Type u_1
inst✝ : EMetricSpace X
s t s' : Set X
r : ENNReal
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ENNReal
r0' : 0 < r'
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ 0 < r ⊓ r'

Proof state:
case intro.intro.intro.intro.refine_2
X : Type u_1
inst✝ : EMetricSpace X
s t s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s → r ⊓ r' ≤ edist x y

Tactic:
exact fun hx => (min_le_left _ _).trans (hr _ hx _ hy)

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_3
X : Type u_1
inst✝ : EMetricSpace X
s t s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s' → r ⊓ r' ≤ edist x y

Tactic:
exact fun hx => (min_le_right _ _).trans (hr' _ hx _ hy)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : EMetricSpace X
s t s' : Set X
h : AreSeparated s t
h' : AreSeparated s' t
⊢ AreSeparated (s ∪ s') t

Tactic:
rcases h, h' with ⟨⟨r, r0, hr⟩, ⟨r', r0', hr'⟩⟩

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝ : EMetricSpace X
s t s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ AreSeparated (s ∪ s') t

Proof state:
case intro.intro.intro.intro.refine_1
X : Type u_1
inst✝ : EMetricSpace X
s t s' : Set X
r : ENNReal
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ENNReal
r0' : 0 < r'
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ 0 < r ⊓ r'

Tactic:
exact lt_min r0 r0'

Result:
no goals