dsimp 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 ^ (2 + k * 3))).f =
      { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
          h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.f ∧
    (↑(unit ^ (2 + k * 3))).g =
        { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
            h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.g ∧
      (↑(unit ^ (2 + k * 3))).h =
        { f := -5 - j1 * 15 + j3 * 12 + j2 * 24, g := -14 - j1 * 42 + j3 * 60 + j2 * 57,
            h := -4 - j1 * 12 + (j3 * 75 - j2 * 6) }.h
⊢ (↑(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 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w :
  (↑(unit ^ (2 + k * 3))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24 ∧
    (↑(unit ^ (2 + k * 3))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57 ∧
      (↑(unit ^ (2 + k * 3))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ (↑(unit ^ (3 * k + 2))).f % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).g % 3 = 1 ∧ (↑(unit ^ (3 * k + 2))).h % 3 = 2