[GOAL]
A : Type u_1
inst✝¹ : Mul A
inst✝ : IsCommJordan A
a b : A
⊢ a * b * a = a * (b * a)
[PROOFSTEP]
rw [IsCommJordan.mul_comm, IsCommJordan.mul_comm a b]
[GOAL]
A : Type u_1
inst✝¹ : Mul A
inst✝ : IsCommJordan A
a b : A
⊢ a * a * (a * b) = a * (a * a * b)
[PROOFSTEP]
rw [IsCommJordan.mul_comm (a * a) (a * b), IsCommJordan.lmul_comm_rmul_rmul, IsCommJordan.mul_comm b (a * a)]
[GOAL]
A : Type u_1
inst✝¹ : Mul A
inst✝ : IsCommJordan A
a b : A
⊢ a * a * (b * a) = a * a * b * a
[PROOFSTEP]
rw [IsCommJordan.mul_comm (a * a) (b * a), IsCommJordan.mul_comm b a, IsCommJordan.lmul_comm_rmul_rmul,
  IsCommJordan.mul_comm, IsCommJordan.mul_comm b (a * a)]
[GOAL]
A : Type u_1
inst✝¹ : Mul A
inst✝ : IsCommJordan A
a b : A
⊢ b * a * (a * a) = b * (a * a) * a
[PROOFSTEP]
rw [IsCommJordan.mul_comm b a, IsCommJordan.lmul_comm_rmul_rmul, IsCommJordan.mul_comm]
[GOAL]
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * b * a = a * (b * a)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * a * (a * b) = a * (a * a * b)
[PROOFSTEP]
rw [mul_assoc, mul_assoc]
[GOAL]
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * a * (b * a) = a * a * b * a
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * b * (a * a) = a * (b * (a * a))
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ b * a * (a * a) = b * (a * a) * a
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) = ⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆
[PROOFSTEP]
suffices 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0 by
  rwa [← sub_eq_zero, ← sub_sub, sub_eq_add_neg, sub_eq_add_neg, lie_skew, lie_skew, nsmul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅↑L a, ↑L (a * b)⁆ + 2 • ⁅↑L b, ↑L (b * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ = 0
⊢ 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) = ⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆
[PROOFSTEP]
rwa [← sub_eq_zero, ← sub_sub, sub_eq_add_neg, sub_eq_add_neg, lie_skew, lie_skew, nsmul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • ⁅↑L a, ↑L (a * b)⁆ + 2 • ⁅↑L b, ↑L (b * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ = 0
[PROOFSTEP]
convert (commute_lmul_lmul_sq (a + b)).lie_eq using 1
[GOAL]
case h.e'_2
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • ⁅↑L a, ↑L (a * b)⁆ + 2 • ⁅↑L b, ↑L (b * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ =
    ⁅↑L (a + b), ↑L ((a + b) * (a + b))⁆
[PROOFSTEP]
simp only [add_mul, mul_add, map_add, lie_add, add_lie, IsCommJordan.mul_comm b a, (commute_lmul_lmul_sq a).lie_eq,
  (commute_lmul_lmul_sq b).lie_eq, zero_add, add_zero, two_smul]
[GOAL]
case h.e'_2
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
⊢ ⁅↑L a, ↑L (a * b)⁆ + ⁅↑L a, ↑L (a * b)⁆ + (⁅↑L b, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) + ⁅↑L b, ↑L (a * a)⁆ +
      ⁅↑L a, ↑L (b * b)⁆ =
    ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
      (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L a, ↑L (b * b)⁆)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
⊢ ⁅↑L a, ↑L (a * b)⁆ + ⁅↑L a, ↑L (a * b)⁆ + (⁅↑L b, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) + ⁅↑L b, ↑L (a * a)⁆ +
      ⁅↑L a, ↑L (b * b)⁆ =
    ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
      (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L a, ↑L (b * b)⁆)
[PROOFSTEP]
abel
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L ((a + b + c) * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [add_mul, add_mul]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * (a + b + c) + b * (a + b + c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
iterate 6 rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * (a + b + c) + b * (a + b + c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * (a + b) + a * c + b * (a + b + c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + b * (a + b + c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + (b * (a + b) + b * c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * (a + b) + c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
iterate 10 rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b) + ↑L c, ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a + a * b + a * c + (b * a + b * b + b * c)) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a + a * b + a * c) + ↑L (b * a + b * b + b * c) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a + a * b) + ↑L (a * c) + ↑L (b * a + b * b + b * c) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + ↑L (b * a + b * b + b * c) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (b * a + b * b) + ↑L (b * c)) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (b * a) + ↑L (b * b) + ↑L (b * c)) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (b * a) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (c * a + c * b) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (b * a) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (c * a) + ↑L (c * b) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [IsCommJordan.mul_comm b a, IsCommJordan.mul_comm c a, IsCommJordan.mul_comm c b]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (a * b) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (a * c) + ↑L (b * c) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (a * c) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
iterate 3 rw [two_smul]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (a * b) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (a * c) + ↑L (b * c) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (a * c) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [two_smul]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (a * b) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (a * c) + ↑L (b * c) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + (↑L (a * b) + ↑L (a * b)) + 2 • ↑L (a * c) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [two_smul]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (a * b) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (a * c) + ↑L (b * c) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + (↑L (a * b) + ↑L (a * b)) + (↑L (a * c) + ↑L (a * c)) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [two_smul]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (a * b) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (a * c) + ↑L (b * c) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + (↑L (a * b) + ↑L (a * b)) + (↑L (a * c) + ↑L (a * c)) +
        (↑L (b * c) + ↑L (b * c))⁆
[PROOFSTEP]
simp only [lie_add, add_lie, commute_lmul_lmul_sq, zero_add, add_zero]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L c, ↑L (a * a)⁆ +
            (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆) +
        (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆ +
            (⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L c, ↑L (b * b)⁆) +
          (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆ +
          (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (c * c)⁆)) =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L c, ↑L (a * a)⁆ +
              (⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L c, ↑L (b * b)⁆) +
            (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (c * c)⁆) +
          (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆ +
            (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆)) +
        (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆ +
          (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆)) +
      (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆ +
        (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
abel
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L c, ↑L (a * a)⁆ +
            (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆) +
        (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆ +
            (⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L c, ↑L (b * b)⁆) +
          (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆ +
          (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (c * c)⁆)) =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L c, ↑L (a * a)⁆ +
              (⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L c, ↑L (b * b)⁆) +
            (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (c * c)⁆) +
          (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆ +
            (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆)) +
        (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆ +
          (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆)) +
      (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆ +
        (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
abel
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [add_lie, add_lie]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
        ⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
iterate 15 rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
        ⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a)⁆ + ⁅↑L a, 2 • ↑L (b * c)⁆ +
        ⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ + ⁅↑L a, 2 • ↑L (b * c)⁆ +
        ⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a) + ↑L (b * b) + ↑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 * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * 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 * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
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 * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
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 * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a)⁆ + ⁅↑L b, 2 • ↑L (b * c)⁆) +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
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 * b) + ↑L (c * c) + 2 • ↑L (a * b)⁆ + ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
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 * 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 (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
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 * 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 (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
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 (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
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 (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a)⁆ + ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
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 (b * b) + ↑L (c * c) + 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
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 (b * b) + ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
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 (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 (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)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
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)⁆)
[PROOFSTEP]
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]
[GOAL]
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)⁆)
[PROOFSTEP]
simp only [lie_nsmul]
[GOAL]
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)⁆)
[PROOFSTEP]
abel
[GOAL]
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)⁆)
[PROOFSTEP]
abel
[GOAL]
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)⁆
[PROOFSTEP]
rw [add_left_eq_self]
  -- Porting note: was `nth_rw` instead of `conv_lhs`
[GOAL]
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
[PROOFSTEP]
conv_lhs => enter [1, 1, 2, 2, 2]; rw [IsCommJordan.mul_comm a b]
[GOAL]
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)⁆))
[PROOFSTEP]
enter [1, 1, 2, 2, 2]; rw [IsCommJordan.mul_comm a b]
[GOAL]
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)⁆))
[PROOFSTEP]
enter [1, 1, 2, 2, 2]; rw [IsCommJordan.mul_comm a b]
[GOAL]
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)⁆))
[PROOFSTEP]
enter [1, 1, 2, 2, 2]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L b, ↑L (a * b)⁆
[PROOFSTEP]
rw [IsCommJordan.mul_comm a b]
[GOAL]
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
[PROOFSTEP]
conv_lhs => enter [1, 2, 2, 2, 1]; rw [IsCommJordan.mul_comm c a]
[GOAL]
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)⁆))
[PROOFSTEP]
enter [1, 2, 2, 2, 1]; rw [IsCommJordan.mul_comm c a]
[GOAL]
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)⁆))
[PROOFSTEP]
enter [1, 2, 2, 2, 1]; rw [IsCommJordan.mul_comm c a]
[GOAL]
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)⁆))
[PROOFSTEP]
enter [1, 2, 2, 2, 1]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L a, ↑L (c * a)⁆
[PROOFSTEP]
rw [IsCommJordan.mul_comm c a]
[GOAL]
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
[PROOFSTEP]
conv_lhs => enter [2, 2, 2, 2]; rw [IsCommJordan.mul_comm b c]
[GOAL]
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)⁆))
[PROOFSTEP]
enter [2, 2, 2, 2]; rw [IsCommJordan.mul_comm b c]
[GOAL]
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)⁆))
[PROOFSTEP]
enter [2, 2, 2, 2]; rw [IsCommJordan.mul_comm b c]
[GOAL]
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)⁆))
[PROOFSTEP]
enter [2, 2, 2, 2]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L c, ↑L (b * c)⁆
[PROOFSTEP]
rw [IsCommJordan.mul_comm b c]
[GOAL]
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
[PROOFSTEP]
iterate 3 rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]
[GOAL]
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
[PROOFSTEP]
rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]
[GOAL]
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)⁆ + 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
[PROOFSTEP]
rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]
[GOAL]
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
[PROOFSTEP]
rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]
[GOAL]
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
[PROOFSTEP]
iterate 2 rw [← lie_skew (L (a * a)), ← lie_skew (L (b * b)), ← lie_skew (L (c * c))]
[GOAL]
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
[PROOFSTEP]
rw [← lie_skew (L (a * a)), ← lie_skew (L (b * b)), ← lie_skew (L (c * c))]
[GOAL]
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
[PROOFSTEP]
rw [← lie_skew (L (a * a)), ← lie_skew (L (b * b)), ← lie_skew (L (c * c))]
[GOAL]
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
[PROOFSTEP]
abel
[GOAL]
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
[PROOFSTEP]
abel
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 2 • (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (c * a)⁆ + ⁅↑L c, ↑L (a * b)⁆) = 0
[PROOFSTEP]
symm
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 = 2 • (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (c * a)⁆ + ⁅↑L c, ↑L (a * b)⁆)
[PROOFSTEP]
calc
  0 = ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆ := by rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]
  _ = _ := by rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 = ⁅↑L (a + b + c), ↑L ((a + b + c) * (a + b + c))⁆
[PROOFSTEP]
rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L ((a + b + c) * (a + b + c))⁆ = 2 • (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (c * a)⁆ + ⁅↑L c, ↑L (a * b)⁆)
[PROOFSTEP]
rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]
