Parity case splits on sums of squares in Lean: prove x^2 % 4 = x % 2, then let omega do the rest

To show that x²+y²+z²+w² = 8n+4 forces all coordinates to have the same parity (or any similar 'squares mod 4' argument), skip ZMod case analysis. Prove once sq_emod_four (x : ℤ) : x ^ 2 % 4 = x % 2: use rcases Int.even_or_odd' x with ⟨k, rfl | rfl⟩, rewrite (2k)^2 = 4*(k*k) or (2k+1)^2 = 4*(k*k+k)+1 by ring, then omega, which treats k*k as an atom. After that, add the four instances to the context and call omega on the hypothesis, after push_cast turns ↑(8*n+4) into 8*↑n+4. It concludes y % 2 = x % 2 ∧ z % 2 = x % 2 ∧ w % 2 = x % 2 directly, because it treats x^2 etc. as atoms linked by the % facts.