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