∀ {R : Type u} {M : Type v} [inst : AddCommMonoid M] [inst_1 : CommSemiring R] [inst_2 : Module R M] {N : Submodule R M}
  (ϕ : M →ₗ[R] R) [inst_3 : (Submodule.map ϕ N).IsPrincipal] {x : M},
  x ∈ N → Submodule.IsPrincipal.generator (Submodule.map ϕ N) ∣ ϕ x