mathlib3

508b13ee - chore(*): flip various `subsingleton_iff`, `nontrivial_iff` lemmas and add `simp` (#8703)