case h.e'_5
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 μ
inst✝ : IsMulRightInvariant ν
⊢ (fun z => (z.fst * z.snd, z.fst⁻¹)) = (fun z => (z.snd, z.fst / z.snd)) ∘ fun z => (z.snd, z.fst * z.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 μ
inst✝ : IsMulRightInvariant ν
⊢ MeasurePreserving fun z => (z.fst * z.snd, z.fst⁻¹)
convert (measurePreserving_prod_div_swap ν μ).comp (measurePreserving_prod_mul_swap_right μ ν)
  using 1
case h.e'_5.h.mk
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 μ
inst✝ : IsMulRightInvariant ν
x y : G
⊢ ((x, y).fst * (x, y).snd, (x, y).fst⁻¹) = ((fun z => (z.snd, z.fst / z.snd)) ∘ fun z => (z.snd, z.fst * z.snd)) (x, y)
case h.e'_5
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 μ
inst✝ : IsMulRightInvariant ν
⊢ (fun z => (z.fst * z.snd, z.fst⁻¹)) = (fun z => (z.snd, z.fst / z.snd)) ∘ fun z => (z.snd, z.fst * z.snd)
ext1 ⟨x, y⟩
no goals
case h.e'_5.h.mk
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 μ
inst✝ : IsMulRightInvariant ν
x y : G
⊢ ((x, y).fst * (x, y).snd, (x, y).fst⁻¹) = ((fun z => (z.snd, z.fst / z.snd)) ∘ fun z => (z.snd, z.fst * z.snd)) (x, y)
simp_rw [Function.comp_apply, div_mul_eq_div_div_swap, div_self', one_div]