-- 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
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)
⊢ (((((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
have e_fst₁ : ∀ (x y : CliffordAlgebra Q)
  (hx :
    (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) sorry :
                    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) sorry :
                    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) sorry :
                  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
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]
Cleared hypotheses: x