∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {M : Type u_4} [inst_5 : Monoid M] [inst_6 : DistribMulAction M F]
  [inst_7 : SMulCommClass R M F] (a b : M) (f : E →ₗ.[R] F),
  { domain := f.domain, toFun := (a * b) • f.toFun } = { domain := f.domain, toFun := a • (b • f).toFun }