-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := CliffordAlgebra (R := R) (M := R) 0 →ₐ[R] CliffordAlgebra (R := R) (M := R) 0)
    (AlgHom.comp (B := 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) ⋯))
      (((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) ⋯)))
    (AlgHom.id R (CliffordAlgebra (R := R) (M := R) 0))
have a : Eq (α := CliffordAlgebra (R := R) (M := R) 0)
  ((AlgHom.toLinearMap
          (AlgHom.comp (B := 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) sorry))
            (((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))) ∘ₗ
        ι 0 :
      (a : R) → CliffordAlgebra 0)
    1)
  ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := R) 0)) ∘ₗ ι 0 : (a : R) → CliffordAlgebra 0) 1)
Tactic: ext : 2