-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
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)
    (0 : 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)
    (0 : 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)
          ((((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)
    (0 : CliffordAlgebra Q)
rw₃ : Eq (α := CliffordAlgebra Q) ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) 0) 0
rw₄ rw₅ : Eq (α := CliffordAlgebra Q) 0 0
⊢ 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)
    (0 : CliffordAlgebra Q)

Tactic:
rw [contractRight_eq, contractRight_eq, reverse_reverse, contractLeft_contractLeft, map_zero]

Premises used: CliffordAlgebra.contractRight_eq, map_zero, CliffordAlgebra.contractLeft_contractLeft, CliffordAlgebra.reverse_reverse