∀ {ι : Type u_1} {S : Type u_3} {R : Type u_2} [inst : AddMonoid ι] [inst_1 : CommSemiring S] [inst_2 : Semiring R]
  [inst_3 : Algebra S R] (A : ι → Submodule S R) [inst_4 : SetLike.GradedMonoid A] (_r : S)
  (x : GradedMonoid fun i => ↥(A i)),
  GradedMonoid.mk 0 ((LinearMap.codRestrict (A 0) (Algebra.linearMap S R) ⋯).toAddMonoidHom _r) * x =
    x * GradedMonoid.mk 0 ((LinearMap.codRestrict (A 0) (Algebra.linearMap S R) ⋯).toAddMonoidHom _r)