-- 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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
d : Module.Dual R M
x : CliffordAlgebra Q
m : M
hx :
  Eq (α := CliffordAlgebra Q')
    ((changeForm h : (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')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
      CliffordAlgebra Q')
ι_mul :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q') ((d : (a : M) → R) m : R)
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q') -
      HSub.hSub (β := CliffordAlgebra Q')
        (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
          ((changeForm h : (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')
                  ((B : (a : M) → M →ₗ[R] R) m) :
                CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
              (a : CliffordAlgebra Q') → CliffordAlgebra Q')
            ((changeForm h : (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') =
    HSub.hSub (β := CliffordAlgebra Q')
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q') ((d : (a : M) → R) m : R)
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q') -
        HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
          ((changeForm h : (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')
                  ((B : (a : M) → M →ₗ[R] R) m) :
                CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
              (a : CliffordAlgebra Q') → CliffordAlgebra Q')
            ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x)) :
        CliffordAlgebra Q')
ι_mul₁ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q') ((d : (a : M) → R) m : R)
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q') -
      HSub.hSub (β := CliffordAlgebra Q')
        (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
          ((changeForm h : (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')
                  ((B : (a : M) → M →ₗ[R] R) m) :
                CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
              (a : CliffordAlgebra Q') → CliffordAlgebra Q')
            ((changeForm h : (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') =
    HSub.hSub (β := CliffordAlgebra Q')
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q') ((d : (a : M) → R) m : R)
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q') -
        HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
          ((changeForm h : (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')
                  ((B : (a : M) → M →ₗ[R] R) m) :
                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')
              ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x)) :
        CliffordAlgebra Q')
ι_mul₂ :
  HAdd.hAdd (β := CliffordAlgebra Q')
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q') ((d : (a : M) → R) m : R)
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q') -
        HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
          ((changeForm h : (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')
                ((B : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
            (a : CliffordAlgebra Q') → CliffordAlgebra Q')
          ((changeForm h : (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') =
    HSub.hSub (β := CliffordAlgebra Q')
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q') ((d : (a : M) → R) m : R)
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q') -
        HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
          ((changeForm h : (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')
                  ((B : (a : M) → M →ₗ[R] R) m) :
                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')
              ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x)) :
        CliffordAlgebra Q')
ι_mul₃ :
  HAdd.hAdd (β := CliffordAlgebra Q')
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q') ((d : (a : M) → R) m : R)
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q') -
        HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
          ((changeForm h : (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')
                ((B : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
            (a : CliffordAlgebra Q') → CliffordAlgebra Q')
          ((changeForm h : (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') =
    HAdd.hAdd (β := CliffordAlgebra Q')
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q') ((d : (a : M) → R) m : R)
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q') -
        HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
          ((changeForm h : (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')
                ((B : (a : M) → M →ₗ[R] R) m) :
              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')
            ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x)) :
        CliffordAlgebra Q')
ι_mul₄ ι_mul₅ :
  HAdd.hAdd (β := CliffordAlgebra Q')
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q') ((d : (a : M) → R) m : R)
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q') -
        HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
          ((changeForm h : (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')
                ((B : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
            (a : CliffordAlgebra Q') → CliffordAlgebra Q')
          ((changeForm h : (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') =
    HAdd.hAdd (β := CliffordAlgebra Q')
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q') ((d : (a : M) → R) m : R)
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q') -
        HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
          ((changeForm h : (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')
                ((B : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
            (a : CliffordAlgebra Q') → CliffordAlgebra Q')
          ((changeForm h : (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)
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q') -
      HSub.hSub (β := CliffordAlgebra Q')
        (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((ι Q' : (a : M) → CliffordAlgebra Q') m : CliffordAlgebra Q')
          ((changeForm h : (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')
                  ((B : (a : M) → M →ₗ[R] R) m) :
                CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
              (a : CliffordAlgebra Q') → CliffordAlgebra Q')
            ((changeForm h : (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') =
    HSub.hSub (β := CliffordAlgebra Q')
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q') ((d : (a : M) → R) m : R)
          ((changeForm h : (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')
              ((changeForm h : (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')
                  ((B : (a : M) → M →ₗ[R] R) m) :
                CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
              (a : CliffordAlgebra Q') → CliffordAlgebra Q')
            ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x)) :
        CliffordAlgebra Q')

Tactic:
rw [← hx, contractLeft_comm, ← sub_add, sub_neg_eq_add, ← hx]

Premises used: sub_add, CliffordAlgebra.contractLeft_comm, sub_neg_eq_add