case h.e'_5
α : Type u
inst✝ : MetricSpace α
⊢ 2 = 1 + 1
α : Type u
inst✝ : MetricSpace α
⊢ LipschitzWith 2 fun p => infDist p.fst ↑p.snd
convert @LipschitzWith.uncurry α (NonemptyCompacts α) ℝ _ _ _
  (fun (x : α) (s : NonemptyCompacts α) => infDist x s) 1 1
  (fun s => lipschitz_infDist_pt ↑s) lipschitz_infDist_set
no goals
case h.e'_5
α : Type u
inst✝ : MetricSpace α
⊢ 2 = 1 + 1
norm_num