-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem measurable_compProdFun (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ)
    [IsSFiniteKernel η] (hs : MeasurableSet s) :
    Measurable fun a ↦ compProdFun κ η a s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
this : (Function.uncurry fun a b => (η (a, b)) {c | (b, c) ∈ s}) = fun p => (η p) {c | (p.2, c) ∈ s}
⊢ Measurable fun p => (η p) {c | (p.2, c) ∈ s}

Tactic:
exact measurable_kernel_prod_mk_left (measurable_fst.snd.prod_mk measurable_snd hs)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
h_meas : Measurable (Function.uncurry fun a b => (η (a, b)) {c | (b, c) ∈ s})
⊢ Measurable fun a => ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a

Tactic:
exact h_meas.lintegral_kernel_prod_right

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
⊢ (Function.uncurry fun a b => (η (a, b)) {c | (b, c) ∈ s}) = fun p => (η p) {c | (p.2, c) ∈ s}

Tactic:
ext1 p

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
p : α × β
⊢ Function.uncurry (fun a b => (η (a, b)) {c | (b, c) ∈ s}) p = (η p) {c | (p.2, c) ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
⊢ Measurable fun a => κ.compProdFun η a s

Tactic:
simp only [compProdFun]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
⊢ Measurable fun a => ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
p : α × β
⊢ Function.uncurry (fun a b => (η (a, b)) {c | (b, c) ∈ s}) p = (η p) {c | (p.2, c) ∈ s}

Tactic:
rw [Function.uncurry_apply_pair]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
this : (Function.uncurry fun a b => (η (a, b)) {c | (b, c) ∈ s}) = fun p => (η p) {c | (p.2, c) ∈ s}
⊢ Measurable (Function.uncurry fun a b => (η (a, b)) {c | (b, c) ∈ s})

Tactic:
rw [this]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
this : (Function.uncurry fun a b => (η (a, b)) {c | (b, c) ∈ s}) = fun p => (η p) {c | (p.2, c) ∈ s}
⊢ Measurable fun p => (η p) {c | (p.2, c) ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
⊢ Measurable fun a => ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a

Tactic:
have h_meas : Measurable (Function.uncurry fun a b => η (a, b) {c : γ | (b, c) ∈ s}) := by
  have : (Function.uncurry fun a b => η (a, b) {c : γ | (b, c) ∈ s})
      = fun p ↦ η p {c : γ | (p.2, c) ∈ s} := by
    ext1 p
    rw [Function.uncurry_apply_pair]
  rw [this]
  exact measurable_kernel_prod_mk_left (measurable_fst.snd.prod_mk measurable_snd hs)

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
h_meas : Measurable (Function.uncurry fun a b => (η (a, b)) {c | (b, c) ∈ s})
⊢ Measurable fun a => ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
⊢ Measurable (Function.uncurry fun a b => (η (a, b)) {c | (b, c) ∈ s})

Tactic:
have : (Function.uncurry fun a b => η (a, b) {c : γ | (b, c) ∈ s})
    = fun p ↦ η p {c : γ | (p.2, c) ∈ s} := by
  ext1 p
  rw [Function.uncurry_apply_pair]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hs : MeasurableSet s
this : (Function.uncurry fun a b => (η (a, b)) {c | (b, c) ∈ s}) = fun p => (η p) {c | (p.2, c) ∈ s}
⊢ Measurable (Function.uncurry fun a b => (η (a, b)) {c | (b, c) ∈ s})