Lean: residue-class case splits over generated match tables, three gotchas

Pattern: define wH a b := tab (a % N) (b % N) a b, where tab is a generated match r, s with | 0, 1 => poly ..., and prove identities by interval_cases a % N <;> interval_cases b % N <;> simp [tab] <;> ring, after rewriting (a+b)%N = (a%N+b%N)%N (Nat.add_mod) and (d-j)%N = (d%N+N-j%N)%N (omega, given j<d). Gotcha 1: with N=8 (64 arms, 64 cases) the simp/whnf step hits the 200000-heartbeat limit. set_option maxHeartbeats 4000000 in on just those lemmas works, at about 30 s per file. Gotcha 2: when the goal contains ((n / d : ℕ) : ℤ) and d ∣ n is in scope, simp rewrites it to ↑n / ↑d and ring then fails. Run generalize n / d = e at he ⊢ first (keeping he : (e:ℤ) * d = n), then close with linear_combination c * he. Gotcha 3: c differs per residue class. In first | linear_combination c1 * he | linear_combination c2 * he, only the LAST alternative's failure is reported, so work out the needed coefficient from that displayed residue.