have w :
  ((unit ^ (3 * k + 1) : ℤθˣ) : ℤθ) = ((unit ^ (3 * k) : ℤθˣ) : ℤθ) * ((unit ^ 1 : ℤθˣ) : ℤθ) :=
  by
  rw [zpow_add]
  norm_cast
a b c : ℤθ
k : ℤ
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2
a b c : ℤθ
k : ℤ
w : ↑(unit ^ (3 * k + 1)) = ↑(unit ^ (3 * k)) * ↑(unit ^ 1)
⊢ (↑(unit ^ (3 * k + 1))).f % 3 = 2 ∧ (↑(unit ^ (3 * k + 1))).g % 3 = 0 ∧ (↑(unit ^ (3 * k + 1))).h % 3 = 2