-- 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_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
x y : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
hy :
  (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
add₁ :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    c •
      HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
add₂ :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
        ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) +
      HSMul.hSMul (β := CliffordAlgebra Q) c
        ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) : CliffordAlgebra Q)
have add₃ : HAdd.hAdd (β := CliffordAlgebra Q)
    (HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
    ((foldr' Q (contractLeftAux Q (c • d)) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) +
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q)
Tactic: rw [map_add, map_add, smul_add, hx, hy]