-- 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 : 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
n : N
m : M
x : CliffordAlgebra Q
e_fst :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q)
      ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                      CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                    (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                  (1, n) :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)).1 :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
e_fst₁ :
  ∀ (x y : CliffordAlgebra Q)
    (hx :
      (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                      CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                    (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                  (1, n) :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
            x).1 =
        x)
    (hy :
      (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                      CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                    (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                  (1, n) :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
            y).1 =
        y),
    (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          (x + y)).1 =
      x + y
e_fst₂ :
  ∀ (m : CliffordAlgebra Q) (x : M)
    (hx :
      (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                      CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                    (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                  (1, n) :
                CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
              (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
            m).1 =
        m),
    (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q) m)).1 =
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q) m
⊢ (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                  CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
              (1, n) :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
        x).1 =
    x

Tactic:
induction x using CliffordAlgebra.left_induction with
  | algebraMap r => simp_rw [foldr_algebraMap, Prod.smul_mk, Algebra.algebraMap_eq_smul_one]
  | add x y hx hy => rw [map_add, Prod.fst_add, hx, hy]
  | ι_mul m x hx => rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply, hx]

Premises used: CliffordAlgebra.foldr_mul, Algebra.algebraMap, map_add, CliffordAlgebra.foldr_ι, Algebra.algebraMap_eq_smul_one, CliffordAlgebra.foldr'Aux_apply_apply, Prod.fst_add, CliffordAlgebra.foldr_algebraMap, Prod.smul_mk