-- 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
a : M
b : CliffordAlgebra Q
rw :
  (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)
          (HMul.hMul (β := CliffordAlgebra Q) b ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)))) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₁ :
  (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)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a) :
            CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q))) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₂ :
  (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)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q))) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₃ :
  (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d : (a : M) → R) a : R)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q) -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : 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) b) :
            CliffordAlgebra Q)) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₄ :
  HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d : (a : M) → R) a : R)
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q)) :
        CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) a : 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) b) :
              CliffordAlgebra Q)) :
        CliffordAlgebra Q) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₅ :
  HSub.hSub (β := CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((d : (a : M) → R) a : R)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b) :
          CliffordAlgebra Q))
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) a : 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) b) :
              CliffordAlgebra Q)) :
        CliffordAlgebra Q) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₆ :
  HSub.hSub (β := CliffordAlgebra Q) (HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) a : 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) b) :
              CliffordAlgebra Q)) :
        CliffordAlgebra Q) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₇ :
  HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := 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) b)) :
          CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a) :
          CliffordAlgebra Q) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₈ :
  HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := 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) b)) :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₉ rw₁₀ :
  HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := 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) b)) :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := 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) b)) :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
⊢ (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
            (HMul.hMul (β := CliffordAlgebra Q) b ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)) :
          Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
        (a : Module.Dual R M) → CliffordAlgebra Q)
      d =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)

Tactic:
rw [contractRight_eq, reverse.map_mul, reverse_ι, contractLeft_ι_mul, map_sub, map_smul,
    reverse_reverse, reverse.map_mul, reverse_ι, contractRight_eq]

Premises used: CliffordAlgebra.contractRight_eq, map_sub, CliffordAlgebra.contractLeft_ι_mul, CliffordAlgebra.reverse.map_mul, CliffordAlgebra.reverse_reverse, CliffordAlgebra.reverse_ι, map_smul