simp only [mul, add]
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝², g := g✝², h := h✝² } (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) =
    add (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.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ { f := f✝² * (f✝¹ + f✝) + 6 * h✝² * (h✝¹ + h✝) - 2 * g✝² * (h✝¹ + h✝) - 2 * h✝² * (g✝¹ + g✝),
      g := f✝² * (g✝¹ + g✝) + g✝² * (f✝¹ + f✝) + 16 * h✝² * (h✝¹ + h✝) - 6 * g✝² * (h✝¹ + h✝) - 6 * h✝² * (g✝¹ + g✝),
      h :=
        f✝² * (h✝¹ + h✝) + h✝² * (f✝¹ + f✝) + g✝² * (g✝¹ + g✝) + 3 * h✝² * (h✝¹ + h✝) - 3 * g✝² * (h✝¹ + h✝) -
          3 * h✝² * (g✝¹ + g✝) } =
    {
      f :=
        f✝² * f✝¹ + 6 * h✝² * h✝¹ - 2 * g✝² * h✝¹ - 2 * h✝² * g✝¹ +
          (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✝¹ +
          (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✝² * h✝ + h✝² * f✝ + g✝² * g✝ + 3 * h✝² * h✝ - 3 * g✝² * h✝ - 3 * h✝² * g✝) }