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