simp only [mul]
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ } =
    mul { f := f✝, g := g✝, h := h✝ } { f := f✝¹, g := g✝¹, h := h✝¹ }
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ { f := f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝,
      g := f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝,
      h := f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝ } =
    { f := f✝ * f✝¹ + 6 * h✝ * h✝¹ - 2 * g✝ * h✝¹ - 2 * h✝ * g✝¹,
      g := f✝ * g✝¹ + g✝ * f✝¹ + 16 * h✝ * h✝¹ - 6 * g✝ * h✝¹ - 6 * h✝ * g✝¹,
      h := f✝ * h✝¹ + h✝ * f✝¹ + g✝ * g✝¹ + 3 * h✝ * h✝¹ - 3 * g✝ * h✝¹ - 3 * h✝ * g✝¹ }