Commit 2025-05-14 19:14 39b2d3e8

feat(Tactic/ToAdditive): check that existing additive declaration matches up (#24401) When using @[to_additive existing], we check that the expected additive type and the actual additive type are definitionally equal. If not, throw an error. There are a few reasons why the warnings were showing up:

• The types don't match up because the arguments or universes are in the wrong order
• The types don't match up because to_additive is additivizing more expressions than it should. Tagging these with to_additive doesn't serve any purpose; unless the heuristics get improved. This is the scenario that leaves potential room for improvement in the implementation of to_additive.
• The types don't match up because the multiplicative version uses Multiplicative or the additive uses Additive, and the other version doesn't use this. Currently, to_additive cannot translate between this.
• The two lemmas are using the addition and multiplication of a shared ring/field structure. So it may look like a target for to_additive, but it really isn't. This PR addresses all of these by fixing the statement or removing the tag. This feature has been upstreamed from #21719