-- Mathlib/MeasureTheory/Group/Prod.lean
theorem measurable_measure_mul_right (hs : MeasurableSet s) :
    Measurable fun x => μ ((fun y => y * x) ⁻¹' s)

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
⊢ Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))

Tactic:
apply measurable_measure_prod_mk_right

Result:
case hs
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
⊢ MeasurableSet ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)

Proof state:
case h.e'_5
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))
⊢ (fun x => μ ((fun y => y * x) ⁻¹' s)) = fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))

Tactic:
ext1 x

Result:
case h.e'_5.h
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))
x : G
⊢ μ ((fun y => y * x) ⁻¹' s) = μ ((fun x_1 => (x_1, x)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
⊢ Measurable fun x => μ ((fun y => y * x) ⁻¹' s)

Tactic:
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

Result:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
⊢ Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))
⊢ Measurable fun x => μ ((fun y => y * x) ⁻¹' s)

Tactic:
convert this using 1

Result:
case h.e'_5
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))
⊢ (fun x => μ ((fun y => y * x) ⁻¹' s)) = fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))

Proof state:
case hs
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
⊢ MeasurableSet ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)

Tactic:
apply measurable_const.prod_mk measurable_mul (MeasurableSet.univ.prod hs)

Result:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
⊢ MeasurableSpace G

Proof state:
case h.e'_5.h.h.e_6.h.h
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))
x y : G
⊢ y ∈ (fun y => y * x) ⁻¹' s ↔ y ∈ (fun x_1 => (x_1, x)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
⊢ MeasurableSpace G

Tactic:
infer_instance

Result:
no goals

Proof state:
case h.e'_5.h
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))
x : G
⊢ μ ((fun y => y * x) ⁻¹' s) = μ ((fun x_1 => (x_1, x)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))

Tactic:
congr 1 with y : 1

Result:
case h.e'_5.h.h.e_6.h.h
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))
x y : G
⊢ y ∈ (fun y => y * x) ⁻¹' s ↔ y ∈ (fun x_1 => (x_1, x)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)