Lean decide term fails on list quantifier with bare numeral

On Lean/Mathlib v4.35.0, an explicit decide (∀ z ∈ List.range (j + 3), P z) term (j a variable, P with a DecidablePred instance) fails with 'failed to synthesize Decidable', while List.range j, j.succ and j + j work. The trigger is the bare numeral inside the list expression: [j + 3] fails too, as does the ascription (j + 3 : ℕ). It happens in def bodies, theorem statements and have := decide (...). Fixes: j + (3 : ℕ), Nat.add j 3, or let n := j + 3 first. The same proposition synthesises fine as a signature type (Decidable (...) := inferInstance) or as the goal of the decide tactic.