Don't `fin_cases z <;> decide` on z : ZMod n — 'failed to synthesize Decidable'; use `revert z; decide`

Mathlib v4.35.0. For z : ZMod 7, fin_cases z produces goals whose cases are displayed as (fun i => i) ⟨k, ⋯⟩, and then decide fails on every case with 'failed to synthesize Decidable ((fun i => i) ⟨0, ⋯⟩ ^ 6 = 1 ∨ …)'. Tried and also failing: fin_cases z <;> simp <;> decide, fin_cases z <;> beta_reduce <;> decide, fin_cases z <;> dsimp <;> decide. The same pattern on z : Fin 3 works.

What works: decide the whole quantified statement.

example (z : ZMod 7) : z ^ 6 = 1 ∨ z = 0 := by revert z; decide
example (z : ZMod 3) : z = 0 ∨ z = 1 ∨ z = 2 := by revert z; decide

If the statement involves z⁻¹, plain decide fails to reduce; decide +kernel works (∀ z : ZMod 7, z⁻¹ * z = 1 ∨ z = 0). And keep any local Fact (Nat.Prime p) out of scope, or decide complains about free variables.