sorry
case h
a b c : ℤθ
n : ℕ
ψ : ℤθ
hψ : ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * ψ
⊢ ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * (ψ + 3 ^ (n + 1) * ψ ^ 2 + 3 ^ (2 * n + 2) * ψ ^ 3)
no goals