feat(set_theory/cardinal): add three_le (#12225)

src/data/finset/card.lean

@@ -308,6 +308,12 @@ lemma card_sdiff (h : s ⊆ t) : card (t \ s) = t.card - s.card :=
 suffices card (t \ s) = card ((t \ s) ∪ s) - s.card, by rwa sdiff_union_of_subset h at this,
 by rw [card_disjoint_union sdiff_disjoint, add_tsub_cancel_right]
 
+lemma le_card_sdiff (s t : finset α) : t.card - s.card ≤ card (t \ s) :=
+calc card t - card s
+      ≤ card t - card (s ∩ t) : tsub_le_tsub_left (card_le_of_subset (inter_subset_left s t)) _
+  ... = card (t \ (s ∩ t)) : (card_sdiff (inter_subset_right s t)).symm
+  ... ≤ card (t \ s) : by rw sdiff_inter_self_right t s
+
 lemma card_sdiff_add_card : (s \ t).card + t.card = (s ∪ t).card :=
 by rw [←card_disjoint_union sdiff_disjoint, sdiff_union_self_eq_union]
 

src/set_theory/cardinal.lean

@@ -1112,24 +1112,6 @@ lemma mk_int : #ℤ = ω := mk_denumerable ℤ
 
 lemma mk_pnat : #ℕ+ = ω := mk_denumerable ℕ+
 
-lemma two_le_iff : (2 : cardinal) ≤ #α ↔ ∃x y : α, x ≠ y :=
-begin
-  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, nat.cast_one, le_one_iff_subsingleton] at h',
-    apply h, exactI subsingleton.elim _ _ }
-end
-
-lemma two_le_iff' (x : α) : (2 : cardinal) ≤ #α ↔ ∃y : α, x ≠ y :=
-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⟩ }
-end
-
 /-- **König's theorem** -/
 theorem sum_lt_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i < g i) : sum f < prod g :=
 lt_of_not_ge $ λ ⟨F⟩, begin
@@ -1364,6 +1346,43 @@ begin
   apply exists_congr, intro t, rw [mk_image_eq], apply subtype.val_injective
 end
 
+lemma two_le_iff : (2 : cardinal) ≤ #α ↔ ∃x y : α, x ≠ y :=
+begin
+  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, nat.cast_one, le_one_iff_subsingleton] at h',
+    apply h, exactI subsingleton.elim _ _ }
+end
+
+lemma two_le_iff' (x : α) : (2 : cardinal) ≤ #α ↔ ∃y : α, x ≠ y :=
+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⟩ }
+end
+
+lemma exists_not_mem_of_length_le {α : Type*} (l : list α) (h : ↑l.length < # α) :
+  ∃ (z : α), z ∉ l :=
+begin
+  contrapose! h,
+  calc # α = # (set.univ : set α) : mk_univ.symm
+    ... ≤ # l.to_finset           : mk_le_mk_of_subset (λ x _, list.mem_to_finset.mpr (h x))
+    ... = l.to_finset.card        : cardinal.mk_finset
+    ... ≤ l.length                : cardinal.nat_cast_le.mpr (list.to_finset_card_le l),
+end
+
+lemma three_le {α : Type*} (h : 3 ≤ # α) (x : α) (y : α) :
+  ∃ (z : α), z ≠ x ∧ z ≠ y :=
+begin
+  have : ((3:nat) : cardinal) ≤ # α, simpa using h,
+  have : ((2:nat) : cardinal) < # α, rwa [← cardinal.succ_le, ← cardinal.nat_succ],
+  have := exists_not_mem_of_length_le [x, y] this,
+  simpa [not_or_distrib] using this,
+end
+
 /-- The function α^{<β}, defined to be sup_{γ < β} α^γ.
   We index over {s : set β.out // #s < β } instead of {γ // γ < β}, because the latter lives in a
   higher universe -/