mathlib3

d9992ade - feat(data/set/basic): Add natural missing lemmas to `set.subsingleton` and slightly refactor (#15886)

feat(data/set/basic): Add natural missing lemmas to `set.subsingleton` and slightly refactor (#15886) - `subsingleton.image` is moved and documentation is added so that it is near related lemmas. - `subsingleton_of_preimage` is added to go with `subsingleton.preimage`, `subsingleton_of_image`., and `subsingleton.image`. - We add `subsingleton_anti` analogously to `nontrivial_mono`. - Some small style tweaks are made. - `subsingleton.mono` is renamed to `subsingleton.anti`. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>