dsimp at w
case intro.intro.intro.intro.intro
a b c : ℤθ
k j1 j2 j3 : ℤ
w :
  ↑(unit ^ (3 * k + 2)) =
    {
      f :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -5, g := -14, h := -4 }.f +
              6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.h -
            2 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.h -
          2 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.g,
      g :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -5, g := -14, h := -4 }.g +
                { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.f +
              16 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.h -
            6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.h -
          6 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.g,
      h :=
        { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.f * { f := -5, g := -14, h := -4 }.h +
                  { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.f +
                { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.g +
              3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.h -
            3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.g * { f := -5, g := -14, h := -4 }.h -
          3 * { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }.h * { f := -5, g := -14, h := -4 }.g }
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) * -5 + 6 * (3 * j3) * -4 - 2 * (3 * j2) * -4 - 2 * (3 * j3) * -14,
      g := (3 * j1 + 1) * -14 + 3 * j2 * -5 + 16 * (3 * j3) * -4 - 6 * (3 * j2) * -4 - 6 * (3 * j3) * -14,
      h := (3 * j1 + 1) * -4 + 3 * j3 * -5 + 3 * j2 * -14 + 3 * (3 * j3) * -4 - 3 * (3 * j2) * -4 - 3 * (3 * j3) * -14 }
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