awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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 η
⊢ κ ⊗ₖ prodMkLeft X η = Kernel.id ×ₖ η ∘ₖ κ
have 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∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ 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∞)
have 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
Tactic: rw [comp_eq_snd_compProd, compProd_apply hs, snd_apply' _ _ hs, compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ 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∞)
have h₁ : MeasurableSet (α := Y × Y × Z) (Prod.snd ⁻¹' s)
Tactic: rw [comp_eq_snd_compProd, compProd_apply hs, snd_apply' _ _ hs, compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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),
      (((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
have 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
Tactic: simp only [prodMkLeft_apply, ← Set.preimage_comp, Prod.snd_comp_mk, Set.preimage_id_eq, id_eq,
    prod_apply' _ _ _ hs, id_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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),
      (((η : (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
have 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
Tactic: congr with b
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ (((η : (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
have h : Measurable (β := ℝ≥0∞) fun (b_1 : Y) ↦
  (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk b_1 ⁻¹' s)
Tactic: rw [lintegral_dirac']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
have pos : ∀ (hκ : IsSFiniteKernel κ), swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
have neg : ∀ (hκ : ¬IsSFiniteKernel κ), swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
have pos : ∀ (hη : IsSFiniteKernel η), swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
Tactic: by_cases hη : IsSFiniteKernel η
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
have neg : ∀ (hη : ¬IsSFiniteKernel η), swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
Tactic: by_cases hη : IsSFiniteKernel η
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
have 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∞)
Tactic: ext ac s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ 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∞)
have 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
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ ∫⁻ (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
have 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
Tactic: rw [MeasureTheory.lintegral_prod_symm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ ∫⁻ (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
have 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))
Tactic: rw [MeasureTheory.lintegral_prod_symm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ ∫⁻ (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
have 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)
Tactic: congr with d
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ ∫⁻ (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)
have 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)
Tactic: simp_rw [Prod.swap_prod_mk, Measure.dirac_apply' _ hs, ← Set.indicator_comp_right,
    lintegral_indicator (measurable_prodMk_left hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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 ξ
⊢ Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)
have pos : ∀ (hκ : IsSFiniteKernel κ), Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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 ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)
⊢ Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)
have neg : ∀ (hκ : ¬IsSFiniteKernel κ), Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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 ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)
have 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∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ 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∞)
have 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
Tactic: rw [comp_apply' _ _ _ hs, parallelComp_apply,
    MeasureTheory.lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ ∫⁻ (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
have 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
Tactic: rw [parallelComp_apply, Measure.prod_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
⊢ ∫⁻ (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
have 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 T) a.2 : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
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 T) a.2 : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
have pos : ∫⁻ (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 =
  ∫⁻ (b : Z),
    (((ξ : (a : Z) → Measure T) b : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂(η : (a : X') → Measure Z) a.2
Tactic: rw [comp_apply' _ _ _ (measurable_prodMk_left hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
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 =
    ∫⁻ (b : Z),
      (((ξ : (a : Z) → Measure T) b : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂(η : (a : X') → Measure Z) a.2
have pos : ∀ (y : Z),
  Eq (α := ℝ≥0∞)
    ((((Kernel.id ∥ₖ ξ : (a : Y × Z) → Measure (Y × T)) (x, y) : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ξ : (a : Z) → Measure T) y : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞)
Tactic: congr with y
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
x : Y
y : Z
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.id ∥ₖ ξ : (a : Y × Z) → Measure (Y × T)) (x, y) : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ξ : (a : Z) → Measure T) y : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞)
have pos : ∫⁻ (b : Y),
    (((ξ : (a : Z) → Measure T) (x, y).2 : Measure T) : (a : Set T) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(Kernel.id : (a : Y) → Measure Y) (x, y).1 =
  (((ξ : (a : Z) → Measure T) y : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
Tactic: rw [parallelComp_apply' hs, Kernel.id_apply,
    lintegral_dirac' _ (measurable_measure_prodMk_left hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
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
x : Y
y : Z
pos :
  ∫⁻ (b : Y),
      (((ξ : (a : Z) → Measure T) (x, y).2 : Measure T) : (a : Set T) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(Kernel.id : (a : Y) → Measure Y) (x, y).1 =
    (((ξ : (a : Z) → Measure T) y : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.id ∥ₖ ξ : (a : Y × Z) → Measure (Y × T)) (x, y) : Measure (Y × T)) : (a : Set (Y × T)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ξ : (a : Z) → Measure T) y : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞)
have pos₁ : ∫⁻ (b : Y),
    (((ξ : (a : Z) → Measure T) (x, y).2 : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂Measure.dirac (x, y).1 =
  (((ξ : (a : Z) → Measure T) y : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
Tactic: rw [parallelComp_apply' hs, Kernel.id_apply,
    lintegral_dirac' _ (measurable_measure_prodMk_left hs)]