-- 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 : 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
hd : M
tl : List M
ih :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) tl)) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n tl
cons :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod ((ι Q : (a : M) → CliffordAlgebra Q) hd :: List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) tl) :
        CliffordAlgebra Q) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n (hd :: tl)
cons₁ :
  (((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)
        ((ι Q : (a : M) → CliffordAlgebra Q) hd : CliffordAlgebra Q)
        (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) tl) : CliffordAlgebra Q)) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n (hd :: tl)
cons₂ :
  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)
          ((ι Q : (a : M) → CliffordAlgebra Q) hd : CliffordAlgebra Q)
          (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) tl) : CliffordAlgebra Q)) :
      N)
    ((((f : (a : M) → N →ₗ[R] N) hd : N →ₗ[R] N) : (a : N) → N)
        (List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n tl) :
      N)
cons₃ :
  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)
              (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) tl))) :
          (a : CliffordAlgebra Q) → N)
        ((ι Q : (a : M) → CliffordAlgebra Q) hd : CliffordAlgebra Q) :
      N)
    ((((f : (a : M) → N →ₗ[R] N) hd : N →ₗ[R] N) : (a : N) → N)
        (List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n tl) :
      N)
⊢ (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) (hd :: tl))) =
    List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n (hd :: tl)
have cons₄ : Eq.{u_3 + 1} (α := N)
  ((((f : (a : M) → N →ₗ[R] N) hd : N →ₗ[R] N) : (a : N) → N)
      ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
            (a : CliffordAlgebra Q) → N)
          (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) tl)) :
        N) :
    N)
  ((((f : (a : M) → N →ₗ[R] N) hd : N →ₗ[R] N) : (a : N) → N)
      (List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n tl) :
    N)
Tactic: rw [List.map_cons, List.prod_cons, List.foldr_cons, foldr_mul, foldr_ι, ih]