∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_3} [inst_1 : Semiring K]
  [inst_2 : AddCommMonoid β] [inst_3 : Module K β] (c : K) (f : MeasureTheory.SimpleFunc α β), ⇑(c • f) = c • ⇑f