G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
⊢ Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
⊢ Measurable fun x => ↑↑μ ((fun y => y * x) ⁻¹' s)
suffices
  Measurable fun y =>
    μ ((fun x => (x, y)) ⁻¹' ((fun z : G × G => ((1 : G), z.1 * z.2)) ⁻¹' univ ×ˢ s))
  by convert this using 1; ext1 x; congr 1 with y : 1; simp
case hs
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
⊢ MeasurableSet ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s)
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
⊢ Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
apply measurable_measure_prod_mk_right
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
⊢ MeasurableSpace G
case hs
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
⊢ MeasurableSet ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s)
apply measurable_const.prod_mk measurable_mul (MeasurableSet.univ.prod hs)
no goals
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
⊢ MeasurableSpace G
infer_instance
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
hs : MeasurableSet s
this : Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
⊢ (fun x => ↑↑μ ((fun y => y * x) ⁻¹' s)) = fun y =>
    ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
⊢ Measurable fun x => ↑↑μ ((fun y => y * x) ⁻¹' s)
convert this using 1
case h.e'_5.h
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
x : G
⊢ ↑↑μ ((fun y => y * x) ⁻¹' s) = ↑↑μ ((fun x_1 => (x_1, x)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
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
hs : MeasurableSet s
this : Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
⊢ (fun x => ↑↑μ ((fun y => y * x) ⁻¹' s)) = fun y =>
    ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
ext1 x
case h.e'_5.h.e_a.h
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
x y : G
⊢ y ∈ (fun y => y * x) ⁻¹' s ↔ y ∈ (fun x_1 => (x_1, x)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s)
case h.e'_5.h
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
x : G
⊢ ↑↑μ ((fun y => y * x) ⁻¹' s) = ↑↑μ ((fun x_1 => (x_1, x)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
congr 1 with y : 1
no goals
case h.e'_5.h.e_a.h
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
x y : G
⊢ y ∈ (fun y => y * x) ⁻¹' s ↔ y ∈ (fun x_1 => (x_1, x)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s)
simp