-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
rw :
  Eq.{u_3 + 1} (α := A)
    (Function.comp (β := FreeAlgebra R M)
      (⇑(AlgHom.comp (B := RingQuot (R := FreeAlgebra R M) (Rel R M))
            (Function.comp (β :=
              { f : FreeAlgebra R M →ₐ[R] A //
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y →
                    Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                      ((f : (a : FreeAlgebra R M) → A) y : A) })
              (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
                (a :
                    { f : FreeAlgebra R M →ₐ[R] A //
                      ∀ ⦃x y : FreeAlgebra R M⦄,
                        Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
                  RingQuot (Rel R M) →ₐ[R] A)
              (fun (f : M →ₗ[R] A) ↦
                Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
                  ∀ ⦃x y : FreeAlgebra R M⦄,
                    Rel R M x y →
                      Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                        ((f : (a : FreeAlgebra R M) → A) y : A))
                  ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) ⋯)
              ((fun (F : TensorAlgebra R M →ₐ[R] A) ↦
                  (F.toLinearMap ∘ₗ
                      {
                        toFun := fun (m : M) ↦
                          (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M))
                            (FreeAlgebra.ι R m),
                        map_add' := ⋯, map_smul' := ⋯ } :
                    M →ₗ[R] A))
                F))
            (RingQuot.mkAlgHom R (Rel R M))) :
        (a : FreeAlgebra R M) → A)
      (FreeAlgebra.ι R) x)
    (Function.comp (β := FreeAlgebra R M) (⇑(F.comp (RingQuot.mkAlgHom R (Rel R M))) : (a : FreeAlgebra R M) → A)
      (FreeAlgebra.ι R) x)
⊢ Eq.{u_3 + 1} (α := A)
    (Function.comp (β := FreeAlgebra R M)
      (⇑(AlgHom.comp (B := RingQuot (R := FreeAlgebra R M) (Rel R M))
            (Function.comp (β :=
              { f : FreeAlgebra R M →ₐ[R] A //
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y →
                    Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                      ((f : (a : FreeAlgebra R M) → A) y : A) })
              (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
                (a :
                    { f : FreeAlgebra R M →ₐ[R] A //
                      ∀ ⦃x y : FreeAlgebra R M⦄,
                        Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
                  RingQuot (Rel R M) →ₐ[R] A)
              (fun (f : M →ₗ[R] A) ↦
                Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
                  ∀ ⦃x y : FreeAlgebra R M⦄,
                    Rel R M x y →
                      Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                        ((f : (a : FreeAlgebra R M) → A) y : A))
                  ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) ⋯)
              ((fun (F : TensorAlgebra R M →ₐ[R] A) ↦ F.toLinearMap ∘ₗ ι R) F))
            (RingQuot.mkAlgHom R (Rel R M))) :
        (a : FreeAlgebra R M) → A)
      (FreeAlgebra.ι R) x)
    (Function.comp (β := FreeAlgebra R M) (⇑(F.comp (RingQuot.mkAlgHom R (Rel R M))) : (a : FreeAlgebra R M) → A)
      (FreeAlgebra.ι R) x)

Tactic:
rw [ι]

Premises used: TensorAlgebra.ι