-- 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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
d : Module.Dual R M
x y : CliffordAlgebra Q
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')
hy :
  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)
          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')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y) :
      CliffordAlgebra Q')
add :
  Eq (α := CliffordAlgebra Q')
    ((changeForm h : (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')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') (x + y)) :
      CliffordAlgebra Q')
add₁ :
  HAdd.hAdd (α := 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')
      ((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)
            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')
      ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') (x + y))
⊢ 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 + 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')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') (x + y)) :
      CliffordAlgebra Q')
have add₂ : HAdd.hAdd (α := 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')
    ((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)
          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')
    (HAdd.hAdd (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
      ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q')
      ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y : CliffordAlgebra Q'))
Tactic: rw [map_add, map_add, map_add, map_add, hx, hy]