question about Mechanics of Proofs exercise 4.4.6.2

Stream: new members

[Hao Wu]

Hi guys, I'm trying to resolve this exercise in Mechanics of Proofs
however got unsolved goals at last contradiction check 'numbers at H', it seems it failed when using ZMOD for bigger numbers ?
the exercise is here : https://hrmacbeth.github.io/math2001/04_Proofs_with_Structure_II.html#id32

example (n : ℤ) (hn : n ^ 2 ≡ 4 [ZMOD 5]) : n ≡ 2 [ZMOD 5] ∨ n ≡ 3 [ZMOD 5] := by
  mod_cases h : n % 5
  · -- case 1: `n ≡ 0 [ZMOD 5]`
    have H :=
    calc
      0 ≡ 0 + 5*0 [ZMOD 5] := by extra
      _ = 0 ^ 2 := by numbers
      _ ≡  n^2 [ZMOD 5] := by rel [h]
      _ ≡ 4[ZMOD 5] := by rel [hn]
    numbers at H
  · -- case 2: `n ≡ 1 [ZMOD 5]`
    have H :=
    calc
      1 ≡ 1 + 5*0 [ZMOD 5] := by extra
      _ = 1 ^2 := by numbers
      _ ≡ n^2 [ZMOD 5] := by rel [h]
      _ ≡ 4 [ZMOD 5] := by rel [hn]
    numbers at H
  · -- case 3: `n ≡ 2 [ZMOD 5]`
    left
    apply h
  · -- case 4: `n ≡ 3 [ZMOD 5]`
    right
    apply h
  · -- case 5: `n ≡ 4 [ZMOD 5]`
    have H :=
    calc
      16 ≡ 16 + 5*0 [ZMOD 5] := by extra
      _ = 4 ^2 := by numbers
      _ ≡ n^2 [ZMOD 5] := by rel [h]
      _ ≡ 4 [ZMOD 5] := by rel [hn]
    numbers at H

Thanks in advance