𝕜 : Type ?u.34294
M : Type ?u.34297
α : Type ?u.34300
G : Type u_1
E : Type u_2
F : Type ?u.34309
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✝ : IsMulLeftInvariant μ
f : G → E
g : G
h_mul : MeasurableEmbedding fun x => g * x
⊢ (∫ (x : G), f (g * x) ∂μ) = ∫ (x : G), f x ∂μ
𝕜 : Type ?u.34294
M : Type ?u.34297
α : Type ?u.34300
G : Type u_1
E : Type u_2
F : Type ?u.34309
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✝ : IsMulLeftInvariant μ
f : G → E
g : G
⊢ (∫ (x : G), f (g * x) ∂μ) = ∫ (x : G), f x ∂μ
have h_mul : MeasurableEmbedding fun x => g * x := (MeasurableEquiv.mulLeft g).measurableEmbedding
no goals
𝕜 : Type ?u.34294
M : Type ?u.34297
α : Type ?u.34300
G : Type u_1
E : Type u_2
F : Type ?u.34309
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✝ : IsMulLeftInvariant μ
f : G → E
g : G
h_mul : MeasurableEmbedding fun x => g * x
⊢ (∫ (x : G), f (g * x) ∂μ) = ∫ (x : G), f x ∂μ
rw [← h_mul.integral_map, map_mul_left_eq_self]