-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
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) ⋯))
              (((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) ⋯))) ∘ₗ
          ι 0 :
        (a : R) → CliffordAlgebra 0)
      1)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := R) 0)) ∘ₗ ι 0 : (a : R) → CliffordAlgebra 0) 1)
⊢ 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))

Tactic:
ext : 2