∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type w}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') (S : Submodule R M') (I : Ideal R),
  I • Submodule.comap f S ≤ Submodule.comap f (I • S)