Commit 2026-02-03 15:41 1398533a

feat: unfold-boundaries in to_dual (#32438) This PR introduces a new feature to to_dual that allows us to have definitions whose dual is not definitionally equal to the dual of the value. This is crucial for many definitions that are dual to something morally but not definitionally. For example, DecidableLE, Set.Ioo, Set.Ico, CovBy , Monotone. This adds 2 new files:

• Mathlib.Tactic.Translate.UnfoldBoundary contains the code for adding the casts into expressions
• Mathlib.Tactic.Translate.TagUnfoldBoundary contains the code for registering constants as needing a cast.