mathlib3

88474d1b - chore(algebraic_geometry/Scheme): remove @[simps] from Spec (#19188)

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. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>