-- 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_1
α : 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 α
x✝¹ : MeasurableSet s
x✝ : μ s < ⊤
⊢ IntegrableOn (fun a => ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)) s μ

Tactic:
exact (hf_int.integral_condDistrib hX.aemeasurable hY).integrableOn

Result:
no goals

Proof state:
α : 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)) μ
⊢ μ[fun a => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᶠ[ae μ] fun a => ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)

Tactic:
refine (ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le hf_int' (fun s _ _ => ?_) ?_ ?_).symm

Result:
case refine_1
α : 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 α
x✝¹ : MeasurableSet s
x✝ : μ s < ⊤
⊢ IntegrableOn (fun a => ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)) s μ

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) ∂μ

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)) μ