mathlib3

0f287f82 - chore(topology/separation): move/add `simp` lemmas (#16470)

chore(topology/separation): move/add `simp` lemmas (#16470) * add `inseparable_iff_eq` and `inseparable_eq_eq`; * add `specializes_eq_eq`, move `@[simp]` from `specializes_iff_eq`; * golf `pure_le_nhds_iff` and `nhds_le_nhds_iff`.