no goals
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Group G
inst✝⁴ : MeasurableMul₂ G
μ ν : Measure G
inst✝³ : SigmaFinite ν
inst✝² : SigmaFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : IsMulLeftInvariant μ
y : G
⊢ ↑↑μ ((fun x => x * y) ⁻¹' s) = 0 ↔ ↑↑μ ((fun x => y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0
simp_rw [← inv_preimage, preimage_preimage, mul_inv_rev, inv_inv]
no goals
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Group G
inst✝⁴ : MeasurableMul₂ G
μ ν : Measure G
inst✝³ : SigmaFinite ν
inst✝² : SigmaFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : IsMulLeftInvariant μ
y : G
⊢ ↑↑μ ((fun x => y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0 ↔ ↑↑μ s = 0
simp only [measure_inv_null μ, measure_preimage_mul]