-- 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 : Module.Dual R M
a : M
b : CliffordAlgebra Q
rw :
  (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          (HMul.hMul (β := CliffordAlgebra Q) b ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)))) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
rw₁ :
  (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a) :
            CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q))) =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
⊢ (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
            (HMul.hMul (β := CliffordAlgebra Q) b ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)) :
          Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
        (a : Module.Dual R M) → CliffordAlgebra Q)
      d =
    HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
                Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
              (a : Module.Dual R M) → CliffordAlgebra Q)
            d :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
have rw₂ : (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
          CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
        (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q))) =
  HSMul.hSMul (α := R) ((d : (a : M) → R) a : R) b -
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) b :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
Tactic: rw [contractRight_eq, reverse.map_mul, reverse_ι, contractLeft_ι_mul, map_sub, map_smul,
    reverse_reverse, reverse.map_mul, reverse_ι, contractRight_eq]