feat(data/fintype/basic): add lemmas about finsets and cardinality (#5886)

Add lemmas about finsets and cardinality. Part of #5695 in order to prove Hall's marriage theorem.

Coauthors: @kmill @b-mehta

Author: agusakov

src/data/fintype/basic.lean

@@ -79,6 +79,9 @@ set.ext $ λ x, mem_compl
 theorem eq_univ_iff_forall {s : finset α} : s = univ ↔ ∀ x, x ∈ s :=
 by simp [ext_iff]
 
+lemma compl_ne_univ_iff_nonempty [decidable_eq α] (s : finset α) : sᶜ ≠ univ ↔ s.nonempty :=
+by simp [eq_univ_iff_forall, finset.nonempty]
+
 @[simp] lemma univ_inter [decidable_eq α] (s : finset α) :
   univ ∩ s = s := ext $ λ a, by simp
 
@@ -306,10 +309,22 @@ lemma finset.eq_univ_of_card [fintype α] (s : finset α) (hs : s.card = fintype
   s = univ :=
 eq_of_subset_of_card_le (subset_univ _) $ by rw [hs, finset.card_univ]
 
+lemma finset.card_eq_iff_eq_univ [fintype α] (s : finset α) :
+  s.card = fintype.card α ↔ s = finset.univ :=
+⟨s.eq_univ_of_card, by { rintro rfl, exact finset.card_univ, }⟩
+
 lemma finset.card_le_univ [fintype α] (s : finset α) :
   s.card ≤ fintype.card α :=
 card_le_of_subset (subset_univ s)
 
+lemma finset.card_lt_iff_ne_univ [fintype α] (s : finset α) :
+  s.card < fintype.card α ↔ s ≠ finset.univ :=
+s.card_le_univ.lt_iff_ne.trans (not_iff_not_of_iff s.card_eq_iff_eq_univ)
+
+lemma finset.card_compl_lt_iff_nonempty [fintype α] [decidable_eq α] (s : finset α) :
+  sᶜ.card < fintype.card α ↔ s.nonempty :=
+sᶜ.card_lt_iff_ne_univ.trans s.compl_ne_univ_iff_nonempty
+
 lemma finset.card_univ_diff [decidable_eq α] [fintype α] (s : finset α) :
   (finset.univ \ s).card = fintype.card α - s.card :=
 finset.card_sdiff (subset_univ s)