-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem skew_product [SFinite μa] [SFinite μc] {f : α → β} (hf : MeasurePreserving f μa μb)
    {g : α → γ → δ} (hgm : Measurable (uncurry g)) (hg : ∀ᵐ a ∂μa, map (g a) μc = μd) :
    MeasurePreserving (fun p : α × γ => (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)

Proof state:
case map_eq.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p => (f p.1, g p.1 p.2)
h✝ : NeZero μa
⊢ map (fun p => (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd

Tactic:
have sf : SFinite μd := by
  obtain ⟨a, ha⟩ : ∃ a, map (g a) μc = μd := hg.exists
  rw [← ha]
  infer_instance

Result:
case map_eq.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p => (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
⊢ map (fun p => (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
⊢ MeasurePreserving (fun p => (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)

Tactic:
have : Measurable fun p : α × γ => (f p.1, g p.1 p.2) := (hf.1.comp measurable_fst).prod_mk hgm

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p => (f p.1, g p.1 p.2)
⊢ MeasurePreserving (fun p => (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)

Proof state:
case map_eq.inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p => (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
⊢ (map (fun p => (f p.1, g p.1 p.2)) (μa.prod μc)) s = (μb.prod μd) s

Tactic:
rw [map_apply this hs, prod_apply (this hs), prod_apply hs,
  ← hf.lintegral_comp (measurable_measure_prod_mk_left hs)]

Result:
case map_eq.inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p => (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), μc (Prod.mk x ⁻¹' ((fun p => (f p.1, g p.1 p.2)) ⁻¹' s)) ∂μa = ∫⁻ (a : α), μd (Prod.mk (f a) ⁻¹' s) ∂μa

Proof state:
case map_eq.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μc
f : α → β
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.1, g p.1 p.2)
inst✝ : SFinite 0
hf : MeasurePreserving f 0 μb
hg : ∀ᵐ (a : α) ∂0, map (g a) μc = μd
⊢ map (fun p => (f p.1, g p.1 p.2)) (Measure.prod 0 μc) = μb.prod μd

Tactic:
simp [← hf.map_eq]

Result:
no goals

Proof state:
case map_eq.inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p => (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), μc (Prod.mk x ⁻¹' ((fun p => (f p.1, g p.1 p.2)) ⁻¹' s)) ∂μa = ∫⁻ (a : α), μd (Prod.mk (f a) ⁻¹' s) ∂μa

Tactic:
apply lintegral_congr_ae

Result:
case map_eq.inr.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p => (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
⊢ (fun a => μc (Prod.mk a ⁻¹' ((fun p => (f p.1, g p.1 p.2)) ⁻¹' s))) =ᶠ[ae μa] fun a => μd (Prod.mk (f a) ⁻¹' s)

Proof state:
case map_eq.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p => (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
⊢ map (fun p => (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd

Tactic:
ext s hs

Result:
case map_eq.inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p => (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
⊢ (map (fun p => (f p.1, g p.1 p.2)) (μa.prod μc)) s = (μb.prod μd) s