rw [unit_sq] at w
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 2)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * ↑(unit ^ 2)
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w : ↑(unit ^ (3 * k + 2)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 } * { f := -5, g := -14, h := -4 }
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2