∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : SMul γ β]
  [inst_2 : SMul K β] [SMulCommClass K γ β], SMulCommClass K γ (MeasureTheory.SimpleFunc α β)