-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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) }
⊢ (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
have 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) sorry :
                    { 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)) sorry) :
                      RingQuot (Rel Q) →ₐ[R] A))
                  f)) :
            M →ₗ[R] A) :
          (a : M) → A)
        x :
      A)
    (((↑f : M →ₗ[R] A) : (a : M) → A) x : A)
Tactic: ext x