∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : CommRing A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} {N : Submodule (MonoidAlgebra A G) ρ.asModule} {w : W},
  (w ∈ Subrepresentation.ofSubmodule' N) = (w ∈ N)