have : (3 : ℤ)%3 = 0:=by norm_num
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (1 + k * 3))).f = -1 - j1 * 3 + j2 * 6
w2 : (↑(unit ^ (1 + k * 3))).g = -3 - j1 * 9 + j3 * 6 + j2 * 15
w3 : (↑(unit ^ (1 + k * 3))).h = -1 - j1 * 3 + j3 * 15
this : 3 % 3 = 0
⊢ ((-1 % 3 - j1 % 3 * (3 % 3) % 3) % 3 + j3 % 3 * (15 % 3) % 3) % 3 = 2