∀ {R : Type u_2} {M : Type u_1} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : Mul M] [IsScalarTower R M M]
  (p q : SubMulAction R M) (r : R),
  ∀ x ∈ Set.image2 (fun x1 x2 => x1 * x2) ↑p ↑q, r • x ∈ Set.image2 (fun x1 x2 => x1 * x2) ↑p ↑q