-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem snd_map_prod_mk₀ {X : α → β} {Y : α → γ} {μ : Measure α} (hX : AEMeasurable X μ) :
    (μ.map fun a => (X a, Y a)).snd = μ.map Y

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable (fun x => (X x, Y x)) μ
⊢ AEMeasurable Y μ

Tactic:
exact measurable_snd.comp_aemeasurable hY

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
⊢ (map (fun a => (X a, Y a)) μ).snd = map Y μ

Tactic:
by_cases hY : AEMeasurable Y μ

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
⊢ (map (fun a => (X a, Y a)) μ).snd = map Y μ

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
⊢ (map (fun a => (X a, Y a)) μ).snd = map Y μ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
⊢ ¬AEMeasurable (fun x => (X x, Y x)) μ

Tactic:
contrapose! hY

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable (fun x => (X x, Y x)) μ
⊢ AEMeasurable Y μ

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
⊢ (map (fun a => (X a, Y a)) μ).snd = map Y μ

Tactic:
have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by
  contrapose! hY; exact measurable_snd.comp_aemeasurable hY

Result:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
this : ¬AEMeasurable (fun x => (X x, Y x)) μ
⊢ (map (fun a => (X a, Y a)) μ).snd = map Y μ

Proof state:
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
s : Set γ
hs : MeasurableSet s
⊢ (map (fun a => (X a, Y a)) μ).snd s = (map Y μ) s

Tactic:
rw [Measure.snd_apply hs, Measure.map_apply_of_aemeasurable (hX.prod_mk hY) (measurable_snd hs),
  Measure.map_apply_of_aemeasurable hY hs, ← univ_prod, mk_preimage_prod, preimage_univ,
  univ_inter]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
this : ¬AEMeasurable (fun x => (X x, Y x)) μ
⊢ (map (fun a => (X a, Y a)) μ).snd = map Y μ

Tactic:
simp [map_of_not_aemeasurable, hY, this]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
⊢ (map (fun a => (X a, Y a)) μ).snd = map Y μ

Tactic:
ext1 s hs

Result:
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
s : Set γ
hs : MeasurableSet s
⊢ (map (fun a => (X a, Y a)) μ).snd s = (map Y μ) s