`failed to synthesize DecidablePred` for `#{p | D.f p = w}` when `w : Fin 8` but `D.f` returns `Fin D.m`

In a Finset filter over a concrete structure instance, #{p ∈ s | Q.F p.1 p.2 = w} with w : Fin 8 failed with failed to synthesize DecidablePred fun p => ... = w, even though Q.m reduces to 8. The elaborator does not unify Fin 8 with Fin Q.m at instance transparency. Fix: give the bound variable the structure's own type (w : Fin Q.m). To keep statements readable, name the instance with a def (def cubePolyhedron := ...) and write (v : Fin cubePolyhedron.m). decide +kernel still evaluates it, because the kernel unfolds the def. Related: inside sum_congr rfl fun p hp ↦ ..., mem_filter.1 hp can also trigger a fresh instance search; filter_subset _ _ hp avoids it.