case refine'_1
ι : Sort ?u.52150
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist (closure s) t ≤ hausdorffEdist s t

case refine'_2
ι : Sort ?u.52150
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s t ≤ hausdorffEdist (closure s) t
ι : Sort ?u.52150
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist (closure s) t = hausdorffEdist s t
refine' le_antisymm _ _
no goals
case refine'_1
ι : Sort ?u.52150
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist (closure s) t ≤ hausdorffEdist s t
calc
  _ ≤ hausdorffEdist (closure s) s + hausdorffEdist s t := hausdorffEdist_triangle
  _ = hausdorffEdist s t := by simp [hausdorffEdist_comm]
no goals
ι : Sort ?u.52150
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist (closure s) s + hausdorffEdist s t = hausdorffEdist s t
simp [hausdorffEdist_comm]
no goals
case refine'_2
ι : Sort ?u.52150
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s t ≤ hausdorffEdist (closure s) t
calc
  _ ≤ hausdorffEdist s (closure s) + hausdorffEdist (closure s) t := hausdorffEdist_triangle
  _ = hausdorffEdist (closure s) t := by simp
no goals
ι : Sort ?u.52150
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s (closure s) + hausdorffEdist (closure s) t = hausdorffEdist (closure s) t
simp