A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ + ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ + ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
        (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆)
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
        (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆)
rw [(commute_lmul_lmul_sq a).lie_eq, (commute_lmul_lmul_sq b).lie_eq,
  (commute_lmul_lmul_sq c).lie_eq, zero_add, add_zero, add_zero]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + 2 • ⁅↑L a, ↑L (a * b)⁆ + 2 • ⁅↑L a, ↑L (c * a)⁆ + 2 • ⁅↑L a, ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (c * c)⁆ + 2 • ⁅↑L b, ↑L (a * b)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ +
          2 • ⁅↑L b, ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆ + 2 • ⁅↑L c, ↑L (c * a)⁆ +
        2 • ⁅↑L c, ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
        (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆)
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ + ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ + ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
        (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆)
simp only [lie_nsmul]
no goals
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + 2 • ⁅↑L a, ↑L (a * b)⁆ + 2 • ⁅↑L a, ↑L (c * a)⁆ + 2 • ⁅↑L a, ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (c * c)⁆ + 2 • ⁅↑L b, ↑L (a * b)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ +
          2 • ⁅↑L b, ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆ + 2 • ⁅↑L c, ↑L (c * a)⁆ +
        2 • ⁅↑L c, ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
        (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆)
abel