∀ {L₁ : Type u_1} {L₂ : Type u_2} [inst : LieRing L₁] [inst_1 : LieRing L₂] (x y z : L₁ × L₂),
  (⁅x.1, (⁅y.1, z.1⁆, ⁅y.2, z.2⁆).1⁆, ⁅x.2, (⁅y.1, z.1⁆, ⁅y.2, z.2⁆).2⁆) =
    (⁅(⁅x.1, y.1⁆, ⁅x.2, y.2⁆).1, z.1⁆, ⁅(⁅x.1, y.1⁆, ⁅x.2, y.2⁆).2, z.2⁆) +
      (⁅y.1, (⁅x.1, z.1⁆, ⁅x.2, z.2⁆).1⁆, ⁅y.2, (⁅x.1, z.1⁆, ⁅x.2, z.2⁆).2⁆)