basic): generalize `finset.nonempty_mk_coe` to `nonempty_mk` (#16399)

Commit

3 years ago

chore(data/finset/basic): generalize `finset.nonempty_mk_coe` to `nonempty_mk` (#16399)

Author

urkud

Parents