-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_le_of_infDist {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ x ∈ s, infDist x t ≤ r)
    (H2 : ∀ x ∈ t, infDist x s ≤ r) : hausdorffDist s t ≤ r

Proof state:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s = ∅
⊢ hausdorffDist s t ≤ r

Tactic:
rwa [hs, hausdorffDist_empty']

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ hausdorffEdist s t ≤ ENNReal.ofReal r

Tactic:
apply hausdorffEdist_le_of_infEdist _ _

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ s, infEdist x t ≤ ENNReal.ofReal r

α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ t, infEdist x s ≤ ENNReal.ofReal r

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ t, infEdist x s ≤ ENNReal.ofReal r

Tactic:
simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEdist_ne_top hs) hr] using H2

Result:
no goals

Proof state:
case inr.inr
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
this : hausdorffEdist s t ≤ ENNReal.ofReal r
⊢ hausdorffDist s t ≤ r

Tactic:
exact ENNReal.toReal_le_of_le_ofReal hr this

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
⊢ hausdorffDist s t ≤ r

Tactic:
rcases s.eq_empty_or_nonempty with hs | hs

Result:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s = ∅
⊢ hausdorffDist s t ≤ r

case inr
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
⊢ hausdorffDist s t ≤ r

Proof state:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
⊢ hausdorffDist s t ≤ r

Tactic:
rcases t.eq_empty_or_nonempty with ht | ht

Result:
case inr.inl
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t = ∅
⊢ hausdorffDist s t ≤ r

case inr.inr
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ hausdorffDist s t ≤ r

Proof state:
case inr.inl
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t = ∅
⊢ hausdorffDist s t ≤ r

Tactic:
rwa [ht, hausdorffDist_empty]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ s, infEdist x t ≤ ENNReal.ofReal r

Tactic:
simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEdist_ne_top ht) hr] using H1

Result:
no goals