mathlib

bedb810b - feat(*): a few more theorems about `unique` and `subsingleton` (#2230)

feat(*): a few more theorems about `unique` and `subsingleton` (#2230) * feat(*): a few more theorems about `unique` and `subsingleton` * Fix compile, fix two non-terminate `simp`s * Update src/topology/metric_space/antilipschitz.lean This lemma will go to another PR Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>