feat(data/set/ncard): noncomputable set cardinality (#18576)
This PR introduces a function `set.ncard` that (noncomputably) gives the cardinality of a finite `set`, or zero if the set is infinite. The intention is to give a way to reason about set cardinality that avoids data and going between `set` and `finset`. This is especially useful for reasoning about sets in a `finite` type.
The added file is somewhat large, but it is essentially just duplicating the API in `data.finset.card` (minus the induction lemmas).
Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
