mathlib3

9a705331 - feat(data/option/basic): add ne_none_iff_exists (#3856)