-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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 : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
a b : CliffordAlgebra Q
rw :
  Eq.{u_3 + 1} (α := N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b) : CliffordAlgebra Q) :
      N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                a) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        b :
      N)
rw₁ :
  Eq.{u_3 + 1} (α := N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b) : CliffordAlgebra Q) :
      N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                a) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q) :
      N)
rw₂ :
  Eq.{u_3 + 1} (α := N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b) : CliffordAlgebra Q) :
      N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a : CliffordAlgebra Q)) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q) :
      N)
rw₃ :
  Eq.{u_3 + 1} (α := N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a : CliffordAlgebra Q)) :
      N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a : CliffordAlgebra Q)) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q) :
      N)
rw₄ rw₅ :
  Eq.{u_3 + 1} (α := N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a : CliffordAlgebra Q)) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q) :
      N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a : CliffordAlgebra Q)) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q) :
      N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        (a * b) :
      N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                a) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        b :
      N)

Tactic:
rw [← foldr_reverse, ← foldr_reverse, ← foldr_reverse, reverse.map_mul, foldr_mul]

Premises used: CliffordAlgebra.foldr_mul, CliffordAlgebra.reverse.map_mul, CliffordAlgebra.foldr_reverse