chore(data/fintype/basic): add card_unique and a warning note to `c…

…ard_of_subsingleton` (#7008)

src/data/fintype/basic.lean

@@ -375,9 +375,16 @@ def of_subsingleton (a : α) [subsingleton α] : fintype α :=
 @[simp] theorem univ_of_subsingleton (a : α) [subsingleton α] :
   @univ _ (of_subsingleton a) = {a} := rfl
 
+/-- Note: this lemma is specifically about `fintype.of_subsingleton`. For a statement about
+arbitrary `fintype` instances, use either `fintype.card_le_one_iff_subsingleton` or
+`fintype.card_unique`. -/
 @[simp] theorem card_of_subsingleton (a : α) [subsingleton α] :
   @fintype.card _ (of_subsingleton a) = 1 := rfl
 
+@[simp] theorem card_unique [unique α] [h : fintype α] :
+  fintype.card α = 1 :=
+subsingleton.elim (of_subsingleton $ default α) h ▸ card_of_subsingleton _
+
 open_locale classical
 variables (α)