𝕜 : Type ?u.79010
M : Type ?u.79013
α : Type ?u.79016
G : Type u_1
E : Type u_2
F : Type ?u.79025
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✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
x' : G
⊢ (∫ (x : G), f (x' * x⁻¹) ∂μ) = ∫ (x : G), f x ∂μ
𝕜 : Type ?u.79010
M : Type ?u.79013
α : Type ?u.79016
G : Type u_1
E : Type u_2
F : Type ?u.79025
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✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
x' : G
⊢ (∫ (x : G), f (x' / x) ∂μ) = ∫ (x : G), f x ∂μ
simp_rw [div_eq_mul_inv]
no goals
𝕜 : Type ?u.79010
M : Type ?u.79013
α : Type ?u.79016
G : Type u_1
E : Type u_2
F : Type ?u.79025
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✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
x' : G
⊢ (∫ (x : G), f (x' * x⁻¹) ∂μ) = ∫ (x : G), f x ∂μ
rw [integral_inv_eq_self (fun x => f (x' * x)) μ, integral_mul_left_eq_self f x']