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