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

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

src/data/finite/card.lean

@@ -62,6 +62,9 @@ finite.card_pos_iff.mpr h
 
 namespace finite
 
+lemma cast_card_eq_mk {α : Type*} [finite α] : ↑(nat.card α) = cardinal.mk α :=
+cardinal.cast_to_nat_of_lt_aleph_0 (cardinal.lt_aleph_0_of_finite α)
+
 lemma card_eq [finite α] [finite β] : nat.card α = nat.card β ↔ nonempty (α ≃ β) :=
 by { haveI := fintype.of_finite α, haveI := fintype.of_finite β, simp [fintype.card_eq] }
 
@@ -137,12 +140,33 @@ card_eq_zero_of_injective f.2 h
 lemma card_sum [finite α] [finite β] : nat.card (α ⊕ β) = nat.card α + nat.card β :=
 by { haveI := fintype.of_finite α, haveI := fintype.of_finite β, simp }
 
-end finite
+lemma card_image_le {s : set α} [finite s] (f : α → β) : nat.card (f '' s) ≤ nat.card s :=
+card_le_of_surjective _ set.surjective_onto_image
+
+lemma card_range_le [finite α] (f : α → β) : nat.card (set.range f) ≤ nat.card α :=
+card_le_of_surjective _ set.surjective_onto_range
 
-theorem finite.card_subtype_le [finite α] (p : α → Prop) :
+theorem card_subtype_le [finite α] (p : α → Prop) :
   nat.card {x // p x} ≤ nat.card α :=
 by { haveI := fintype.of_finite α, simpa using fintype.card_subtype_le p }
 
-theorem finite.card_subtype_lt [finite α] {p : α → Prop} {x : α} (hx : ¬ p x) :
+theorem card_subtype_lt [finite α] {p : α → Prop} {x : α} (hx : ¬ p x) :
   nat.card {x // p x} < nat.card α :=
 by { haveI := fintype.of_finite α, simpa using fintype.card_subtype_lt hx }
+
+end finite
+
+namespace set
+
+lemma card_union_le (s t : set α) : nat.card ↥(s ∪ t) ≤ nat.card s + nat.card t :=
+begin
+  casesI _root_.finite_or_infinite ↥(s ∪ t) with h h,
+  { rw [finite_coe_iff, finite_union, ←finite_coe_iff, ←finite_coe_iff] at h,
+    casesI h,
+    rw [←cardinal.nat_cast_le, nat.cast_add,
+        finite.cast_card_eq_mk, finite.cast_card_eq_mk, finite.cast_card_eq_mk],
+    exact cardinal.mk_union_le s t },
+  { exact nat.card_eq_zero_of_infinite.trans_le (zero_le _) },
+end
+
+end set