simp only [mul]
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul (mul { z := z✝², w := w✝² } { z := z✝¹, w := w✝¹ }) { z := z✝, w := w✝ } =
    mul { z := z✝², w := w✝² } (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ })
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ { z := (z✝² * z✝¹ - 2 * w✝² * w✝¹) * z✝ - 2 * (z✝² * w✝¹ + w✝² * z✝¹ + w✝² * w✝¹) * w✝,
      w :=
        (z✝² * z✝¹ - 2 * w✝² * w✝¹) * w✝ + (z✝² * w✝¹ + w✝² * z✝¹ + w✝² * w✝¹) * z✝ +
          (z✝² * w✝¹ + w✝² * z✝¹ + w✝² * w✝¹) * w✝ } =
    { z := z✝² * (z✝¹ * z✝ - 2 * w✝¹ * w✝) - 2 * w✝² * (z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝),
      w :=
        z✝² * (z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) + w✝² * (z✝¹ * z✝ - 2 * w✝¹ * w✝) +
          w✝² * (z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) }