Commit 2023-11-12 11:28 1fe87718

fix: attribute [simp] ... in -> attribute [local simp] ... in (#7678) Mathlib.Logic.Unique contains the line attribute [simp] eq_iff_true_of_subsingleton in ...: https://github.com/leanprover-community/mathlib4/blob/96a11c7aac574c00370c2b3dab483cb676405c5d/Mathlib/Logic/Unique.lean#L255-L256 Despite what the in part may imply, this adds the lemma to the simp set "globally", including for downstream files; it is likely that attribute [local simp] eq_iff_true_of_subsingleton in ... was meant instead (or maybe scoped simp, but I think "scoped" refers to the current namespace). Indeed, the relevant lemma is not marked with @[simp] for possible slowness: https://github.com/leanprover/std4/blob/846e9e1d6bb534774d1acd2dc430e70987da3c18/Std/Logic.lean#L749. Adding it to the simp set causes the example at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Regression.20in.20simp to slow down. This PR changes this and fixes the relevant downstream simps. There was also one ocurrence of attribute [simp] FullSubcategory.comp_def FullSubcategory.id_def in in Mathlib.CategoryTheory.Monoidal.Subcategory but that was much easier to fix. https://github.com/leanprover-community/mathlib4/blob/bc49eb9ba756a233370b4b68bcdedd60402f71ed/Mathlib/CategoryTheory/Monoidal/Subcategory.lean#L118-L119