theorem lie_jacobi_swap {L : Type u_1} [LieRing L] (x y z : L) : ⁅⁅x, y⁆, z⁆ + ⁅⁅y, z⁆, x⁆ + ⁅⁅z, x⁆, y⁆ = 0