-- 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 y : CliffordAlgebra Q
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)
hy :
  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)
          y) :
      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)
            y) :
      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)
          (x + y)) :
      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 + y)) :
      CliffordAlgebra Q)
have add : 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)
      (HAdd.hAdd (α := 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)
            y :
          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)
          (x + y)) :
    CliffordAlgebra Q)
Tactic: rw [map_add, map_add, map_add, map_add, hx, hy, neg_add]