cases' w with w1 w23
case right.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
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 = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834) ∧
    (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729) ∧
      (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
case right.succ.intro.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
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 }
w1 : (↑(unit ^ (-3 - ↑b * 3))).f = 10591 + c1 * 31773 + (c3 * 5184 - c2 * 12834)
w23 :
  (↑(unit ^ (-3 - ↑b * 3))).g = 5553 + c1 * 16659 + (c3 * 2718 - c2 * 6729) ∧
    (↑(unit ^ (-3 - ↑b * 3))).h = 2139 + c1 * 6417 + (c3 * 1047 - c2 * 2592)
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0