Commit 2023-06-15 13:54 88474d1b
View on Github →chore(algebraic_geometry/Scheme): remove @[simps] from Spec (#19188)
The @[simps] on Spec produces lemmas that aren't needed in mathlib3, and get in the way in mathlib4. This backports the removal of this attribute, to match https://github.com/leanprover-community/mathlib4/pull/5040.