mathlib

4ed50443 - feat(tactic/positivity): Extension for `finset.card` (#16637)

feat(tactic/positivity): Extension for `finset.card` (#16637) A best effort `positivity` extension for `finset.card`. This looks for an assumption of the form `s.nonempty` in context to prove `0 < s.card`.