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