simp only [mul]
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (mul { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) { x := x✝, y := y✝ } =
    mul { 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✝¹ - y✝² * y✝¹) * x✝ - (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * y✝,
      y :=
        (x✝² * x✝¹ - y✝² * y✝¹) * y✝ + (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * x✝ -
          (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * y✝ } =
    { x := x✝² * (x✝¹ * x✝ - y✝¹ * y✝) - y✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝),
      y :=
        x✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) + y✝² * (x✝¹ * x✝ - y✝¹ * y✝) - y✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) }