Commit 2026-07-08 18:17 463839db

feat(Translate): validate all translations (#40365) Make to_dual/to_additive validate all translations that are added. In particular, translations between fields of structures, and between lemmas generated by simps, are now validated. This will help catch translation problems. In the file Limits.Cones, the same issue with simps keeps arising due to how CategoryTheory.Iso interacts with to_dual. Ideally this could be fixed at the meta level to avoid these awkward workarounds. This PR also removes a heuristic in the name guessing algorithm for re-tagging declarations that were already tagged. After this PR, there won't be any reason anymore to re-tag declarations, so this heuristic can be removed. Additionally, the translateOverwrite linter is strengthened so that it always warns when overwriting an existing translation. Due to #40493, which added a universe metavariable unification, we now need to call processPostponed to ensure all universe metavariables will be assigned.