@[to_dual] fails when a `Decidable` instance's argument is itself an `ite`

[kim-em]

import Mathlib.Order.Basic
import Mathlib.Tactic.Translate.ToDual

variable {β : Type*} [LinearOrder β]

-- succeeds
@[to_dual]
theorem control_max (a b : β) : (if a < b then b else a) = (if a < b then b else a) := rfl

-- fails
@[to_dual]
theorem nested_max (a b : β) :
    (if (if a < b then b else a) < b then b else a) =
      (if (if a < b then b else a) < b then b else a) := rfl

@[to_dual] failed to insert a cast to make `fun {β} [LinearOrder β] a b => rfl` have type ...

function expected
  LinearOrder.toDecidableLT (if a < b then b else a)

to_dual swaps the two arguments of LinearOrder.toDecidableLT, and UnfoldBoundary.insertBoundaries rebuilds applications one argument at a time (args.foldlM (mkAppWithCast b) f), so the intermediate one-argument application is ill-typed, mkAppWithCast falls through to its catch, and whnf (← inferType f) is not a pi.

to_dual already handles this correctly at the level of statements. Probing with

@[to_dual self]
theorem probe (x : β) : LinearOrder.toDecidableLT x = fun y => LinearOrder.toDecidableLT x y := rfl

shows it eta-expanding and swapping, producing (fun b ↦ LinearOrder.toDecidableLT b x) = fun y ↦ LinearOrder.toDecidableLT y x. So the machinery exists but is not reached from inside insertBoundaries. Eta-expanding a head constant to full arity before folding arguments into it, when to_dual reorders that constant's arguments, looks like it would be enough, though I have not tried it.

Note the proof above is rfl, so this does not involve grind.

In the wild: List.argmax_cons in Mathlib/Data/List/MinMax.lean, where rw [← apply_ite, ← apply_ite] produces exactly this shape. That proof was grind -abstractProof, and six @[to_dual] errors in the file cascaded from it. Worked around by replacing the grind with an explicit case analysis, in chore: adapt to grind homomorphisms in nightly-2026-08-13 on nightly-testing. That was only ever a workaround: the underlying hole predates the grind change, which merely altered the proof term so that it started hitting it.

cc @JovanGerb