chore: rename Finset.card_doubleton to Finset.card_pair (#9379)

Author: jcommelin

Mathlib/Combinatorics/SimpleGraph/Clique.lean

@@ -339,7 +339,7 @@ theorem cliqueFree_two : G.CliqueFree 2 ↔ G = ⊥ := by
   classical
   constructor
   · simp_rw [← edgeSet_eq_empty, Set.eq_empty_iff_forall_not_mem, Sym2.forall, mem_edgeSet]
-    exact fun h a b hab => h _ ⟨by simpa [hab.ne], card_doubleton hab.ne⟩
+    exact fun h a b hab => h _ ⟨by simpa [hab.ne], card_pair hab.ne⟩
   · rintro rfl
     exact cliqueFree_bot le_rfl
 #align simple_graph.clique_free_two SimpleGraph.cliqueFree_two
@@ -396,7 +396,7 @@ theorem cliqueFreeOn_of_card_lt {s : Finset α} (h : s.card < n) : G.CliqueFreeO
 @[simp]
 theorem cliqueFreeOn_two : G.CliqueFreeOn s 2 ↔ s.Pairwise (G.Adjᶜ) := by
   classical
-  refine' ⟨fun h a ha b hb _ hab => h _ ⟨by simpa [hab.ne], card_doubleton hab.ne⟩, _⟩
+  refine' ⟨fun h a ha b hb _ hab => h _ ⟨by simpa [hab.ne], card_pair hab.ne⟩, _⟩
   · push_cast
     exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩
   simp only [CliqueFreeOn, isNClique_iff, card_eq_two, coe_subset, not_and, not_exists]

Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

@@ -136,7 +136,7 @@ theorem sum_incMatrix_apply_of_mem_edgeSet :
     refine' e.ind _
     intro a b h
     rw [mem_edgeSet] at h
-    rw [← Nat.cast_two, ← card_doubleton h.ne]
+    rw [← Nat.cast_two, ← card_pair h.ne]
     simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h, true_and_iff]
     congr 2
     ext e
@@ -157,7 +157,7 @@ theorem incMatrix_transpose_mul_diag [DecidableRel G.Adj] :
     · revert h
       refine' e.ind _
       intro v w h
-      rw [← Nat.cast_two, ← card_doubleton (G.ne_of_adj h)]
+      rw [← Nat.cast_two, ← card_pair (G.ne_of_adj h)]
       simp only [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h, true_and, mem_univ, forall_true_left,
         forall_eq_or_imp, forall_eq, and_self, mem_singleton, ne_eq]
       congr 2

Mathlib/Data/Finset/Card.lean

@@ -149,9 +149,11 @@ theorem card_insert_eq_ite : card (insert a s) = if a ∈ s then s.card else s.c
 #align finset.card_insert_eq_ite Finset.card_insert_eq_ite
 
 @[simp]
-theorem card_doubleton (h : a ≠ b) : ({a, b} : Finset α).card = 2 := by
+theorem card_pair (h : a ≠ b) : ({a, b} : Finset α).card = 2 := by
   rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton]
-#align finset.card_doubleton Finset.card_doubleton
+#align finset.card_doubleton Finset.card_pair
+
+@[deprecated] alias card_doubleton := Finset.card_pair
 
 /-- $\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$. -/
 @[simp]
@@ -694,7 +696,7 @@ theorem card_eq_two : s.card = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y} := by
     rintro ⟨a, _, hab, rfl, b, rfl⟩
     exact ⟨a, b, not_mem_singleton.1 hab, rfl⟩
   · rintro ⟨x, y, h, rfl⟩
-    exact card_doubleton h
+    exact card_pair h
 #align finset.card_eq_two Finset.card_eq_two
 
 theorem card_eq_three : s.card = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z} := by

Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean

@@ -264,7 +264,7 @@ theorem quadraticChar_card_sqrts (hF : ringChar F ≠ 2) (a : F) :
           simp only [neg_sq]
       norm_cast
       rw [h₁, List.toFinset_cons, List.toFinset_cons, List.toFinset_nil]
-      exact Finset.card_doubleton (Ne.symm (mt (Ring.eq_self_iff_eq_zero_of_char_ne_two hF).mp h₀))
+      exact Finset.card_pair (Ne.symm (mt (Ring.eq_self_iff_eq_zero_of_char_ne_two hF).mp h₀))
     · rw [quadraticChar_neg_one_iff_not_isSquare.mpr h]
       simp only [Int.coe_nat_eq_zero, Finset.card_eq_zero, Set.toFinset_card, Fintype.card_ofFinset,
         Set.mem_setOf_eq, add_left_neg]

Mathlib/NumberTheory/NumberField/Embeddings.lean

@@ -461,7 +461,7 @@ theorem card_filter_mk_eq [NumberField K] (w : InfinitePlace K) :
   split_ifs with hw
   · rw [ComplexEmbedding.isReal_iff.mp (isReal_iff.mp hw), Finset.union_idempotent,
       Finset.card_singleton]
-  · refine Finset.card_doubleton ?_
+  · refine Finset.card_pair ?_
     rwa [Ne.def, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]
 
 open scoped BigOperators