-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem exists_pos_forall_lt_edist (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) :
    ∃ r : ℝ≥0, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (r : ℝ≥0∞) < edist x y

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
⊢ ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Result:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
ht : IsClosed t
hs : IsCompact ∅
hst : Disjoint ∅ t
⊢ ∃ r, 0 < r ∧ ∀ x ∈ ∅, ∀ y ∈ t, ↑r < edist x y

case inr
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : s.Nonempty
⊢ ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

Proof state:
case inr.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : s.Nonempty
x : α
hx : x ∈ s
h : IsMinOn (fun x => infEdist x ?m.39220) s x
this : 0 < infEdist x t
⊢ ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 this with ⟨r, h₀, hr⟩

Result:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : s.Nonempty
x : α
hx : x ∈ s
h : IsMinOn (fun x => infEdist x ?m.39220) s x
this : 0 < infEdist x t
r : ℝ≥0
h₀ : 0 < ↑r
hr : ↑r < infEdist x t
⊢ ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

Proof state:
case inr.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : s.Nonempty
x : α
hx : x ∈ s
h : IsMinOn (fun x => infEdist x ?m.39220) s x
⊢ ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

Tactic:
have : 0 < infEdist x t :=
  pos_iff_ne_zero.2 fun H => hst.le_bot ⟨hx, (mem_iff_infEdist_zero_of_closed ht).mpr H⟩

Result:
case inr.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : s.Nonempty
x : α
hx : x ∈ s
h : IsMinOn (fun x => infEdist x ?m.39220) s x
this : 0 < infEdist x t
⊢ ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

Proof state:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
ht : IsClosed t
hs : IsCompact ∅
hst : Disjoint ∅ t
⊢ ∃ r, 0 < r ∧ ∀ x ∈ ∅, ∀ y ∈ t, ↑r < edist x y

Tactic:
use 1

Result:
case h
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
ht : IsClosed t
hs : IsCompact ∅
hst : Disjoint ∅ t
⊢ 0 < 1 ∧ ∀ x ∈ ∅, ∀ y ∈ t, ↑1 < edist x y

Proof state:
case h
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
ht : IsClosed t
hs : IsCompact ∅
hst : Disjoint ∅ t
⊢ 0 < 1 ∧ ∀ x ∈ ∅, ∀ y ∈ t, ↑1 < edist x y

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : s.Nonempty
⊢ ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

Tactic:
obtain ⟨x, hx, h⟩ := hs.exists_isMinOn hne continuous_infEdist.continuousOn

Result:
case inr.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : s.Nonempty
x : α
hx : x ∈ s
h : IsMinOn (fun x => infEdist x ?m.39220) s x
⊢ ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

Proof state:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : s.Nonempty
x : α
hx : x ∈ s
h : IsMinOn (fun x => infEdist x ?m.39220) s x
this : 0 < infEdist x t
r : ℝ≥0
h₀ : 0 < ↑r
hr : ↑r < infEdist x t
⊢ ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

Tactic:
exact ⟨r, ENNReal.coe_pos.mp h₀, fun y hy z hz => hr.trans_le <| le_infEdist.1 (h hy) z hz⟩

Result:
no goals