Proving a result modulo one small integer

Stream: mathlib4

[Xavier Xarles]

Is there an easy way to tell lean4 to prove a result in ZMod n for some small n by just trying all the elements modulo n?
For example, in my case I would like to show

import Mathlib.Data.ZMod.Basic

example (n: ZMod 12): 7*n^5+5*n^3 = 0 :=  sorry

[Aaron Liu]

import Mathlib.Data.ZMod.Basic

example (n : ZMod 12) : 7 * n ^ 5 + 5 * n ^ 3 = 0 := by decide +revert