basic): remove duplicate `nonempty_insert` in favor of `insert_nonempty` (#14884)

Commit

3 years ago

chore(data/set/basic): remove duplicate `nonempty_insert` in favor of `insert_nonempty` (#14884) This name matches e.g. `univ_nonempty` and `singleton_nonempty`.

Author

vihdzp

Parents

365b2ee5

mathlib ee7f38c7 - chore(data/set/basic): remove duplicate `nonempty_insert` in favor of `insert_nonempty` (#14884)

mathlib
ee7f38c7 - chore(data/set/basic): remove duplicate `nonempty_insert` in favor of `insert_nonempty` (#14884)