feat(data/finset/basic): A finset has card two iff it's {x, y} for some x ≠ y (#10252)

and the similar result for card three. Dumb but surprisingly annoying!

Author: YaelDillies

src/data/finset/basic.lean

@@ -2427,6 +2427,31 @@ iff.intro
       by simp only [eq, card_erase_of_mem has, pred_succ]⟩)
   (assume ⟨a, t, hat, s_eq, n_eq⟩, s_eq ▸ n_eq ▸ card_insert_of_not_mem hat)
 
+lemma card_eq_two [decidable_eq α] {s : finset α} : s.card = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y} :=
+begin
+  split,
+  { rw card_eq_succ,
+    simp_rw [card_eq_one],
+    rintro ⟨a, _, hab, rfl, b, rfl⟩,
+    exact ⟨a, b, not_mem_singleton.1 hab, rfl⟩ },
+  { rintro ⟨x, y, hxy, rfl⟩,
+    simp only [hxy, card_insert_of_not_mem, not_false_iff, mem_singleton, card_singleton] }
+end
+
+lemma card_eq_three [decidable_eq α] {s : finset α} :
+  s.card = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z} :=
+begin
+  split,
+  { rw card_eq_succ,
+    simp_rw [card_eq_two],
+    rintro ⟨a, _, abc, rfl, b, c, bc, rfl⟩,
+    rw [mem_insert, mem_singleton, not_or_distrib] at abc,
+    exact ⟨a, b, c, abc.1, abc.2, bc, rfl⟩ },
+  { rintro ⟨x, y, z, xy, xz, yz, rfl⟩,
+    simp only [xy, xz, yz, mem_insert, card_insert_of_not_mem, not_false_iff, mem_singleton,
+      or_self, card_singleton] }
+end
+
 theorem card_filter_le (s : finset α) (p : α → Prop) [decidable_pred p] :
   card (s.filter p) ≤ card s :=
 card_le_of_subset $ filter_subset _ _

src/data/list/basic.lean

@@ -236,6 +236,12 @@ end
 @[simp] lemma length_injective [subsingleton α] : injective (length : list α → ℕ) :=
 length_injective_iff.mpr $ by apply_instance
 
+lemma length_eq_two {l : list α} : l.length = 2 ↔ ∃ a b, l = [a, b] :=
+⟨match l with [a, b], _ := ⟨a, b, rfl⟩ end, λ ⟨a, b, e⟩, e.symm ▸ rfl⟩
+
+lemma length_eq_three {l : list α} : l.length = 3 ↔ ∃ a b c, l = [a, b, c] :=
+⟨match l with [a, b, c], _ := ⟨a, b, c, rfl⟩ end, λ ⟨a, b, c, e⟩, e.symm ▸ rfl⟩
+
 /-! ### set-theoretic notation of lists -/
 
 lemma empty_eq : (∅ : list α) = [] := by refl

src/data/multiset/basic.lean

@@ -504,6 +504,16 @@ pos_iff_ne_zero.trans $ not_congr card_eq_zero
 theorem card_pos_iff_exists_mem {s : multiset α} : 0 < card s ↔ ∃ a, a ∈ s :=
 quot.induction_on s $ λ l, length_pos_iff_exists_mem
 
+lemma card_eq_two {s : multiset α} : s.card = 2 ↔ ∃ x y, s = {x, y} :=
+⟨quot.induction_on s (λ l h, (list.length_eq_two.mp h).imp
+  (λ a, Exists.imp (λ b, congr_arg coe))), λ ⟨a, b, e⟩, e.symm ▸ rfl⟩
+
+lemma card_eq_three {s : multiset α} : s.card = 3 ↔ ∃ x y z, s = {x, y, z} :=
+⟨quot.induction_on s (λ l h, (list.length_eq_three.mp h).imp
+  (λ a, Exists.imp (λ b, Exists.imp (λ c, congr_arg coe)))), λ ⟨a, b, c, e⟩, e.symm ▸ rfl⟩
+
+/-! ### Induction principles -/
+
 /-- A strong induction principle for multisets:
 If you construct a value for a particular multiset given values for all strictly smaller multisets,
 you can construct a value for any multiset.