-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem _root_.Disjoint.exists_thickenings (hst : Disjoint s t) (hs : IsCompact s)
    (ht : IsClosed t) :
    ∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)

Proof state:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal (↑r / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal (↑r / 2)
⊢ z ∈ ⊥

Tactic:
rw [← NNReal.coe_two, ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal] at hzs hzt

Result:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ↑(r / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ↑(r / 2)
⊢ z ∈ ⊥

Proof state:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ↑(r / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ↑(r / 2)
⊢ z ∈ ⊥

Tactic:
obtain ⟨x, hx, hzx⟩ := hzs

Result:
case intro.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzt : ∃ z_1 ∈ t, edist z z_1 < ↑(r / 2)
x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
⊢ z ∈ ⊥

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ edist x y ≤ ↑r

Tactic:
calc
  edist x y ≤ edist z x + edist z y := edist_triangle_left _ _ _
  _ ≤ ↑(r / 2) + ↑(r / 2) := add_le_add hzx.le hzy.le
  _ = r := by rw [← ENNReal.coe_add, add_halves]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ z ∈ ⊥

Tactic:
refine (h x hx y hy).not_le ?_

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ edist x y ≤ ↑r

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
⊢ ∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)

Tactic:
obtain ⟨r, hr, h⟩ := exists_pos_forall_lt_edist hs ht hst

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
⊢ ∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
⊢ ∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)

Tactic:
refine ⟨r / 2, half_pos (NNReal.coe_pos.2 hr), ?_⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
⊢ Disjoint (thickening (↑r / 2) s) (thickening (↑r / 2) t)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ ↑(r / 2) + ↑(r / 2) = ↑r

Tactic:
rw [← ENNReal.coe_add, add_halves]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzs : z ∈ thickening (↑r / 2) s
hzt : z ∈ thickening (↑r / 2) t
⊢ z ∈ ⊥

Tactic:
rw [mem_thickening_iff_exists_edist_lt] at hzs hzt

Result:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal (↑r / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal (↑r / 2)
⊢ z ∈ ⊥

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
⊢ thickening (↑r / 2) s ⊓ thickening (↑r / 2) t ≤ ⊥

Tactic:
rintro z ⟨hzs, hzt⟩

Result:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzs : z ∈ thickening (↑r / 2) s
hzt : z ∈ thickening (↑r / 2) t
⊢ z ∈ ⊥

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
⊢ Disjoint (thickening (↑r / 2) s) (thickening (↑r / 2) t)

Tactic:
rw [disjoint_iff_inf_le]

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
⊢ thickening (↑r / 2) s ⊓ thickening (↑r / 2) t ≤ ⊥

Proof state:
case intro.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzt : ∃ z_1 ∈ t, edist z z_1 < ↑(r / 2)
x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
⊢ z ∈ ⊥

Tactic:
obtain ⟨y, hy, hzy⟩ := hzt

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ z ∈ ⊥