rw [this]
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 42 % 3 = 0
this✝ : 60 % 3 = 0
this : 57 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * (57 % 3) % 3) % 3 = 1
case intro.intro.intro.intro.intro.intro.intro.right.left
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 42 % 3 = 0
this✝ : 60 % 3 = 0
this : 57 % 3 = 0
⊢ (((-14 % 3 - j1 % 3 * 0 % 3) % 3 + j3 % 3 * 0 % 3) % 3 + j2 % 3 * 0 % 3) % 3 = 1