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)⁆
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)⁆
rw [add_mul, add_mul]
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)⁆
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)⁆
iterate 6 rw [mul_add]
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)⁆
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)⁆
iterate 10 rw [map_add]
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)⁆
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)⁆
rw [IsCommJordan.mul_comm b a, IsCommJordan.mul_comm c a, IsCommJordan.mul_comm c b]
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))⁆
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)⁆
iterate 3 rw [two_smul]
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)⁆))
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))⁆
simp only [lie_add, add_lie, commute_lmul_lmul_sq, zero_add, add_zero]
no goals
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)⁆))
abel
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)⁆
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)⁆
rw [mul_add]
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)⁆
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)⁆
rw [map_add]
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))⁆
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)⁆
rw [two_smul]