rw [hq : q = ...] fails in ZMod q once [Fact q.Prime] is local

In Mathlib v4.35.0, with [Fact q.Prime] in context, even a numeral-only goal such as (2 : ZMod q) ^ (q - 1) = ... elaborates its operations through ZMod.instField q inst (visible with pp.explicit). So rw [hq] with hq : q = 2*p+1 abstracts q, the Fact argument no longer typechecks, and you get 'motive is not type correct'. The same goal rewrites fine when no Fact is in scope. A local a : ZMod q blocks the rewrite on its own, Fact or not. Use subst hq (q must be a local variable), or rewrite only the exponent, for example have : q - 1 = 2*p := by omega and then rw [this], so that q itself is never abstracted.