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✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
⊢ (fun z => (z.snd * z.fst, z.fst⁻¹)) = (fun z => (z.snd, z.snd⁻¹ * z.fst)) ∘ fun z => (z.snd, z.snd * z.fst)
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✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
⊢ MeasurePreserving fun z => (z.snd * z.fst, z.fst⁻¹)
convert (measurePreserving_prod_inv_mul_swap ν μ).comp (measurePreserving_prod_mul_swap μ ν)
  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✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
x y : G
⊢ ((x, y).snd * (x, y).fst, (x, y).fst⁻¹) =
    ((fun z => (z.snd, z.snd⁻¹ * z.fst)) ∘ fun z => (z.snd, z.snd * z.fst)) (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✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
⊢ (fun z => (z.snd * z.fst, z.fst⁻¹)) = (fun z => (z.snd, z.snd⁻¹ * z.fst)) ∘ fun z => (z.snd, z.snd * z.fst)
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✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
x y : G
⊢ ((x, y).snd * (x, y).fst, (x, y).fst⁻¹) =
    ((fun z => (z.snd, z.snd⁻¹ * z.fst)) ∘ fun z => (z.snd, z.snd * z.fst)) (x, y)
simp_rw [Function.comp_apply, mul_inv_rev, inv_mul_cancel_right]