-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_apply_eq_compProdFun (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ)
    [IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
    (κ ⊗ₖ η) a s = 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 η
a : α
hs : MeasurableSet s
⊢ ({
          toFun := fun a =>
            let_fun this := ⋯;
            Measure.ofMeasurable (fun s x => κ.compProdFun η a s) ⋯ ⋯,
          measurable' := ⋯ }
        a)
      s =
    κ.compProdFun η a s

case hc
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ IsSFiniteKernel κ ∧ IsSFiniteKernel η

Tactic:
swap

Result:
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ IsSFiniteKernel κ ∧ IsSFiniteKernel η

α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ({
          toFun := fun a =>
            let_fun this := ⋯;
            Measure.ofMeasurable (fun s x => κ.compProdFun η a s) ⋯ ⋯,
          measurable' := ⋯ }
        a)
      s =
    κ.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 η
a : α
hs : MeasurableSet s
⊢ (Measure.ofMeasurable (fun s x => κ.compProdFun η a s) ⋯ ⋯) s = ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a

Tactic:
rw [Measure.ofMeasurable_apply _ 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 η
a : α
hs : MeasurableSet s
⊢ κ.compProdFun η a s = ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a

Proof state:
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ IsSFiniteKernel κ ∧ IsSFiniteKernel η

Tactic:
constructor <;> infer_instance

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 η
a : α
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = κ.compProdFun η a s

Tactic:
rw [compProd, dif_pos]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ({
          toFun := fun a =>
            let_fun this := ⋯;
            Measure.ofMeasurable (fun s x => κ.compProdFun η a s) ⋯ ⋯,
          measurable' := ⋯ }
        a)
      s =
    κ.compProdFun η a s

case hc
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ IsSFiniteKernel κ ∧ IsSFiniteKernel η

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 η
a : α
hs : MeasurableSet s
⊢ ({
          toFun := fun a =>
            let_fun this := ⋯;
            Measure.ofMeasurable (fun s x => κ.compProdFun η a s) ⋯ ⋯,
          measurable' := ⋯ }
        a)
      s =
    κ.compProdFun η a s

Tactic:
change
  Measure.ofMeasurable (fun s _ => compProdFun κ η a s) (compProdFun_empty κ η a)
      (compProdFun_iUnion κ η a) s =
    ∫⁻ b, η (a, b) {c | (b, c) ∈ s} ∂κ a

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ (Measure.ofMeasurable (fun s x => κ.compProdFun η a s) ⋯ ⋯) s = ∫⁻ (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 η
a : α
hs : MeasurableSet s
⊢ κ.compProdFun η a s = ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a

Tactic:
rfl

Result:
no goals