perf: remove @[simp] on Fintype.card_of{IsEmpty,Subsingleton} (#2…

…0524)

These lemmas only apply to `Fintype.ofIsEmpty` and `Fintype.ofSubsingleton`, but they're discrimination tree keys match any `Fintype.card` application. This forces Lean to attempt to unify the variables too often, especially because unification problems which introduce metavariables don't benefit from the same caching mechanisms. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Adding.20.2F.20modifying.20Aesop.20lemmas/near/491949014)

Mathlib/Data/Fintype/Card.lean

@@ -194,7 +194,6 @@ theorem card_eq {α β} [_F : Fintype α] [_G : Fintype β] : card α = card β
 /-- Note: this lemma is specifically about `Fintype.ofSubsingleton`. For a statement about
 arbitrary `Fintype` instances, use either `Fintype.card_le_one_iff_subsingleton` or
 `Fintype.card_unique`. -/
-@[simp]
 theorem card_ofSubsingleton (a : α) [Subsingleton α] : @Fintype.card _ (ofSubsingleton a) = 1 :=
   rfl
 
@@ -204,7 +203,6 @@ theorem card_unique [Unique α] [h : Fintype α] : Fintype.card α = 1 :=
 
 /-- Note: this lemma is specifically about `Fintype.ofIsEmpty`. For a statement about
 arbitrary `Fintype` instances, use `Fintype.card_eq_zero`. -/
-@[simp]
 theorem card_ofIsEmpty [IsEmpty α] : @Fintype.card α Fintype.ofIsEmpty = 0 :=
   rfl