no goals
R : Type u_2
inst✝⁴ : CommSemiring R
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap (↑(lift R) f)) (ι R) = f
convert (lift R).symm_apply_apply f