-- 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 : CliffordAlgebra Q
m : M
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)
⊢ (((contractLeftAux Q (d₁ + d₂) : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) m :
          CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
        (a : CliffordAlgebra Q × 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)) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractLeftAux Q d₁ : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) m :
              CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q × CliffordAlgebra Q) → CliffordAlgebra Q)
          (x, (foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)
      ((((contractLeftAux Q d₂ : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) m :
              CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q × CliffordAlgebra Q) → CliffordAlgebra Q)
          (x, (foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q)
have ι_mul : HSMul.hSMul (α := R) ((d₁ + d₂ : (a : M) → R) m : R) x -
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : 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) x : CliffordAlgebra Q)) =
  HSMul.hSMul (α := R) ((d₁ : (a : M) → R) m : R) x -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d₁) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) +
    (HSMul.hSMul (α := R) ((d₂ : (a : M) → R) m : R) x -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d₂) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
Tactic: dsimp only [contractLeftAux_apply_apply]