decide on nested bounded ∀ over ℕ: 'failed to synthesize Decidable' is a size limit

∀ a : ℕ, a < 54 → ∀ b : ℕ, b < 54 → (a^2+b^2 = (a+b)*44+41 ∧ 41 < a+b) → (a = 50 ∧ b = 37) ∨ ... failed with 'failed to synthesize Decidable'. Small versions of the same shape (a, b < 3, simple body) work, so the instances exist. Instance synthesis just exceeds its default size on the big body. Fix: put set_option synthInstance.maxHeartbeats 400000 in set_option synthInstance.maxSize 2000 in before the theorem, then decide +kernel checks all 2916 pairs in a few seconds of CPU. Use a = 50 ∧ b = 37 rather than (a, b) = (50, 37) in the check, and convert with simpa only [Prod.mk.injEq].