-- 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
rw :
  ⁅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) +
            HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A) +
          HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (c * a) : AddMonoid.End A) +
        HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)⁆ =
    HSMul.hSMul (α := ℕ) 2
      (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) (b * c)) :
            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 * 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 * b)) :
          AddMonoid.End A))
rw₁ :
  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 * 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 : 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)
                (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
                  ((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)
              (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
                ((L : (a : A) → AddMonoid.End A) (c * a) : AddMonoid.End A)) +
          Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
            (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
              ((L : (a : A) → AddMonoid.End A) (b * c) : 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) 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) b : 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) +
              Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
                (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
                  ((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)
              (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
                ((L : (a : A) → AddMonoid.End A) (c * a) : AddMonoid.End A)) +
          Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
            (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
              ((L : (a : A) → AddMonoid.End A) (b * c) : 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) 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) 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) 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)
              (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
                ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A)) +
          Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
            (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
              ((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)
          (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A))) =
    HSMul.hSMul (α := ℕ) 2
      (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) (b * c)) :
            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 * 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 * b)) :
          AddMonoid.End A))
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) (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))) +
      (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) (b * c)) :
              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) (c * a)) :
              AddMonoid.End A) +
        HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * b)) :
            AddMonoid.End A)) =
    HSMul.hSMul (α := ℕ) 2
      (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) (b * c)) :
            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 * 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 * b)) :
          AddMonoid.End A))
⊢ Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a + b + c) : AddMonoid.End A)
      ((L : (a : A) → AddMonoid.End A) ((a + b + c) * (a + b + c))) =
    HSMul.hSMul (α := ℕ) 2
      (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) (b * c)) :
            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 * 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 * b)) :
          AddMonoid.End A))
have rw₃ : 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) (b * c)) :
          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) (c * a)) :
          AddMonoid.End A) +
    HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) (a * b)) :
        AddMonoid.End A) =
  HSMul.hSMul (α := ℕ) 2
    (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) (b * c)) :
          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 * 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 * b)) :
        AddMonoid.End A))
Tactic: rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]