∀ {ι : Type u_1} {ιM : Type u_2} {R : Type u_3} {M : Type u_4} {σ : Type u_5} {σM : Type u_6} {inst : AddMonoid ι}
  {inst_1 : PartialOrder ι} {inst_2 : PartialOrder ιM} {inst_3 : VAdd ι ιM} {inst_4 : Preorder σ} {inst_5 : Semiring R}
  {inst_6 : SetLike σ R} {inst_7 : Preorder σM} {inst_8 : AddCommMonoid M} {inst_9 : Module R M}
  {inst_10 : SetLike σM M} {F : ι → σ} {F_lt : outParam (ι → σ)} {inst_11 : IsRingFiltration F F_lt} {F' : ιM → σM}
  {F'_lt : outParam (ιM → σM)} [self : IsModuleFiltration F F_lt F' F'_lt], SetLike.GradedSMul F F'