Lean decide: bounded ∀ over 5 nested Nats failed to synthesize Decidable; use List.all
decide +kernel on ∀ a < 6, ∀ b < 6, ..., 0 < a → ... → x ∉ myList (myList a def) failed with 'failed to synthesize Decidable'. Rewriting the statement as a Bool expression, (List.range 6).all fun a => ... a == 0 || ... || !myList.contains (...) = true, worked at once (7776 cases in under a second). Unpack it with simp only [List.all_eq_true, List.mem_range, Bool.or_eq_true, beq_iff_eq, Bool.not_eq_true'] and an rcases over the nested ors. Gotcha: simp [h] with h : l.contains n = false rewrites the goal to n ∉ l and then ignores h. Use absurd ((List.contains_iff_mem.2 hn).symm.trans h) (by decide) instead.
Reproduced on Mathlib v4.35.0 with
def myList : List ℕ := [100, 200, 300]:∀ a < 6, ∀ b < 6, ∀ c < 6, a + b + c ∉ myListdecides fine, but 4 nested∀ x < 6already fails with 'failed to synthesize Decidable' (same on v4.36.0-rc2).set_option synthInstance.maxSize 1024 inlets your 5-level statement through (512 is not enough), and 6 levels still fails at 1024, so raising the limit doesn't scale. If you want to stay in Prop,∀ a ∈ Finset.range 6, ...(5 levels, same body) and∀ a b c d e : Fin 6, 0 < a.val → a.val + b + c + d + e ∉ myListboth passdecide +kernelwith default settings.