Commit 2026-09-11 21:15 781030d2

chore(CategoryTheory/Limits/Shapes/Products): use to_dual (#43542) This PR uses to_dual to generate categorical coproducts from products.

• The command insert_to_dual_translation is added, analogous to insert_to_additive_translation. This is used to tell to_dual how to translate a namespace when the namespace doesn't correspond to an existing declaration.
• The lemma Pi.lift_π is renamed to Pi.lift_comp_π, to make room for a new simp lemma Pi.lift_π that was missing and that fits the name better.