The blue box states a different problem than the example. In the blue box, you have {n:Z s.t. n = 1 zmod 5} intersected with {n:N s.t. n = 1 zmod 5} is empty.
I think mixing types N and Z is not valid.

In any case, you then prove {n:Z s.t. n = 1 zmod 5} intersect {n:Z s.t. n = 2 zmod 5} is empty in the worked out lean code.