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