-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
rw :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) x :
                  Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
                (a : Module.Dual R M) → CliffordAlgebra Q)
              d))) :
      CliffordAlgebra Q)
    (-(((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
                ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) x :
                      Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
                    (a : Module.Dual R M) → CliffordAlgebra Q)
                  d') :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
      CliffordAlgebra Q)
rw₁ :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                    CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
                  (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))))) :
      CliffordAlgebra Q)
    (-(((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
                ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) x :
                      Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
                    (a : Module.Dual R M) → CliffordAlgebra Q)
                  d') :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
      CliffordAlgebra Q)
rw₂ :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                    CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
                  (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))))) :
      CliffordAlgebra Q)
    (-(reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) x :
                    Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
                  (a : Module.Dual R M) → CliffordAlgebra Q)
                d'))) :
      CliffordAlgebra Q)
rw₃ :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                    CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
                  (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))))) :
      CliffordAlgebra Q)
    (-(reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
                      CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
                    (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                  ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))))) :
      CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
              ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) x :
                    Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
                  (a : Module.Dual R M) → CliffordAlgebra Q)
                d) :
            Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
          (a : Module.Dual R M) → CliffordAlgebra Q)
        d' :
      CliffordAlgebra Q)
    (-(((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
                ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) x :
                      Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
                    (a : Module.Dual R M) → CliffordAlgebra Q)
                  d') :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
      CliffordAlgebra Q)
have rw₄ : Eq (α := CliffordAlgebra Q)
  ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))) :
    CliffordAlgebra Q)
  (-(reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
                    CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
                  (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))))) :
    CliffordAlgebra Q)
Tactic: rw [contractRight_eq, contractRight_eq, contractRight_eq, contractRight_eq, reverse_reverse,
    reverse_reverse, contractLeft_comm, map_neg]