-- Mathlib/Probability/Kernel/MeasurableIntegral.lean
theorem StronglyMeasurable.integral_kernel_prod_left'' {f : γ × β → E} (hf : StronglyMeasurable f) :
    StronglyMeasurable fun y => ∫ x, f (x, y) ∂η (a, y)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst✝² : NormedAddCommGroup E
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable ((fun y => ∫ (x : γ), (fun u => f (u.1, u.2.2)) (x, y) ∂η y) ∘ fun x => (a, x))

Tactic:
apply StronglyMeasurable.comp_measurable _ (measurable_prod_mk_left (m := mα))

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst✝² : NormedAddCommGroup E
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun y => ∫ (x : γ), (fun u => f (u.1, u.2.2)) (x, y) ∂η y

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst✝² : NormedAddCommGroup E
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun y => ∫ (x : γ), f (x, y) ∂η (a, y)

Tactic:
change
  StronglyMeasurable
    ((fun y => ∫ x, (fun u : γ × α × β => f (u.1, u.2.2)) (x, y) ∂η y) ∘ fun x => (a, x))

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst✝² : NormedAddCommGroup E
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable ((fun y => ∫ (x : γ), (fun u => f (u.1, u.2.2)) (x, y) ∂η y) ∘ fun x => (a, x))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst✝² : NormedAddCommGroup E
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
this : StronglyMeasurable fun y => ∫ (x : γ), (f ∘ fun a => (a.1, a.2.2)) (x, y) ∂η y
⊢ StronglyMeasurable fun y => ∫ (x : γ), (fun u => f (u.1, u.2.2)) (x, y) ∂η y

Tactic:
simpa using this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst✝² : NormedAddCommGroup E
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun y => ∫ (x : γ), (fun u => f (u.1, u.2.2)) (x, y) ∂η y

Tactic:
have := MeasureTheory.StronglyMeasurable.integral_kernel_prod_left' (κ := η)
  (hf.comp_measurable (measurable_fst.prod_mk measurable_snd.snd))

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst✝² : NormedAddCommGroup E
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
this : StronglyMeasurable fun y => ∫ (x : γ), (f ∘ fun a => (a.1, a.2.2)) (x, y) ∂η y
⊢ StronglyMeasurable fun y => ∫ (x : γ), (fun u => f (u.1, u.2.2)) (x, y) ∂η y