∀ {ιA : Type u_5} {ιM : Type u_6} {A : Type u_1} {M : Type u_3} {σ : Type u_4} {σ' : Type u_2} [inst : AddMonoid ιA]
  [inst_1 : AddAction ιA ιM] [inst_2 : Semiring A] (𝓐 : ιA → σ') [inst_3 : SetLike σ' A] (𝓜 : ιM → σ)
  [inst_4 : AddCommMonoid M] [inst_5 : Module A M] [inst_6 : SetLike σ M] [inst_7 : AddSubmonoidClass σ M]
  [inst_8 : SetLike.GradedMonoid 𝓐] [inst_9 : SetLike.GradedSMul 𝓐 𝓜] {i : ιA} {j : ιM} (a : ↥(𝓐 i)) (b c : ↥(𝓜 j)),
  GradedMonoid.GSMul.smul a (b + c) = GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a c