case h.e'_3.h.e'_3
𝕜 : Type ?u.5463
M : Type ?u.5466
α : Type ?u.5469
G : Type u_1
E : Type ?u.5475
F : Type ?u.5478
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 → ℝ≥0∞
g : G
⊢ μ = map (↑(MeasurableEquiv.mulLeft g)) μ
𝕜 : Type ?u.5463
M : Type ?u.5466
α : Type ?u.5469
G : Type u_1
E : Type ?u.5475
F : Type ?u.5478
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 → ℝ≥0∞
g : G
⊢ (∫⁻ (x : G), f (g * x) ∂μ) = ∫⁻ (x : G), f x ∂μ
convert (lintegral_map_equiv f <| MeasurableEquiv.mulLeft g).symm
no goals
case h.e'_3.h.e'_3
𝕜 : Type ?u.5463
M : Type ?u.5466
α : Type ?u.5469
G : Type u_1
E : Type ?u.5475
F : Type ?u.5478
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 → ℝ≥0∞
g : G
⊢ μ = map (↑(MeasurableEquiv.mulLeft g)) μ
simp [map_mul_left_eq_self μ g]