-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_triangle : hausdorffEdist s u ≤ hausdorffEdist s t + hausdorffEdist t u

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ (⨆ x ∈ s, infEdist x u) ⊔ ⨆ y ∈ u, infEdist y s ≤ hausdorffEdist s t + hausdorffEdist t u

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ (∀ i ∈ s, infEdist i u ≤ hausdorffEdist s t + hausdorffEdist t u) ∧
    ∀ i ∈ u, infEdist i s ≤ hausdorffEdist s t + hausdorffEdist t u

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ hausdorffEdist s u ≤ hausdorffEdist s t + hausdorffEdist t u

Tactic:
rw [hausdorffEdist_def]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ (⨆ x ∈ s, infEdist x u) ⊔ ⨆ y ∈ u, infEdist y s ≤ hausdorffEdist s t + hausdorffEdist t u

Proof state:
case left
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ ∀ i ∈ s, infEdist i u ≤ hausdorffEdist s t + hausdorffEdist t u

Tactic:
show ∀ x ∈ s, infEdist x u ≤ hausdorffEdist s t + hausdorffEdist t u

Result:
case left
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ ∀ x ∈ s, infEdist x u ≤ hausdorffEdist s t + hausdorffEdist t u

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ (∀ i ∈ s, infEdist i u ≤ hausdorffEdist s t + hausdorffEdist t u) ∧
    ∀ i ∈ u, infEdist i s ≤ hausdorffEdist s t + hausdorffEdist t u

Tactic:
constructor

Result:
case left
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ ∀ i ∈ s, infEdist i u ≤ hausdorffEdist s t + hausdorffEdist t u

case right
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ ∀ i ∈ u, infEdist i s ≤ hausdorffEdist s t + hausdorffEdist t u

Proof state:
case left
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ ∀ x ∈ s, infEdist x u ≤ hausdorffEdist s t + hausdorffEdist t u

Tactic:
exact fun x xs =>
  calc
    infEdist x u ≤ infEdist x t + hausdorffEdist t u :=
      infEdist_le_infEdist_add_hausdorffEdist
    _ ≤ hausdorffEdist s t + hausdorffEdist t u :=
      add_le_add_right (infEdist_le_hausdorffEdist_of_mem xs) _

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
x : α
xu : x ∈ u
⊢ hausdorffEdist u t + hausdorffEdist t s = hausdorffEdist s t + hausdorffEdist t u

Tactic:
simp [hausdorffEdist_comm, add_comm]

Result:
no goals

Proof state:
case right
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ ∀ i ∈ u, infEdist i s ≤ hausdorffEdist s t + hausdorffEdist t u

Tactic:
show ∀ x ∈ u, infEdist x s ≤ hausdorffEdist s t + hausdorffEdist t u

Result:
case right
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ ∀ x ∈ u, infEdist x s ≤ hausdorffEdist s t + hausdorffEdist t u

Proof state:
case right
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ ∀ x ∈ u, infEdist x s ≤ hausdorffEdist s t + hausdorffEdist t u

Tactic:
exact fun x xu =>
  calc
    infEdist x s ≤ infEdist x t + hausdorffEdist t s :=
      infEdist_le_infEdist_add_hausdorffEdist
    _ ≤ hausdorffEdist u t + hausdorffEdist t s :=
      add_le_add_right (infEdist_le_hausdorffEdist_of_mem xu) _
    _ = hausdorffEdist s t + hausdorffEdist t u := by simp [hausdorffEdist_comm, add_comm]

Result:
no goals