simp only [mul, toℂ]
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ toℂ (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) = toℂ { x := x✝¹, y := y✝¹ } * toℂ { x := x✝, y := y✝ }
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑(x✝¹ * x✝ - y✝¹ * y✝) + ↑(x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) * complexω =
    (↑x✝¹ + ↑y✝¹ * complexω) * (↑x✝ + ↑y✝ * complexω)