∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] (p : SubMulAction R M) {G : Type u_1}
  [inst_2 : Group G] [inst_3 : SMul G R] [inst_4 : MulAction G M] [IsScalarTower G R M] (g : G) {x : M},
  g • x ∈ p ↔ x ∈ p