𝕜 : Type ?u.2501
M : Type ?u.2504
α : Type ?u.2507
G : Type u_1
E : Type u_2
F : Type ?u.2516
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✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : IsInvInvariant μ
h : MeasurableEmbedding fun x => x⁻¹
⊢ (∫ (x : G), f x⁻¹ ∂μ) = ∫ (x : G), f x ∂μ
𝕜 : Type ?u.2501
M : Type ?u.2504
α : Type ?u.2507
G : Type u_1
E : Type u_2
F : Type ?u.2516
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✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : IsInvInvariant μ
⊢ (∫ (x : G), f x⁻¹ ∂μ) = ∫ (x : G), f x ∂μ
have h : MeasurableEmbedding fun x : G => x⁻¹ := (MeasurableEquiv.inv G).measurableEmbedding
no goals
𝕜 : Type ?u.2501
M : Type ?u.2504
α : Type ?u.2507
G : Type u_1
E : Type u_2
F : Type ?u.2516
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✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : IsInvInvariant μ
h : MeasurableEmbedding fun x => x⁻¹
⊢ (∫ (x : G), f x⁻¹ ∂μ) = ∫ (x : G), f x ∂μ
rw [← h.integral_map, map_inv_eq_self]