The sum of two squares is never congruent to 3 modulo 4

Enuntiatio — the claim

The sum of two squares is never congruent to 3 modulo 4

Refuted by Some non-negative integers a, b with (a^2 + b^2) % 4 == 3, i.e. a sum of two squares congruent to 3 mod 4.

Expressio — the formal statement

import Mathlib.Tactic

theorem residue_law_8a475b40329d : ∀ (a b : ℤ), (0 ≤ a) → (0 ≤ b) → ((a ≥ 0) ∧ (b ≥ 0)) → ((Int.emod ((a ^ (2 : ℕ)) + (b ^ (2 : ℕ))) 4) ≠ 3)

Demonstratio — the kernel-checked proof

by
  have key : ∀ (a b : ZMod 4), ((a ^ (2 : ℕ)) + (b ^ (2 : ℕ))) ≠ 3 := by decide
  intro a b _ha _hb _ h
  have h' : ((a ^ (2 : ℕ)) + (b ^ (2 : ℕ))) % 4 = 3 := h
  apply key ((a : ℤ) : ZMod 4) ((b : ℤ) : ZMod 4)
  have hz : ((((a ^ (2 : ℕ)) + (b ^ (2 : ℕ))) : ℤ) : ZMod 4) = ((3 : ℤ) : ZMod 4) := by
    rw [ZMod.intCast_eq_intCast_iff']
    simpa using h'
  push_cast at hz
  exact hz