case h.e'_2.h.e'_3
𝕜 : Type ?u.585203
G : Type u_1
H : Type ?u.585209
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : TopologicalGroup G
inst✝ : BorelSpace G
g : G
⊢ {g} = (fun h => g⁻¹ * h) ⁻¹' {1}
𝕜 : Type ?u.585203
G : Type u_1
H : Type ?u.585209
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : TopologicalGroup G
inst✝ : BorelSpace G
g : G
⊢ ↑↑μ {g} = ↑↑μ {1}
convert measure_preimage_mul μ g⁻¹ _
no goals
case h.e'_2.h.e'_3
𝕜 : Type ?u.585203
G : Type u_1
H : Type ?u.585209
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : TopologicalGroup G
inst✝ : BorelSpace G
g : G
⊢ {g} = (fun h => g⁻¹ * h) ⁻¹' {1}
simp only [mul_one, preimage_mul_left_singleton, inv_inv]