-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
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) ⋯))
            ((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) ⋯)) :
          (a : R[ε]) → R[ε])
        ε :
      R[ε])
    ((AlgHom.id R R[ε] : (a : R[ε]) → R[ε]) ε : 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[ε])

Tactic:
ext : 1