Commit 2026-10-19 20:06 ca997990

fix(Translate): don't panic when existing is missing (#45049) This PR fixes the panic in @[to_dual] alias ... when the translation already exists. The problem was that we checked cfg.existing (i.e. whether the user wrote existing), instead of checking whether the translation actually already exists. Reported at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Order.20dual.20tactic/near/632686490