∀ (R : Type u_3) [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_2}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A),
  (fun F => F.toLinearMap ∘ₗ TensorAlgebra.ι R) ((⇑(RingQuot.liftAlgHom R) ∘ fun f => ⟨(FreeAlgebra.lift R) ⇑f, ⋯⟩) f) =
    f