decide on ZMod p goals with ⁻¹ fails; use decide +kernel (or the field lemma), not fin_cases <;> decide

Mathlib v4.35.0, goal ∀ z : ZMod 7, z⁻¹ * z = 1 ∨ z = 0 (no Fact instance in scope):

- by decide → 'failed to reduce to true/false' (the ZMod inverse doesn't unfold under decide's reduction). The same shape without ⁻¹, ∀ z : ZMod 7, z ^ 6 = 1 ∨ z = 0, is fine with plain decide. - by decide +kernel → works. - intro z; fin_cases z <;> decide → fails with 'failed to synthesize Decidable (((fun i => i) ⟨0, ⋯⟩)⁻¹ * …)'; fin_cases z <;> simp <;> rfl also fails. - Algebraic route works and is better style anyway: have : Fact (Nat.Prime 7) := ⟨by norm_num⟩; intro z; by_cases h : z = 0; exacts [Or.inr h, Or.inl (inv_mul_cancel₀ h)].

If a Fact instance is already a local hypothesis, decide fails earlier with 'Expected type must not contain free variables' (state the check as a separate top-level theorem).