-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b c : 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) (b * 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) +
          HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) b) :
              AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End 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) (c * c)) :
              AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : 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 * a) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) c) :
              AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End 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) b : 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)
              ((L : (a : A) → AddMonoid.End A) (b * 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 * b) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) c) :
            AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) b) :
            AddMonoid.End A)) =
    0
have iterate : 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) (b * 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) +
        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 * 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) (β := 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) (c * c)) :
            AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : 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) c : 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) (c * c)) :
            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) (c * c)) :
          AddMonoid.End A)
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (b * b)) :
          AddMonoid.End A) +
      HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
        (-Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : 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) b : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (c * c)) :
          AddMonoid.End A)) =
  0
Tactic: iterate 2 rw [← lie_skew (L (a * a)), ← lie_skew (L (b * b)), ← lie_skew (L (c * c))]