rw [ℤθ.ext_iff] at w
case left.succ.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
c1 : ℤ
hc1 : (↑(unit ^ (3 * b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * b))).h = 3 * c3
s : ↑(unit ^ (3 * b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w :
  ↑(unit ^ (3 + b * 3)) =
    { f := -23 - c1 * 69 + c3 * 108 + c2 * 90, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
      h := -15 - c1 * 45 + (c3 * 363 - c2 * 54) }
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
case left.succ.intro.intro.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
c1 : ℤ
hc1 : (↑(unit ^ (3 * b))).f = 3 * c1 + 1
c2 : ℤ
hc2 : (↑(unit ^ (3 * b))).g = 3 * c2
c3 : ℤ
hc3 : (↑(unit ^ (3 * b))).h = 3 * c3
s : ↑(unit ^ (3 * b)) = { f := 3 * c1 + 1, g := 3 * c2, h := 3 * c3 }
w :
  (↑(unit ^ (3 + b * 3))).f =
      { f := -23 - c1 * 69 + c3 * 108 + c2 * 90, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
          h := -15 - c1 * 45 + (c3 * 363 - c2 * 54) }.f ∧
    (↑(unit ^ (3 + b * 3))).g =
        { f := -23 - c1 * 69 + c3 * 108 + c2 * 90, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
            h := -15 - c1 * 45 + (c3 * 363 - c2 * 54) }.g ∧
      (↑(unit ^ (3 + b * 3))).h =
        { f := -23 - c1 * 69 + c3 * 108 + c2 * 90, g := -63 - c1 * 189 + c3 * 414 + c2 * 201,
            h := -15 - c1 * 45 + (c3 * 363 - c2 * 54) }.h
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0