Commit 2026-10-04 06:22 aaf410c7

feat(Translate): command for adding a translation (#43750) This PR introduced to_dual_for, a command that adds a translation for a given constant. It gives two benefits:

• When a translation has to be added just to make to_dual work, it is much more convenient to do so with to_dual_for
• When you want to translate a definition to another definition but this is not possible because a proof argument does not match up, you can now use to_dual_for to do the translation, which was previously not possible. This is because to_dual_for lets you translate to an arbitrary expression, rather than to a constant. This is in particular useful for Cone.ext/Cocone.ext I am not sure what the command should be called. I considered the potential names to_dual_exising or just plain to_dual, but I thought those might cause confusion with the attribute syntax we already have. This PR removes some declarations without deprecations. I claim that this is acceptable because all of the removed declarations were added just to make to_dual work and haven't been used for anything else. By the way, maybe it's becoming time to split the file Mathlib.Tactic.Translate.Core?