-- 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)
ι_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₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
    HSMul.hSMul (α := R) ((d₁ : (a : M) → R) m : R) x + 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₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) +
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
ι_mul₁ :
  HSMul.hSMul (α := R) ((d₁ + 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₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) +
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
    HSMul.hSMul (α := R) ((d₁ : (a : M) → R) m : R) x + 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₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) +
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
⊢ 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₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d₂) ⋯ 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₁) ⋯ 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₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
have ι_mul₂ : HAdd.hAdd (α := R) (β := R) ((d₁ : (a : M) → R) m : 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) +
      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 + 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) +
      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: rw [sub_add_sub_comm, mul_add, LinearMap.add_apply, add_smul]