-- 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 d' : Module.Dual R M
x : CliffordAlgebra Q
m : M
hx :
  Eq (α := 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)
          x) :
      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)
            x) :
      CliffordAlgebra Q)
ι_mul :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d' : (a : M) → R) m : R)
        ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            x :
          CliffordAlgebra Q) -
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d : (a : M) → R) m : R)
          ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
                  CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
                (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              x :
            CliffordAlgebra Q) -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : 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)
                x) :
            CliffordAlgebra Q)) =
    -(HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d : (a : M) → R) m : R)
          ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d' :
                  CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
                (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              x :
            CliffordAlgebra Q) -
        (HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d' : (a : M) → R) m : R)
            ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
                    CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
                  (a : CliffordAlgebra Q) → CliffordAlgebra Q)
                x :
              CliffordAlgebra Q) -
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m : 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)
                  x) :
              CliffordAlgebra Q)))
⊢ Eq (α := 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)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)) :
      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)
            (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)) :
      CliffordAlgebra Q)

Tactic:
simp only [contractLeft_ι_mul, map_sub, map_smul]

Premises used: map_sub, CliffordAlgebra.contractLeft_ι_mul, map_smul