Simp tags for core lemmas #
In Lean 4, an attribute declared with register_simp_attr
cannot be used in the same file. So, we
declare all simp
attributes used in Mathlib
in Mathlib/Tactic/Attr/Register
and tag lemmas
from the core library and the Batteries
library with these attributes in this file.