z : ℤ
⊢ ¬z * z % ↑4 = 2 % ↑4
z : ℤ
⊢ z * z % 4 ≠ 2
suffices ¬z * z % (4 : ℕ) = 2 % (4 : ℕ) by exact this
z : ℤ
⊢ ¬↑(z * z) = ↑2
z : ℤ
⊢ ¬z * z % ↑4 = 2 % ↑4
rw [← ZMod.int_cast_eq_int_cast_iff']
no goals
z : ℤ
⊢ ¬↑(z * z) = ↑2
simpa using sq_ne_two_fin_zmod_four _
no goals
z : ℤ
this : ¬z * z % ↑4 = 2 % ↑4
⊢ z * z % 4 ≠ 2
exact this