induction' k with b hb
case left
a b c : ℤθ
k : ℕ
⊢ (↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0
case left.zero
a b c : ℤθ
⊢ (↑(unit ^ (3 * ↑Nat.zero))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑Nat.zero))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑Nat.zero))).h % 3 = 0

case left.succ
a b✝ c : ℤθ
b : ℕ
hb : (↑(unit ^ (3 * ↑b))).f % 3 = 1 ∧ (↑(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