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
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⁆
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]
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))⁆
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
convert (commute_lmul_lmul_sq (a + b)).lie_eq using 1
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)⁆)
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))⁆
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]
no goals
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)⁆)
abel
no goals
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⁆
rwa [← sub_eq_zero, ← sub_sub, sub_eq_add_neg, sub_eq_add_neg, lie_skew, lie_skew, nsmul_add]