-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b c : A
nth_rw :
  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) +
          HSMul.hSMul (α := ℕ) 2
            (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) (b * 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) +
          HSMul.hSMul (α := ℕ) 2
            (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 * 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) (c * 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) +
        HSMul.hSMul (α := ℕ) 2
          (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) (b * 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 * c)) :
              AddMonoid.End A))) =
    0
⊢ 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) +
          HSMul.hSMul (α := ℕ) 2
            (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) (β := 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) +
          HSMul.hSMul (α := ℕ) 2
            (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 * 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) (c * 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) +
        HSMul.hSMul (α := ℕ) 2
          (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) (b * 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 * c)) :
              AddMonoid.End A))) =
    0

Tactic:
nth_rw 2 [mul_comm a b]

Premises used: mul_comm