feat(data/finite/card): Cardinality of union, image, and range (#17253)
feat(data/finite/card): Cardinality of union, image, and range (#17253)

This PR adds lemmas for the cardinality of union, image, and range.





leanprover-community/mathlib,leanprover-community/mathlib