∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (φ : M →ₗ[R] M)
  (m : Module.AEval' φ), (Module.AEval'.of φ).symm (Polynomial.X • m) = φ ((Module.AEval'.of φ).symm m)