refactor(set_theory/cardinal): review API about #α = 2/`nat.card α …

…= 2` (#16899)

* Rename `cardinal.mk_eq_nat_iff_finset` to `cardinal.mk_set_eq_nat_iff_finset`, add a version for types and `cardinal.mk_eq_nat_iff_fintype`.
* Add `cardinal.to_nat_eq_iff`, a more general version of `cardinal.to_nat_eq_one`.
* Rename `cardinal.exists_not_mem_of_length_le` to `cardinal.exists_not_mem_of_length_lt`.
* Add `cardinal.mk_eq_two_iff`, `cardinal.mk_eq_two_iff'`, `nat.card_eq_two_iff`, and `nat.card_eq_two_iff'`.

src/linear_algebra/dimension.lean

@@ -1203,7 +1203,7 @@ lemma le_dim_iff_exists_linear_independent_finset {n : ℕ} :
   ↑n ≤ module.rank K V ↔
     ∃ s : finset V, s.card = n ∧ linear_independent K (coe : (s : set V) → V) :=
 begin
-  simp only [le_dim_iff_exists_linear_independent, cardinal.mk_eq_nat_iff_finset],
+  simp only [le_dim_iff_exists_linear_independent, cardinal.mk_set_eq_nat_iff_finset],
   split,
   { rintro ⟨s, ⟨t, rfl, rfl⟩, si⟩,
     exact ⟨t, rfl, si⟩ },
@@ -1332,7 +1332,7 @@ lemma le_rank_iff_exists_linear_independent_finset {n : ℕ} {f : V →ₗ[K] V'
   ↑n ≤ rank f ↔ ∃ s : finset V, s.card = n ∧ linear_independent K (λ x : (s : set V), f x) :=
 begin
   simp only [le_rank_iff_exists_linear_independent, cardinal.lift_nat_cast,
-    cardinal.lift_eq_nat_iff, cardinal.mk_eq_nat_iff_finset],
+    cardinal.lift_eq_nat_iff, cardinal.mk_set_eq_nat_iff_finset],
   split,
   { rintro ⟨s, ⟨t, rfl, rfl⟩, si⟩,
     exact ⟨t, rfl, si⟩ },

src/set_theory/cardinal/basic.lean

@@ -1169,10 +1169,13 @@ by rw [←to_nat_cast 0, nat.cast_zero]
 @[simp] lemma one_to_nat : to_nat 1 = 1 :=
 by rw [←to_nat_cast 1, nat.cast_one]
 
+lemma to_nat_eq_iff {c : cardinal} {n : ℕ} (hn : n ≠ 0) : to_nat c = n ↔ c = n :=
+⟨λ h, (cast_to_nat_of_lt_aleph_0 (lt_of_not_ge (hn ∘ h.symm.trans ∘
+  to_nat_apply_of_aleph_0_le))).symm.trans (congr_arg coe h),
+  λ h, (congr_arg to_nat h).trans (to_nat_cast n)⟩
+
 @[simp] lemma to_nat_eq_one {c : cardinal} : to_nat c = 1 ↔ c = 1 :=
-⟨λ h, (cast_to_nat_of_lt_aleph_0 (lt_of_not_ge (one_ne_zero ∘ h.symm.trans ∘
-  to_nat_apply_of_aleph_0_le))).symm.trans ((congr_arg coe h).trans nat.cast_one),
-  λ h, (congr_arg to_nat h).trans one_to_nat⟩
+by rw [to_nat_eq_iff one_ne_zero, nat.cast_one]
 
 lemma to_nat_eq_one_iff_unique {α : Type*} : (#α).to_nat = 1 ↔ subsingleton α ∧ nonempty α :=
 to_nat_eq_one.trans eq_one_iff_unique
@@ -1388,7 +1391,7 @@ by { rw bUnion_eq_Union, apply mk_Union_le }
 lemma finset_card_lt_aleph_0 (s : finset α) : #(↑s : set α) < ℵ₀ :=
 lt_aleph_0_of_finite _
 
-theorem mk_eq_nat_iff_finset {α} {s : set α} {n : ℕ} :
+theorem mk_set_eq_nat_iff_finset {α} {s : set α} {n : ℕ} :
   #s = n ↔ ∃ t : finset α, (t : set α) = s ∧ t.card = n :=
 begin
   split,
@@ -1399,6 +1402,19 @@ begin
     exact mk_coe_finset }
 end
 
+theorem mk_eq_nat_iff_finset {n : ℕ} : #α = n ↔ ∃ t : finset α, (t : set α) = univ ∧ t.card = n :=
+by rw [← mk_univ, mk_set_eq_nat_iff_finset]
+
+theorem mk_eq_nat_iff_fintype {n : ℕ} : #α = n ↔ ∃ (h : fintype α), @fintype.card α h = n :=
+begin
+  rw [mk_eq_nat_iff_finset],
+  split,
+  { rintro ⟨t, ht, hn⟩,
+    exact ⟨⟨t, eq_univ_iff_forall.1 ht⟩, hn⟩ },
+  { rintro ⟨⟨t, ht⟩, hn⟩,
+    exact ⟨t, eq_univ_iff_forall.2 ht, hn⟩ }
+end
+
 theorem mk_union_add_mk_inter {α : Type u} {S T : set α} :
   #(S ∪ T : set α) + #(S ∩ T : set α) = #S + #T :=
 quot.sound ⟨equiv.set.union_sum_inter S T⟩
@@ -1507,24 +1523,33 @@ begin
 end
 
 lemma two_le_iff : (2 : cardinal) ≤ #α ↔ ∃x y : α, x ≠ y :=
+by rw [← nat.cast_two, nat_succ, succ_le_iff, nat.cast_one, one_lt_iff_nontrivial, nontrivial_iff]
+
+lemma two_le_iff' (x : α) : (2 : cardinal) ≤ #α ↔ ∃y : α, y ≠ x :=
+by rw [two_le_iff, ← nontrivial_iff, nontrivial_iff_exists_ne x]
+
+lemma mk_eq_two_iff : #α = 2 ↔ ∃ x y : α, x ≠ y ∧ ({x, y} : set α) = univ :=
 begin
+  simp only [← @nat.cast_two cardinal, mk_eq_nat_iff_finset, finset.card_eq_two],
   split,
-  { rintro ⟨f⟩, refine ⟨f $ sum.inl ⟨⟩, f $ sum.inr ⟨⟩, _⟩, intro h, cases f.2 h },
-  { rintro ⟨x, y, h⟩, by_contra h',
-    rw [not_le, ←nat.cast_two, nat_succ, lt_succ_iff, nat.cast_one, le_one_iff_subsingleton] at h',
-    apply h, exactI subsingleton.elim _ _ }
+  { rintro ⟨t, ht, x, y, hne, rfl⟩,
+    exact ⟨x, y, hne, by simpa using ht⟩ },
+  { rintro ⟨x, y, hne, h⟩,
+    exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩ }
 end
 
-lemma two_le_iff' (x : α) : (2 : cardinal) ≤ #α ↔ ∃y : α, x ≠ y :=
+lemma mk_eq_two_iff' (x : α) : #α = 2 ↔ ∃! y, y ≠ x :=
 begin
-  rw [two_le_iff],
-  split,
-  { rintro ⟨y, z, h⟩, refine classical.by_cases (λ(h' : x = y), _) (λ h', ⟨y, h'⟩),
-    rw [←h'] at h, exact ⟨z, h⟩ },
-  { rintro ⟨y, h⟩, exact ⟨x, y, h⟩ }
+  rw [mk_eq_two_iff], split,
+  { rintro ⟨a, b, hne, h⟩,
+    simp only [eq_univ_iff_forall, mem_insert_iff, mem_singleton_iff] at h,
+    rcases h x with rfl|rfl,
+    exacts [⟨b, hne.symm, λ z, (h z).resolve_left⟩, ⟨a, hne, λ z, (h z).resolve_right⟩] },
+  { rintro ⟨y, hne, hy⟩,
+    exact ⟨x, y, hne.symm, eq_univ_of_forall $ λ z, or_iff_not_imp_left.2 (hy z)⟩ }
 end
 
-lemma exists_not_mem_of_length_le {α : Type*} (l : list α) (h : ↑l.length < # α) :
+lemma exists_not_mem_of_length_lt {α : Type*} (l : list α) (h : ↑l.length < # α) :
   ∃ (z : α), z ∉ l :=
 begin
   contrapose! h,
@@ -1539,7 +1564,7 @@ lemma three_le {α : Type*} (h : 3 ≤ # α) (x : α) (y : α) :
 begin
   have : ↑(3 : ℕ) ≤ # α, simpa using h,
   have : ↑(2 : ℕ) < # α, rwa [← succ_le_iff, ← cardinal.nat_succ],
-  have := exists_not_mem_of_length_le [x, y] this,
+  have := exists_not_mem_of_length_lt [x, y] this,
   simpa [not_or_distrib] using this,
 end
 

src/set_theory/cardinal/finite.lean

@@ -70,6 +70,12 @@ card_of_subsingleton default
 lemma card_eq_one_iff_unique : nat.card α = 1 ↔ subsingleton α ∧ nonempty α :=
 cardinal.to_nat_eq_one_iff_unique
 
+lemma card_eq_two_iff : nat.card α = 2 ↔ ∃ x y : α, x ≠ y ∧ {x, y} = @set.univ α :=
+(to_nat_eq_iff two_ne_zero).trans $ iff.trans (by rw [nat.cast_two]) mk_eq_two_iff
+
+lemma card_eq_two_iff' (x : α) : nat.card α = 2 ↔ ∃! y, y ≠ x :=
+(to_nat_eq_iff two_ne_zero).trans $ iff.trans (by rw [nat.cast_two]) (mk_eq_two_iff' x)
+
 theorem card_of_is_empty [is_empty α] : nat.card α = 0 := by simp
 
 @[simp] lemma card_prod (α β : Type*) : nat.card (α × β) = nat.card α * nat.card β :=