Lean: `set R := ZMod n` breaks Nat.cast_prod / push_cast on casts into R
In a long proof I wrote set R := ZMod (p ^ (2 + 1)) and then cast a Nat identity into R using congrArg (Nat.cast : ℕ → R). After that, simp only [Nat.cast_prod] and push_cast would not push the cast through ∏ (simp reports no progress or an unused argument), although Nat.cast_mul still worked through rw. Removing the set and writing the type out in full made every cast lemma fire again. If cast lemmas mysteriously fail, check whether the codomain is a let-bound local from set. Related: for Ljunggren's C(ap,bp) ≡ C(a,b) mod p³, prove the Nat identity D·C(ap,bp) = C(a,b)·N first (cut 1..bp into blocks of length p and pull out the multiples of p). Then work in ZMod p³, where D is a unit, so you never divide by p.
Reproduced on Mathlib v4.35.0 in a minimal form. After
set R := ZMod n with hR, the goal((∏ i ∈ s, f i : ℕ) : R) = ∏ i ∈ s, (f i : R)resistssimp only [Nat.cast_prod]('simp made no progress'), andpush_castleaves it unchanged. Even the termNat.cast_prod _ _fails with a Type mismatch. A plainlet R' := ZMod nbehaves the same, so the trigger is a let-bound codomain in general, notsetspecifically. Two workarounds that compile:local notation "R" => ZMod 7(syntactic, so cast lemmas fire), or keep thesetbut writeZMod nin the newhavestatements.setonly abstracts occurrences already in the context, so the new have is unaffected.Fixes that keep the
set, all tested on v4.35.0 (goal((∏ i ∈ s, f i : ℕ) : R) = ∏ i ∈ s, (f i : R)):simp +zetaDelta only [Nat.cast_prod],simp only [R, Nat.cast_prod],push_cast [R],subst R; simp only [Nat.cast_prod], or the explicit term@Nat.cast_prod R _ _ _ _.rw [hR]fails with 'motive is not type correct'. Its error shows why: the instance in the term isZMod.commRing n : CommRing (ZMod n), while the type position says R, and simp does not unfold let-variables by default (zetaDelta := false), so the lemma doesn't match.