awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
h_int :
  (∀ᵐ (y : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
      @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) y)) ∧
    @Integrable ℝ _ _ _ mα (fun (y : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) y) fun (z : β) ↦ ‖f z‖)
      ((Kernel.const Unit μ : (a : Unit) → Measure α) ())
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f y‖) μ

Tactic:
exact h_int.2

Premises used: And.right
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
η : Kernel Y Z
inst : IsSFiniteKernel η
κ : Kernel X Y
inst_1 : IsSFiniteKernel κ
h :
  ∀ (a : X) (s : Set Z) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : X) → Measure Z) a : Measure Z) : (a : Set Z) → ℝ≥0∞) s : ℝ≥0∞)
      (((((κ ⊗ₖ prodMkLeft X η).snd : (a : X) → Measure Z) a : Measure Z) : (a : Set Z) → ℝ≥0∞) s : ℝ≥0∞)
⊢ η ∘ₖ κ = (κ ⊗ₖ prodMkLeft X η).snd

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
η : Kernel Y Z
inst : IsSFiniteKernel η
κ : Kernel X Y
inst_1 : IsSFiniteKernel κ
a : X
s : Set Z
hs : MeasurableSet s
h :
  ∫⁻ (b : Y), (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) s ∂(κ : (a : X) → Measure Y) a =
    ∫⁻ (b : Y),
      (((prodMkLeft X η : (a : X × Y) → Measure Z) (a, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂(κ : (a : X) → Measure Y) a
⊢ Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : X) → Measure Z) a : Measure Z) : (a : Set Z) → ℝ≥0∞) s : ℝ≥0∞)
    (((((κ ⊗ₖ prodMkLeft X η).snd : (a : X) → Measure Z) a : Measure Z) : (a : Set Z) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comp_apply' _ _ _ hs, snd_apply' _ _ hs, compProd_apply (measurable_snd hs)]

Premises used: ProbabilityTheory.Kernel.snd_apply', measurable_snd, ProbabilityTheory.Kernel.comp_apply', ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
η : Kernel Y Z
inst : IsSFiniteKernel η
κ : Kernel X Y
inst_1 : IsSFiniteKernel κ
a : X
s : Set Z
hs : MeasurableSet s
⊢ ∫⁻ (b : Y), (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) s ∂(κ : (a : X) → Measure Y) a =
    ∫⁻ (b : Y),
      (((prodMkLeft X η : (a : X × Y) → Measure Z) (a, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂(κ : (a : X) → Measure Y) a

Tactic:
simp [← Set.preimage_comp]

Premises used: Set.preimage_comp
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
η : Kernel Y Z
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
⊢ (κ ⊗ₖ prodMkLeft X η).snd = η ∘ₖ κ

Tactic:
(comp_eq_snd_compProd η κ).symm

Premises used: ProbabilityTheory.Kernel.comp_eq_snd_compProd, Eq.symm
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel Y Z
inst_1 : IsSFiniteKernel η
h :
  ∀ (a : X) (s : Set (Y × Z)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((κ ⊗ₖ prodMkLeft X η : (a : X) → Measure (Y × Z)) a : Measure (Y × Z)) : (a : Set (Y × Z)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((Kernel.id ×ₖ η ∘ₖ κ : (a : X) → Measure (Y × Z)) a : Measure (Y × Z)) : (a : Set (Y × Z)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ ⊗ₖ prodMkLeft X η = Kernel.id ×ₖ η ∘ₖ κ

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel Y Z
inst_1 : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
h :
  ∫⁻ (b : Y),
      (((prodMkLeft X η : (a : X × Y) → Measure Z) (a, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : X) → Measure Y) a =
    ∫⁻ (b : Y),
      (((prodMkLeft X (Kernel.id ×ₖ η) : (a : X × Y) → Measure (Y × Z)) (a, b) : Measure (Y × Z)) :
          (a : Set (Y × Z)) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂(κ : (a : X) → Measure Y) a
h₁ : MeasurableSet (α := Y × Y × Z) (Prod.snd ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ prodMkLeft X η : (a : X) → Measure (Y × Z)) a : Measure (Y × Z)) : (a : Set (Y × Z)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.id ×ₖ η ∘ₖ κ : (a : X) → Measure (Y × Z)) a : Measure (Y × Z)) : (a : Set (Y × Z)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comp_eq_snd_compProd, compProd_apply hs, snd_apply' _ _ hs, compProd_apply]

Premises used: ProbabilityTheory.Kernel.comp_eq_snd_compProd, ProbabilityTheory.Kernel.snd_apply', ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel Y Z
inst_1 : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
⊢ MeasurableSet (α := Y × Y × Z) (Prod.snd ⁻¹' s)

Tactic:
measurable_snd hs

Premises used: measurable_snd
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel Y Z
inst_1 : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
⊢ MeasurableSet (α := Y × Y × Z) (Prod.snd ⁻¹' s)

Tactic:
exact measurable_snd hs

Premises used: measurable_snd
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel Y Z
inst_1 : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
h :
  ∫⁻ (b : Y),
      (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : X) → Measure Y) a =
    ∫⁻ (b : Y),
      ∫⁻ (b_1 : Y),
        (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞)
          (Prod.mk b_1 ⁻¹' s) ∂Measure.dirac b ∂(κ : (a : X) → Measure Y) a
⊢ ∫⁻ (b : Y),
      (((prodMkLeft X η : (a : X × Y) → Measure Z) (a, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : X) → Measure Y) a =
    ∫⁻ (b : Y),
      (((prodMkLeft X (Kernel.id ×ₖ η) : (a : X × Y) → Measure (Y × Z)) (a, b) : Measure (Y × Z)) :
          (a : Set (Y × Z)) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂(κ : (a : X) → Measure Y) a

Tactic:
simp only [prodMkLeft_apply, ← Set.preimage_comp, Prod.snd_comp_mk, Set.preimage_id_eq, id_eq,
    prod_apply' _ _ _ hs, id_apply]

Premises used: ProbabilityTheory.Kernel.prod_apply', ProbabilityTheory.Kernel.prodMkLeft_apply, Set.preimage_comp, Prod.snd_comp_mk, Set.preimage_id_eq, ProbabilityTheory.Kernel.id_apply, id_eq
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel Y Z
inst_1 : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
h :
  ∀ (b : Y),
    (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk b ⁻¹' s) =
      ∫⁻ (b_1 : Y),
        (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk b_1 ⁻¹' s) ∂Measure.dirac b
⊢ ∫⁻ (b : Y),
      (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : X) → Measure Y) a =
    ∫⁻ (b : Y),
      ∫⁻ (b_1 : Y),
        (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞)
          (Prod.mk b_1 ⁻¹' s) ∂Measure.dirac b ∂(κ : (a : X) → Measure Y) a

Tactic:
congr with b
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel Y Z
inst_1 : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
b : Y
h :
  Measurable (β := ℝ≥0∞) fun (b_1 : Y) ↦
    (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk b_1 ⁻¹' s)
⊢ (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk b ⁻¹' s) =
    ∫⁻ (b_1 : Y), (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk b_1 ⁻¹' s) ∂Measure.dirac b

Tactic:
rw [lintegral_dirac']

Premises used: MeasureTheory.lintegral_dirac'
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel Y Z
inst_1 : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
b : Y
⊢ Measurable (β := ℝ≥0∞) fun (b_1 : Y) ↦
    (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk b_1 ⁻¹' s)

Tactic:
measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel Y Z
inst_1 : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
b : Y
⊢ Measurable (β := ℝ≥0∞) fun (b_1 : Y) ↦
    (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk b_1 ⁻¹' s)

Tactic:
exact measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
pos : ∀ (hκ : IsSFiniteKernel κ), swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
neg : ∀ (hκ : ¬IsSFiniteKernel κ), swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
⊢ swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : ¬IsSFiniteKernel κ
⊢ swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z

Tactic:
simp [hκ]
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
pos : ∀ (hη : IsSFiniteKernel η), swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
neg : ∀ (hη : ¬IsSFiniteKernel η), swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
⊢ swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z

Tactic:
by_cases hη : IsSFiniteKernel η

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z

Tactic:
simp [hη]
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
pos :
  ∀ (ac : X × Z) (s : Set (T × Y)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((swap Y T ∘ₖ (κ ∥ₖ η) : (a : X × Z) → Measure (T × Y)) ac : Measure (T × Y)) : (a : Set (T × Y)) → ℝ≥0∞) s :
        ℝ≥0∞)
      ((((η ∥ₖ κ ∘ₖ swap X Z : (a : X × Z) → Measure (T × Y)) ac : Measure (T × Y)) : (a : Set (T × Y)) → ℝ≥0∞) s :
        ℝ≥0∞)
⊢ swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z

Tactic:
ext ac s hs
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
pos :
  ∫⁻ (a : Y × T),
      (Measure.dirac a.swap : (a : Set (T × Y)) → ℝ≥0∞)
        s ∂Measure.prod ((κ : (a : X) → Measure Y) ac.1) ((η : (a : Z) → Measure T) ac.2) =
    ∫⁻ (b : T),
      (((κ : (a : X) → Measure Y) ac.1 : Measure Y) : (a : Set Y) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(η : (a : Z) → Measure T) ac.2
⊢ Eq (α := ℝ≥0∞)
    ((((swap Y T ∘ₖ (κ ∥ₖ η) : (a : X × Z) → Measure (T × Y)) ac : Measure (T × Y)) : (a : Set (T × Y)) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((η ∥ₖ κ ∘ₖ swap X Z : (a : X × Z) → Measure (T × Y)) ac : Measure (T × Y)) : (a : Set (T × Y)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [comp_apply, parallelComp_apply, Measure.bind_apply hs (Kernel.aemeasurable _),
    swap_apply, lintegral_dirac' _ (Kernel.measurable_coe _ hs), parallelComp_apply' hs,
    Prod.fst_swap, Prod.snd_swap]

Premises used: MeasureTheory.Measure.bind_apply, Prod.fst_swap, ProbabilityTheory.Kernel.swap_apply, MeasureTheory.lintegral_dirac', ProbabilityTheory.Kernel.aemeasurable, ProbabilityTheory.Kernel.comp_apply, ProbabilityTheory.Kernel.parallelComp_apply', Prod.snd_swap, ProbabilityTheory.Kernel.measurable_coe, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
pos :
  ∫⁻ (y : T),
      ∫⁻ (x : Y),
        (Measure.dirac (x, y).swap : (a : Set (T × Y)) → ℝ≥0∞)
          s ∂(κ : (a : X) → Measure Y) ac.1 ∂(η : (a : Z) → Measure T) ac.2 =
    ∫⁻ (b : T),
      (((κ : (a : X) → Measure Y) ac.1 : Measure Y) : (a : Set Y) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(η : (a : Z) → Measure T) ac.2
pos₁ :
  AEMeasurable (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (fun (a : Y × T) ↦ (Measure.dirac a.swap : (a : Set (T × Y)) → ℝ≥0∞) s)
    (Measure.prod ((κ : (a : X) → Measure Y) ac.1) ((η : (a : Z) → Measure T) ac.2))
⊢ ∫⁻ (a : Y × T),
      (Measure.dirac a.swap : (a : Set (T × Y)) → ℝ≥0∞)
        s ∂Measure.prod ((κ : (a : X) → Measure Y) ac.1) ((η : (a : Z) → Measure T) ac.2) =
    ∫⁻ (b : T),
      (((κ : (a : X) → Measure Y) ac.1 : Measure Y) : (a : Set Y) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(η : (a : Z) → Measure T) ac.2

Tactic:
rw [MeasureTheory.lintegral_prod_symm]

Premises used: MeasureTheory.lintegral_prod_symm
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ AEMeasurable (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (fun (a : Y × T) ↦ (Measure.dirac a.swap : (a : Set (T × Y)) → ℝ≥0∞) s)
    (Measure.prod ((κ : (a : X) → Measure Y) ac.1) ((η : (a : Z) → Measure T) ac.2))

Tactic:
((Kernel.id.measurable_coe hs).comp measurable_swap).aemeasurable

Premises used: Measurable.aemeasurable, Measurable.comp, ProbabilityTheory.Kernel.id, measurable_swap, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ AEMeasurable (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (fun (a : Y × T) ↦ (Measure.dirac a.swap : (a : Set (T × Y)) → ℝ≥0∞) s)
    (Measure.prod ((κ : (a : X) → Measure Y) ac.1) ((η : (a : Z) → Measure T) ac.2))

Tactic:
exact ((Kernel.id.measurable_coe hs).comp measurable_swap).aemeasurable

Premises used: Measurable.aemeasurable, Measurable.comp, ProbabilityTheory.Kernel.id, measurable_swap, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
pos :
  ∀ (d : T),
    ∫⁻ (x : Y), (Measure.dirac (x, d).swap : (a : Set (T × Y)) → ℝ≥0∞) s ∂(κ : (a : X) → Measure Y) ac.1 =
      (((κ : (a : X) → Measure Y) ac.1 : Measure Y) : (a : Set Y) → ℝ≥0∞) (Prod.mk d ⁻¹' s)
⊢ ∫⁻ (y : T),
      ∫⁻ (x : Y),
        (Measure.dirac (x, y).swap : (a : Set (T × Y)) → ℝ≥0∞)
          s ∂(κ : (a : X) → Measure Y) ac.1 ∂(η : (a : Z) → Measure T) ac.2 =
    ∫⁻ (b : T),
      (((κ : (a : X) → Measure Y) ac.1 : Measure Y) : (a : Set Y) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(η : (a : Z) → Measure T) ac.2

Tactic:
congr with d
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
d : T
pos :
  ∫⁻ (a : Y) in Prod.mk d ⁻¹' s, (1 ∘ Prod.mk d) a ∂(κ : (a : X) → Measure Y) ac.1 =
    (((κ : (a : X) → Measure Y) ac.1 : Measure Y) : (a : Set Y) → ℝ≥0∞) (Prod.mk d ⁻¹' s)
⊢ ∫⁻ (x : Y), (Measure.dirac (x, d).swap : (a : Set (T × Y)) → ℝ≥0∞) s ∂(κ : (a : X) → Measure Y) ac.1 =
    (((κ : (a : X) → Measure Y) ac.1 : Measure Y) : (a : Set Y) → ℝ≥0∞) (Prod.mk d ⁻¹' s)

Tactic:
simp_rw [Prod.swap_prod_mk, Measure.dirac_apply' _ hs, ← Set.indicator_comp_right,
    lintegral_indicator (measurable_prodMk_left hs)]

Premises used: MeasureTheory.Measure.dirac_apply', Prod.swap_prod_mk, Set.indicator_comp_right, MeasureTheory.lintegral_indicator, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
d : T
⊢ ∫⁻ (a : Y) in Prod.mk d ⁻¹' s, (1 ∘ Prod.mk d) a ∂(κ : (a : X) → Measure Y) ac.1 =
    (((κ : (a : X) → Measure Y) ac.1 : Measure Y) : (a : Set Y) → ℝ≥0∞) (Prod.mk d ⁻¹' s)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst : IsSFiniteKernel η
ξ : Kernel Z T
inst_1 : IsSFiniteKernel ξ
pos : ∀ (hκ : IsSFiniteKernel κ), Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)
neg : ∀ (hκ : ¬IsSFiniteKernel κ), Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)
⊢ Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst : IsSFiniteKernel η
ξ : Kernel Z T
inst_1 : IsSFiniteKernel ξ
hκ : ¬IsSFiniteKernel κ
⊢ Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)

Tactic:
simp [hκ]
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst : IsSFiniteKernel η
ξ : Kernel Z T
inst_1 : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
pos :
  ∀ (a : X × X') (s : Set (Y × T)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) : (a : X × X') → Measure (Y × T)) a : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((κ ∥ₖ (ξ ∘ₖ η) : (a : X × X') → Measure (Y × T)) a : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst : IsSFiniteKernel η
ξ : Kernel Z T
inst_1 : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
pos :
  ∫⁻ (x : Y),
      ∫⁻ (y : Z),
        (((Kernel.id ∥ₖ ξ : (a : Y × Z) → Measure (Y × T)) (x, y) : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞)
          s ∂(η : (a : X') → Measure Z) a.2 ∂(κ : (a : X) → Measure Y) a.1 =
    (((κ ∥ₖ (ξ ∘ₖ η) : (a : X × X') → Measure (Y × T)) a : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) : (a : X × X') → Measure (Y × T)) a : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ ∥ₖ (ξ ∘ₖ η) : (a : X × X') → Measure (Y × T)) a : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comp_apply' _ _ _ hs, parallelComp_apply,
    MeasureTheory.lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_prod, ProbabilityTheory.Kernel.measurable_coe, ProbabilityTheory.Kernel.comp_apply', ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.KernelLemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst : IsSFiniteKernel η
ξ : Kernel Z T
inst_1 : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
pos :
  ∫⁻ (x : Y),
      ∫⁻ (y : Z),
        (((Kernel.id ∥ₖ ξ : (a : Y × Z) → Measure (Y × T)) (x, y) : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞)
          s ∂(η : (a : X') → Measure Z) a.2 ∂(κ : (a : X) → Measure Y) a.1 =
    ∫⁻ (x : Y),
      (((ξ ∘ₖ η : (a : X') → Measure T) a.2 : Measure T) : (a : Set T) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ : (a : X) → Measure Y) a.1
⊢ ∫⁻ (x : Y),
      ∫⁻ (y : Z),
        (((Kernel.id ∥ₖ ξ : (a : Y × Z) → Measure (Y × T)) (x, y) : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞)
          s ∂(η : (a : X') → Measure Z) a.2 ∂(κ : (a : X) → Measure Y) a.1 =
    (((κ ∥ₖ (ξ ∘ₖ η) : (a : X × X') → Measure (Y × T)) a : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞) s

Tactic:
rw [parallelComp_apply, Measure.prod_apply hs]

Premises used: MeasureTheory.Measure.prod_apply, ProbabilityTheory.Kernel.parallelComp_apply