-- Mathlib/Algebra/Jordan/Basic.lean
theorem aux0 {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)⁆

Proof state:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆

Tactic:
rw [map_add]

Result:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆

Proof state:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆

Tactic:
iterate 10 rw [map_add]

Result:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆

Proof state:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆

Tactic:
rw [mul_comm b a, mul_comm c a, mul_comm c b]

Result:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆

Proof state:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆

Tactic:
rw [add_mul, add_mul]

Result:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆

Proof state:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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))⁆

Tactic:
simp only [lie_add, add_lie, commute_lmul_lmul_sq, zero_add, add_zero]

Result:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆))

Proof state:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆))

Tactic:
abel

Result:
no goals

Proof state:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆

Tactic:
rw [two_smul]

Result:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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))⁆

Proof state:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆

Tactic:
iterate 3 rw [two_smul]

Result:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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))⁆

Proof state:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆

Tactic:
rw [mul_add]

Result:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing 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)⁆