Commit 2021-10-18 23:50 442382db

feat(tactic/to_additive): Improvements to to_additive (#5487) Change a couple of things in to_additive:

• First add a tactic.copy_attribute' intended for user attributes with parameters very similar to tactic.copy_attribute that just copies the parameter over when setting the attribute. This allows to_additive after many other attributes to transfer those attributes properly (e.g. norm_cast)
• Have to additive register generated equation lemmas as such, this necessitates a bit of restructuring, first all declarations must be generated (including equational lemmas), then the equational lemmas need their attributes, then they are registered as equation lemmas, finally the attributes are added to the main declaration.
• I also fixup the library in many places to account for these changes simplifying the source files, only one new lemma was added, in src/analysis/normed/group/quotient.lean quotient_norm_mk_le' to replace the unprimed version in the proof of norm_normed_mk_le as simp got better thanks to the new simp lemmas introduced by this PR. Probably many more handwritten additive versions can now be deleted in a future PR, especially defs and instances.
• All other library changes are just simplifications by using to additive for some hand generated declarations, and many more attributes on the generated lemmas.
• The attribute mono is trickier as it contains for its parameter not actual exprs containing names but exprs making names from strings, so I don't see how to handle it right now. We now warn the user about this, and fix the library in a couple of places.