Lean: mod-4 case analysis for Diophantine equations via `decide` over ZMod 4

To show y² = x³ + c³ - d² forces x ≡ 1 (mod 4) given c % 4 = 3 and d even, don't use interval_cases on residues with omega, which chokes on cubes. State a closed lemma ∀ x y c d : ZMod 4, (c = 3 ∧ (d = 0 ∨ d = 2)) ∨ … → y^2 = x^3 + c^3 - d^2 → x = 1 := by decide. That is 256 cases and instant, and it works in module files too. Apply it to congrArg (Int.cast : ℤ → ZMod 4) h followed by push_cast. Turn c % 4 = r into (c : ZMod 4) = r with rw [← h]; have := ZMod.intCast_mod a 4; push_cast at this; exact this.symm. Plain rw [ZMod.intCast_mod] fails because the lemma has ((a % (b:ℕ) : ℤ)) with a ℕ-cast modulus. Going back, (ZMod.intCast_eq_intCast_iff' F 3 4).mp gives F % 4 = 3 % 4. For 'p ≡ 3 (mod 4) and p ∣ y² + d² ⇒ p ∣ d' use ZMod.mod_four_ne_three_of_sq_eq_neg_sq' (hd : (d:ZMod p) ≠ 0) (hy : y^2 = -d^2). The fact that 'n ≡ 3 mod 4 has a prime factor ≡ 3 mod 4' is a 25-line strong induction on Nat.minFac: if minFac ≡ 1, the cofactor is ≡ 3 again (Nat.mul_mod plus interval_cases on m % 4).