no goals
𝕜 : Type ?u.51091
M : Type ?u.51094
α : Type ?u.51097
G : Type u_1
E : Type u_2
F : Type ?u.51106
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
hf' : ∀ (x : G), f (x * g) = -f x
⊢ (∫ (x : G), f x ∂μ) = 0
simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self]