simp only [mul, add]
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul { x := x✝², y := y✝² } (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) =
    add (mul { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) (mul { x := x✝², y := y✝² } { x := x✝, y := y✝ })
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := x✝² * (x✝¹ + x✝) - y✝² * (y✝¹ + y✝), y := x✝² * (y✝¹ + y✝) + y✝² * (x✝¹ + x✝) - y✝² * (y✝¹ + y✝) } =
    { x := x✝² * x✝¹ - y✝² * y✝¹ + (x✝² * x✝ - y✝² * y✝),
      y := x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹ + (x✝² * y✝ + y✝² * x✝ - y✝² * y✝) }