mathlib

e3d9ab8f - feat(tactic/simps): store generated lemmas in attribute (#17964)

feat(tactic/simps): store generated lemmas in attribute (#17964) * `@[simps] def equiv.prod` now adds an attribute ``@[_simps_aux [`equiv.prod_apply, `equiv.prod_symm_apply]]`` to `equiv.prod` * Remark: the lemmas generated by `simps` can have `to_additive` attributes themselves, if the original declaration had a `to_additive` attribute (but it doesn't recurse any deeper than that) * Can be used by mathport to generate `#align` statements