rw [← add_assoc] at hk
case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ (k + 1))).f = 1 + 3 ^ (k + 1) + 3 ^ (k + (1 + 1)) * a ∧
      (↑(unit ^ 3 ^ (k + 1))).g = 3 ^ (k + (1 + 1)) * b ∧
        (↑(unit ^ 3 ^ (k + 1))).h = 3 ^ (k + 1) + 3 ^ (k + (1 + 1)) * c
l : k + 1 = Nat.succ k
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ (Nat.succ k + 1))).f = 1 + 3 ^ (Nat.succ k + 1) + 3 ^ (Nat.succ k + 2) * a ∧
      (↑(unit ^ 3 ^ (Nat.succ k + 1))).g = 3 ^ (Nat.succ k + 2) * b ∧
        (↑(unit ^ 3 ^ (Nat.succ k + 1))).h = 3 ^ (Nat.succ k + 1) + 3 ^ (Nat.succ k + 2) * c
case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ (k + 1))).f = 1 + 3 ^ (k + 1) + 3 ^ (k + 1 + 1) * a ∧
      (↑(unit ^ 3 ^ (k + 1))).g = 3 ^ (k + 1 + 1) * b ∧ (↑(unit ^ 3 ^ (k + 1))).h = 3 ^ (k + 1) + 3 ^ (k + 1 + 1) * c
l : k + 1 = Nat.succ k
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ (Nat.succ k + 1))).f = 1 + 3 ^ (Nat.succ k + 1) + 3 ^ (Nat.succ k + 2) * a ∧
      (↑(unit ^ 3 ^ (Nat.succ k + 1))).g = 3 ^ (Nat.succ k + 2) * b ∧
        (↑(unit ^ 3 ^ (Nat.succ k + 1))).h = 3 ^ (Nat.succ k + 1) + 3 ^ (Nat.succ k + 2) * c