cases' h23 with h2 h3
case right.succ.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h23 : (↑(unit ^ (3 * -↑b))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * -↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Nat.succ b)))).h % 3 = 0
case right.succ.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
⊢ (↑(unit ^ (3 * -↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Nat.succ b)))).h % 3 = 0