𝕜 : Type ?u.510422
G : Type u_1
H : Type ?u.510428
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : DivisionMonoid G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
μ✝ μ : Measure G
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
⊢ MeasurePreserving fun t => g * t⁻¹
𝕜 : Type ?u.510422
G : Type u_1
H : Type ?u.510428
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : DivisionMonoid G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
μ✝ μ : Measure G
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
⊢ MeasurePreserving fun t => g / t
simp_rw [div_eq_mul_inv]
no goals
𝕜 : Type ?u.510422
G : Type u_1
H : Type ?u.510428
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : DivisionMonoid G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
μ✝ μ : Measure G
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
⊢ MeasurePreserving fun t => g * t⁻¹
exact (measurePreserving_mul_left μ g).comp (measurePreserving_inv μ)