-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f :
  { f : M →ₗ[R] A //
    ∀ (m : M),
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }
a :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := A)
      (((↑((fun (F : CliffordAlgebra Q →ₐ[R] A) ↦
                    (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
                        ∀ (m : M),
                          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
                        (F.toLinearMap ∘ₗ ι Q) ⋯ :
                      { f : M →ₗ[R] A //
                        ∀ (m : M),
                          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }))
                  ((fun
                        (f :
                          { f : M →ₗ[R] A //
                            ∀ (m : M),
                              HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                                (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }) ↦
                      ((RingQuot.liftAlgHom R (s := Rel Q) :
                            (a :
                                { f : TensorAlgebra R M →ₐ[R] A //
                                  ∀ ⦃x y : TensorAlgebra R M⦄,
                                    Rel Q x y →
                                      (f : (a : TensorAlgebra R M) → A) x = (f : (a : TensorAlgebra R M) → A) y }) →
                              RingQuot (Rel Q) →ₐ[R] A)
                          (Subtype.mk (p := fun (f : TensorAlgebra R M →ₐ[R] A) ↦
                            ∀ ⦃x y : TensorAlgebra R M⦄,
                              Rel Q x y →
                                Eq.{u_3 + 1} (α := A) ((f : (a : TensorAlgebra R M) → A) x : A)
                                  ((f : (a : TensorAlgebra R M) → A) y : A))
                            ((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A)) ⋯) :
                        RingQuot (Rel Q) →ₐ[R] A))
                    f)) :
              M →ₗ[R] A) :
            (a : M) → A)
          x :
        A)
      (((↑f : M →ₗ[R] A) : (a : M) → A) x : A)
⊢ (fun (F : CliffordAlgebra Q →ₐ[R] A) ↦
        (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
            ∀ (m : M),
              HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
            (F.toLinearMap ∘ₗ ι Q) ⋯ :
          { f : M →ₗ[R] A //
            ∀ (m : M),
              HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }))
      ((fun
            (f :
              { f : M →ₗ[R] A //
                ∀ (m : M),
                  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }) ↦
          ((RingQuot.liftAlgHom R (s := Rel Q) :
                (a :
                    { f : TensorAlgebra R M →ₐ[R] A //
                      ∀ ⦃x y : TensorAlgebra R M⦄,
                        Rel Q x y → (f : (a : TensorAlgebra R M) → A) x = (f : (a : TensorAlgebra R M) → A) y }) →
                  RingQuot (Rel Q) →ₐ[R] A)
              (Subtype.mk (p := fun (f : TensorAlgebra R M →ₐ[R] A) ↦
                ∀ ⦃x y : TensorAlgebra R M⦄,
                  Rel Q x y →
                    Eq.{u_3 + 1} (α := A) ((f : (a : TensorAlgebra R M) → A) x : A)
                      ((f : (a : TensorAlgebra R M) → A) y : A))
                ((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A)) ⋯) :
            RingQuot (Rel Q) →ₐ[R] A))
        f) =
    f

Tactic:
ext x