∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} {f : G → E} {g : G} [inst_3 : AddGroup G] [MeasurableAdd G] [μ.IsAddLeftInvariant],
  (∀ (x : G), f (g + x) = -f x) → ∫ (x : G), f x ∂μ = 0