no goals
𝕜 : Type ?u.367252
G : Type u_1
H : Type ?u.367258
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSpace H
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : IsMulRightInvariant μ
g : G
⊢ MeasurePreserving fun x => x / g
simp_rw [div_eq_mul_inv, measurePreserving_mul_right μ g⁻¹]