-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
a b c : A
simp :
  Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
          (HAdd.hAdd (β := AddMonoid.End A)
                (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A))
                ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A) +
              HAdd.hAdd (β := AddMonoid.End A)
                (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
                ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A) +
            HAdd.hAdd (β := AddMonoid.End A)
              (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A))
              ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A)) +
        Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
          (HAdd.hAdd (β := AddMonoid.End A)
                (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A))
                ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A) +
              HAdd.hAdd (β := AddMonoid.End A)
                (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
                ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A) +
            HAdd.hAdd (β := AddMonoid.End A)
              (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A))
              ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A)) +
      Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
        (HAdd.hAdd (β := AddMonoid.End A)
              (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A))
              ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A) +
            HAdd.hAdd (β := AddMonoid.End A)
              (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
              ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A) +
          HAdd.hAdd (β := AddMonoid.End A)
            (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A))
            ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A)) =
    Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
          (HAdd.hAdd (β := AddMonoid.End A)
                  (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                    ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
                    ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
                  ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A) +
                HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A) +
              HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A) +
            HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)) +
        Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
          (HAdd.hAdd (β := AddMonoid.End A)
                  (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                    ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
                    ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
                  ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A) +
                HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A) +
              HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A) +
            HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)) +
      Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
        (HAdd.hAdd (β := AddMonoid.End A)
                (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
                ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A) +
              HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A) +
            HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A) +
          HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A))
⊢ ⁅HAdd.hAdd (β := AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A))
        ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A),
      HAdd.hAdd (β := AddMonoid.End A)
            (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A))
            ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A) +
          HAdd.hAdd (β := AddMonoid.End A)
            (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
            ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A) +
        HAdd.hAdd (β := AddMonoid.End A)
          (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A))
          ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A)⁆ =
    ⁅HAdd.hAdd (β := AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A))
        ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A),
      HAdd.hAdd (β := AddMonoid.End A)
              (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
              ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A) +
            HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A) +
          HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * c) : AddMonoid.End A) +
        HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)⁆

Tactic:
simp only [add_lie]

Premises used: add_lie