-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b : A
this :
  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) =
    0
rwa :
  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 * 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) =
    0
⊢ 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 * 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)
have rwa₁ : HSub.hSub (β := AddMonoid.End A)
    (HSub.hSub (β := 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)))
      (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) =
  0
Tactic: rwa [← sub_eq_zero, ← sub_sub, sub_eq_add_neg, sub_eq_add_neg, lie_skew, lie_skew, nsmul_add]