-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b : A
h :
  HAdd.hAdd (β := AddMonoid.End A)
      (HAdd.hAdd (β := AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b)) :
              AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b)) :
              AddMonoid.End A) +
          HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b)) :
              AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b)) :
              AddMonoid.End A))
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * a)) :
          AddMonoid.End A))
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) (b * b)) :
        AddMonoid.End A) =
    HAdd.hAdd (α := AddMonoid.End A)
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * a)) :
          AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * b)) :
            AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * b)) :
            AddMonoid.End A)) +
      HAdd.hAdd (β := AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * b)) :
            AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * b)) :
            AddMonoid.End A))
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (b * b)) :
          AddMonoid.End A)
⊢ HAdd.hAdd (β := AddMonoid.End A)
      (HAdd.hAdd (β := AddMonoid.End A)
        (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b)) :
              AddMonoid.End A) +
          HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (b * a)) :
              AddMonoid.End A))
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * a)) :
          AddMonoid.End A))
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) (b * b)) :
        AddMonoid.End A) =
    Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a + b) : AddMonoid.End A)
      ((L : (a : A) → AddMonoid.End A) ((a + b) * (a + b)))

Tactic:
simp only [add_mul, mul_add, map_add, lie_add, add_lie, mul_comm b a,
    (commute_lmul_lmul_sq a).lie_eq, (commute_lmul_lmul_sq b).lie_eq, zero_add, add_zero, two_smul]

Premises used: add_mul, Commute.lie_eq, two_smul, map_add, commute_lmul_lmul_sq, zero_add, mul_comm, mul_add, add_zero, lie_add, add_lie