-- 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
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) -
        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)
ι_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) +
        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) -
      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)
ι_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) +
        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) -
      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) -
      (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)))
have ι_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) +
      -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) -
    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)
Tactic: rw [neg_sub, sub_sub_eq_add_sub, hx, mul_neg, ← sub_eq_add_neg]