∀ {α : Type u_1} {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : CommGroup G]
  [MeasurableMul₂ G] [MeasurableInv G] {f g : α → G}, Measurable f → (Measurable (f * g) ↔ Measurable g)