-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
v : M
x_fx : CliffordAlgebra Q × N
rw :
  (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) *
        x_fx.1,
      (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              x_fx) :
          CliffordAlgebra Q × N)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
rw₁ :
  (HMul.hMul (α := CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) v) : CliffordAlgebra Q)
        x_fx.1,
      (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              x_fx) :
          CliffordAlgebra Q × N)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
⊢ (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1),
      (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              x_fx) :
          CliffordAlgebra Q × N)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
have rw₂ : (HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx.1,
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
        (a : CliffordAlgebra Q × N) → N)
      ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1,
          (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
              (a : CliffordAlgebra Q × N) → N)
            x_fx) :
        CliffordAlgebra Q × N)) =
  HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
Tactic: rw [← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, hf, Prod.smul_mk]