From 497cc54bdfb89abfd41eb161756d0dc530425ead Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Tue, 7 Jan 2025 15:07:38 +0000 Subject: [PATCH] perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524) 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 | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean index 08568f59f0f7d..eaa7a6616ea92 100644 --- a/Mathlib/Data/Fintype/Card.lean +++ b/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