A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑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)⁆)) =
    0
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑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)⁆) =
    2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆
rw [add_left_eq_self]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
        (⁅↑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)⁆)) =
    0
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑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)⁆)) =
    0
conv_lhs => enter [1, 1, 2, 2, 2]; rw [IsCommJordan.mul_comm a b]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * c)⁆ + ⁅↑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)⁆)) =
    0
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
        (⁅↑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)⁆)) =
    0
conv_lhs => enter [1, 2, 2, 2, 1]; rw [IsCommJordan.mul_comm c a]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (c * b)⁆)) =
    0
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * c)⁆ + ⁅↑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)⁆)) =
    0
conv_lhs => enter [   2, 2, 2, 2]; rw [IsCommJordan.mul_comm b c]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L c⁆ + ⁅↑L (c * c), ↑L a⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (⁅↑L (b * b), ↑L c⁆ + ⁅↑L (c * c), ↑L b⁆)) =
    0
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (c * b)⁆)) =
    0
iterate 3 rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (-⁅↑L b, ↑L (a * a)⁆ + -⁅↑L a, ↑L (b * b)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (-⁅↑L c, ↑L (a * a)⁆ + -⁅↑L a, ↑L (c * c)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (-⁅↑L c, ↑L (b * b)⁆ + -⁅↑L b, ↑L (c * c)⁆)) =
    0
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L c⁆ + ⁅↑L (c * c), ↑L a⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (⁅↑L (b * b), ↑L c⁆ + ⁅↑L (c * c), ↑L b⁆)) =
    0
iterate 2 rw [← lie_skew (L (a * a)), ← lie_skew (L (b * b)), ← lie_skew (L (c * c))]
no goals
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (-⁅↑L b, ↑L (a * a)⁆ + -⁅↑L a, ↑L (b * b)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (-⁅↑L c, ↑L (a * a)⁆ + -⁅↑L a, ↑L (c * c)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (-⁅↑L c, ↑L (b * b)⁆ + -⁅↑L b, ↑L (c * c)⁆)) =
    0
abel
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L c⁆ + ⁅↑L (c * c), ↑L a⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (⁅↑L (b * b), ↑L c⁆ + ⁅↑L (c * c), ↑L b⁆)) =
    0
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L c⁆ + ⁅↑L (c * c), ↑L a⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (c * b)⁆)) =
    0
rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (-⁅↑L b, ↑L (a * a)⁆ + -⁅↑L a, ↑L (b * b)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (-⁅↑L c, ↑L (a * a)⁆ + -⁅↑L a, ↑L (c * c)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (-⁅↑L c, ↑L (b * b)⁆ + -⁅↑L b, ↑L (c * c)⁆)) =
    0
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (-⁅↑L b, ↑L (a * a)⁆ + -⁅↑L a, ↑L (b * b)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L c⁆ + -⁅↑L a, ↑L (c * c)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (⁅↑L (b * b), ↑L c⁆ + ⁅↑L (c * c), ↑L b⁆)) =
    0
rw [← lie_skew (L (a * a)), ← lie_skew (L (b * b)), ← lie_skew (L (c * c))]