theorem
MeasureTheory.Measure.compProd_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{f : β → γ}
(hf : Measurable f)
: