rfl
a✝ b✝ c a b : ℤθ
⊢ a * b =
    { f := a.f * b.f + 6 * a.h * b.h - 2 * a.g * b.h - 2 * a.h * b.g,
      g := a.f * b.g + a.g * b.f + 16 * a.h * b.h - 6 * a.g * b.h - 6 * a.h * b.g,
      h := a.f * b.h + a.h * b.f + a.g * b.g + 3 * a.h * b.h - 3 * a.g * b.h - 3 * a.h * b.g }
no goals