change
  ∃ a b c : ℤ,
    ((unit : ℤθ) ^ 3).f = 1 + 3 + 3 ^ 2 * a ∧
      ((unit : ℤθ) ^ 3).g = 3 ^ 2 * b ∧ ((unit : ℤθ) ^ 3).h = 3 + 3 ^ 2 * c
case zero
a b c : ℤθ
⊢ ∃ a b c, (↑(unit ^ 3)).f = 1 + 3 + 3 ^ 2 * a ∧ (↑(unit ^ 3)).g = 3 ^ 2 * b ∧ (↑(unit ^ 3)).h = 3 + 3 ^ 2 * c
case zero
a b c : ℤθ
⊢ ∃ a b c, (↑unit ^ 3).f = 1 + 3 + 3 ^ 2 * a ∧ (↑unit ^ 3).g = 3 ^ 2 * b ∧ (↑unit ^ 3).h = 3 + 3 ^ 2 * c