∀ {G : Type u_2} {α : Type u_3} [inst : Inv G] [inst_1 : MeasurableSpace G] [MeasurableInv G] {m : MeasurableSpace α}
  {f : α → G} {μ : MeasureTheory.Measure α}, AEMeasurable f μ → AEMeasurable (fun x => (f x)⁻¹) μ