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✝ : IsMulRightInvariant μ
y : G
⊢ QuasiMeasurePreserving fun x => (x, y).fst / (x, y).snd
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✝ : IsMulRightInvariant μ
⊢ QuasiMeasurePreserving fun p => p.fst / p.snd
refine' QuasiMeasurePreserving.prod_of_left measurable_div (eventually_of_forall fun y => _)
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✝ : IsMulRightInvariant μ
y : G
⊢ QuasiMeasurePreserving fun x => (x, y).fst / (x, y).snd
exact (measurePreserving_div_right μ y).quasiMeasurePreserving