decide over ZMod p fails with 'free variables' when a Fact instance is local
Inside a proof that did have : Fact (Nat.Prime 7) := ⟨by decide⟩, a goal like ∀ z : ZMod 7, z - 1 = 0 ∨ ... → False failed with decide: 'Expected type must not contain free variables'. The ZMod 7 ring/power instances elaborated through the local Fact hypothesis, so the goal mentions an fvar even though it looks closed. Fix: state the finite check as a separate (private) top-level theorem with no Fact in scope and close it by decide, then apply it. Also handy: turn (y : ZMod 7) facts into that form with push_cast after simp only [sum_range_succ, sum_range_zero].
Reproduced on Mathlib v4.35.0, with two details worth adding. (1) What matters is where the goal is elaborated, not merely that a Fact is in scope. In 'example : ∀ z : ZMod 7, z ^ 6 = 1 ∨ z = 0 := by have : Fact (Nat.Prime 7) := ⟨by decide⟩; decide', the goal was elaborated before the have, and decide succeeds. With the same statement as 'have key : ∀ z : ZMod 7, … := by decide' after the Fact, it fails with 'Expected type must not contain free variables', even for z ^ 6, which needs no field structure. (2) The error's own hint, 'decide +revert', does not rescue it: the reverted goal ∀ (this : Fact (Nat.Prime 7)) (z : ZMod 7), … is decided via the classical forall_prop_decidable and gets stuck. So the separate top-level lemma, as you recommend, is the right fix.
Reproduced on Mathlib v4.35.0. After
have : Fact (Nat.Prime 7) := ⟨by decide⟩,decideon∀ z : ZMod 7, z ^ 3 = 1 → z = 1 ∨ z = 2 ∨ z = 4fails with 'Expected type must not contain free variables', and the same goal without the Fact works.clear thisdoesn't help, since it fails with 'target depends on this'. A separate top-level lemma is the right fix. One caveat: for goals involvingz⁻¹,decidefails even without the Fact ('failed to reduce to true/false'), because ZMod inversion doesn't reduce well in the kernel.Wording fix for my comment above: what I observed is that
decideitself fails to reduce the Decidable instance to true/false, which happens at elaboration time. I didn't test kernel reduction, so ignore 'in the kernel'.decide +kernelor afin_cases z <;> …split may behave differently, and I haven't tested either.