-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem condExp_prod_ae_eq_integral_condDistrib' [NormedSpace ℝ F] [CompleteSpace F]
    (hX : Measurable X) (hY : AEMeasurable Y μ)
    (hf_int : Integrable f (μ.map fun a => (X a, Y a))) :
    μ[fun a => f (X a, Y a)|mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a,y) ∂condDistrib Y X μ (X a)

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int' : Integrable (fun a => f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ⊤
⊢ ∫ (y : β), ∫ (y_1 : Ω), f (y, y_1) ∂(condDistrib Y X μ) y ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ

Tactic:
rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prod_mk₀ hY, condDistrib,
  Measure.setIntegral_condKernel_univ_right ht hf_int.integrableOn,
  setIntegral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prod_mk hY),
  mk_preimage_prod, preimage_univ, inter_univ]

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int' : Integrable (fun a => f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ⊤
⊢ AEStronglyMeasurable (fun x' => ∫ (y : Ω), f (x', y) ∂(condDistrib Y X μ) x') (Measure.map X (μ.restrict (X ⁻¹' t)))

Tactic:
rw [← Measure.restrict_map hX ht]

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int' : Integrable (fun a => f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ⊤
⊢ AEStronglyMeasurable (fun x' => ∫ (y : Ω), f (x', y) ∂(condDistrib Y X μ) x') ((Measure.map X μ).restrict t)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int' : Integrable (fun a => f (X a, Y a)) μ
⊢ ∀ (s : Set α),
    MeasurableSet s →
      μ s < ⊤ → ∫ (x : α) in s, ∫ (y : Ω), f (X x, y) ∂(condDistrib Y X μ) (X x) ∂μ = ∫ (x : α) in s, f (X x, Y x) ∂μ

Tactic:
rintro s ⟨t, ht, rfl⟩ _

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int' : Integrable (fun a => f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ⊤
⊢ ∫ (x : α) in X ⁻¹' t, ∫ (y : Ω), f (X x, y) ∂(condDistrib Y X μ) (X x) ∂μ = ∫ (x : α) in X ⁻¹' t, f (X x, Y x) ∂μ

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int' : Integrable (fun a => f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ⊤
⊢ ∫ (y : β), ∫ (y_1 : Ω), f (y, y_1) ∂(condDistrib Y X μ) y ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ

case refine_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int' : Integrable (fun a => f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ⊤
⊢ AEStronglyMeasurable (fun x' => ∫ (y : Ω), f (x', y) ∂(condDistrib Y X μ) x') (Measure.map X (μ.restrict (X ⁻¹' t)))

Tactic:
swap

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int' : Integrable (fun a => f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ⊤
⊢ AEStronglyMeasurable (fun x' => ∫ (y : Ω), f (x', y) ∂(condDistrib Y X μ) x') (Measure.map X (μ.restrict (X ⁻¹' t)))

case refine_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int' : Integrable (fun a => f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ⊤
⊢ ∫ (y : β), ∫ (y_1 : Ω), f (y, y_1) ∂(condDistrib Y X μ) y ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ

Proof state:
case refine_3
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int' : Integrable (fun a => f (X a, Y a)) μ
⊢ AEStronglyMeasurable (fun a => ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)) μ

Tactic:
exact aestronglyMeasurable_integral_condDistrib hX.aemeasurable hY hf_int.1

Result:
no goals