-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[ε] →ₐ[R] R[ε])
    (AlgHom.comp (B := CliffordAlgebra (R := R) (M := R) 0)
      (((CliffordAlgebra.lift.{u_1, u_1, u_1} (R := R) (M := R) 0 (A := R[ε]) :
            { f : R →ₗ[R] R[ε] //
                ∀ (m : R),
                  HMul.hMul (α := R[ε]) (β := R[ε]) ((f : (a : R) → R[ε]) m : R[ε]) ((f : (a : R) → R[ε]) m : R[ε]) =
                    (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m : R) } ≃
              (CliffordAlgebra (R := R) (M := R) 0 →ₐ[R] R[ε])) :
          (a :
              { f : R →ₗ[R] R[ε] //
                ∀ (m : R),
                  (f : (a : R) → R[ε]) m * (f : (a : R) → R[ε]) m =
                    (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m) }) →
            CliffordAlgebra 0 →ₐ[R] R[ε])
        (Subtype.mk (p := fun (f : R →ₗ[R] R[ε]) ↦
          ∀ (m : R),
            HMul.hMul (α := R[ε]) (β := R[ε]) ((f : (a : R) → R[ε]) m : R[ε]) ((f : (a : R) → R[ε]) m : R[ε]) =
              (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m : R))
          (inrHom R R) ⋯))
      ((DualNumber.lift :
          (a :
              { fe : (R →ₐ[R] CliffordAlgebra 0) × CliffordAlgebra 0 //
                fe.2 * fe.2 = 0 ∧ ∀ (a : R), Commute fe.2 ((fe.1 : (a : R) → CliffordAlgebra 0) a) }) →
            R[ε] →ₐ[R] CliffordAlgebra 0)
        (Subtype.mk (p :=
          fun (fe : (R →ₐ[R] CliffordAlgebra (R := R) (M := R) 0) × CliffordAlgebra (R := R) (M := R) 0) ↦
          fe.2 * fe.2 = 0 ∧ ∀ (a : R), Commute fe.2 ((fe.1 : (a : R) → CliffordAlgebra 0) a))
          (Algebra.ofId R (CliffordAlgebra (R := R) (M := R) 0), (ι 0 : (a : R) → CliffordAlgebra 0) 1) ⋯)))
    (AlgHom.id R R[ε])
have hε : Eq (α := R[ε])
  ((AlgHom.comp (B := CliffordAlgebra (R := R) (M := R) 0)
          (((CliffordAlgebra.lift.{u_1, u_1, u_1} (R := R) (M := R) 0 (A := R[ε]) :
                { f : R →ₗ[R] R[ε] //
                    ∀ (m : R),
                      HMul.hMul (α := R[ε]) (β := R[ε]) ((f : (a : R) → R[ε]) m : R[ε])
                          ((f : (a : R) → R[ε]) m : R[ε]) =
                        (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m : R) } ≃
                  (CliffordAlgebra (R := R) (M := R) 0 →ₐ[R] R[ε])) :
              (a :
                  { f : R →ₗ[R] R[ε] //
                    ∀ (m : R),
                      (f : (a : R) → R[ε]) m * (f : (a : R) → R[ε]) m =
                        (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m) }) →
                CliffordAlgebra 0 →ₐ[R] R[ε])
            (Subtype.mk (p := fun (f : R →ₗ[R] R[ε]) ↦
              ∀ (m : R),
                HMul.hMul (α := R[ε]) (β := R[ε]) ((f : (a : R) → R[ε]) m : R[ε]) ((f : (a : R) → R[ε]) m : R[ε]) =
                  (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m : R))
              (inrHom R R) sorry))
          ((DualNumber.lift :
              (a :
                  { fe : (R →ₐ[R] CliffordAlgebra 0) × CliffordAlgebra 0 //
                    fe.2 * fe.2 = 0 ∧ ∀ (a : R), Commute fe.2 ((fe.1 : (a : R) → CliffordAlgebra 0) a) }) →
                R[ε] →ₐ[R] CliffordAlgebra 0)
            (Subtype.mk (p :=
              fun (fe : (R →ₐ[R] CliffordAlgebra (R := R) (M := R) 0) × CliffordAlgebra (R := R) (M := R) 0) ↦
              fe.2 * fe.2 = 0 ∧ ∀ (a : R), Commute fe.2 ((fe.1 : (a : R) → CliffordAlgebra 0) a))
              (Algebra.ofId R (CliffordAlgebra (R := R) (M := R) 0), (ι 0 : (a : R) → CliffordAlgebra 0) 1) sorry)) :
        (a : R[ε]) → R[ε])
      ε :
    R[ε])
  ((AlgHom.id R R[ε] : (a : R[ε]) → R[ε]) ε : R[ε])
Tactic: ext : 1