∀ {R : Type u_3} [inst : Semiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] (A' : Submodule R A) (M' : Submodule R M)
  (r : R) (m₁ m₂ : M),
  r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier →
    r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier →
      r • (m₁ + m₂) ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier