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