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✝ : IsMulRightInvariant μ
⊢ MeasurePreserving ?m.553003
apply measurePreserving_prod_mul_swap_right μ ν