awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 T) a.2 : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' 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

Tactic:
congr with x
-- 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
x : Y
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
⊢ ∫⁻ (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:
rw [comp_apply' _ _ _ (measurable_prodMk_left hs)]

Premises used: ProbabilityTheory.Kernel.comp_apply', 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
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
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∞)
⊢ ∫⁻ (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:
congr with y
-- 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
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)
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)
pos₂ pos₃ :
  Eq (α := ℝ≥0∞)
    ((((ξ : (a : Z) → Measure T) (x, y).2 : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk (x, y).1 ⁻¹' s) : ℝ≥0∞)
    ((((ξ : (a : Z) → Measure T) y : Measure T) : (a : Set T) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞)
⊢ 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:
rw [parallelComp_apply' hs, Kernel.id_apply,
    lintegral_dirac' _ (measurable_measure_prodMk_left hs)]

Premises used: MeasureTheory.lintegral_dirac', ProbabilityTheory.Kernel.parallelComp_apply', measurable_measure_prodMk_left, ProbabilityTheory.Kernel.id_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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
simp_rw : ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = swap Y T ∘ₖ swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)
simp_rw₁ : ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = Kernel.id ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ))

Tactic:
simp_rw [← comp_assoc, swap_swap, id_comp]

Premises used: ProbabilityTheory.Kernel.comp_assoc, ProbabilityTheory.Kernel.swap_swap, ProbabilityTheory.Kernel.id_comp
-- 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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
rw rw₁ : swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ))
⊢ swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ))

Tactic:
rw [this]
-- 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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
simp_rw : swap Y T ∘ₖ swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ
simp_rw₁ : Kernel.id ∘ₖ (ξ ∘ₖ η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ
⊢ swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)) = ξ ∘ₖ η ∥ₖ κ

Tactic:
simp_rw [← comp_assoc, swap_swap, id_comp]

Premises used: ProbabilityTheory.Kernel.comp_assoc, ProbabilityTheory.Kernel.swap_swap, ProbabilityTheory.Kernel.id_comp
-- 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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
calc : ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ))
calc₁ : swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ))
calc₂ : swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)) = ξ ∘ₖ η ∥ₖ κ
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ

Tactic:
calc ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ)
    _ = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)) := by
      simp_rw [← comp_assoc, swap_swap, id_comp]
    _ = swap Y T ∘ₖ (swap T Y ∘ₖ ((ξ ∘ₖ η) ∥ₖ κ)) := by rw [this]
    _ = ξ ∘ₖ η ∥ₖ κ := by simp_rw [← comp_assoc, swap_swap, id_comp]

Premises used: ProbabilityTheory.Kernel.comp, ProbabilityTheory.Kernel.id, ProbabilityTheory.Kernel.swap, ProbabilityTheory.Kernel.parallelComp
-- 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 ξ
suffices : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ

Tactic:
suffices swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ ((ξ ∘ₖ η) ∥ₖ κ) by
    calc ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ)
    _ = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)) := by
      simp_rw [← comp_assoc, swap_swap, id_comp]
    _ = swap Y T ∘ₖ (swap T Y ∘ₖ ((ξ ∘ₖ η) ∥ₖ κ)) := by rw [this]
    _ = ξ ∘ₖ η ∥ₖ κ := by simp_rw [← comp_assoc, swap_swap, id_comp]
-- 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 ξ
simp_rw : Kernel.id ∥ₖ ξ ∘ₖ swap Z Y ∘ₖ (η ∥ₖ κ) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
simp_rw₁ : Kernel.id ∥ₖ ξ ∘ₖ (swap Z Y ∘ₖ (η ∥ₖ κ)) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
simp_rw₂ : Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η ∘ₖ swap X' X) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
simp_rw₃ : Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) ∘ₖ swap X' X = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
⊢ swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)

Tactic:
simp_rw [swap_parallelComp, comp_assoc, swap_parallelComp, ← comp_assoc,
    parallelComp_id_left_comp_parallelComp]

Premises used: ProbabilityTheory.Kernel.comp_assoc, ProbabilityTheory.Kernel.swap_parallelComp, ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp
-- 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
X' : Type u_5
Y' : Type u_6
Z' : Type u_7
mX' : MeasurableSpace X'
mY' : MeasurableSpace Y'
mZ' : MeasurableSpace Z'
inst : IsSFiniteKernel κ
η : Kernel Y Z
inst_1 : IsSFiniteKernel η
κ' : Kernel X' Y'
inst_2 : IsSFiniteKernel κ'
η' : Kernel Y' Z'
inst_3 : IsSFiniteKernel η'
rw : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = Kernel.id ∥ₖ η' ∘ₖ (η ∘ₖ κ ∥ₖ κ')
rw₁ : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = Kernel.id ∥ₖ η' ∘ₖ (η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ κ'))
rw₂ : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = Kernel.id ∥ₖ η' ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ (κ ∥ₖ κ')
rw₃ : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∥ₖ (η' ∘ₖ Kernel.id) ∘ₖ (κ ∥ₖ κ')
rw₄ rw₅ : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∥ₖ η' ∘ₖ (κ ∥ₖ κ')
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∘ₖ κ ∥ₖ (η' ∘ₖ κ')

Tactic:
rw [← parallelComp_id_left_comp_parallelComp, ← parallelComp_id_right_comp_parallelComp,
    ← comp_assoc, parallelComp_id_left_comp_parallelComp, comp_id]

Premises used: ProbabilityTheory.Kernel.comp_assoc, ProbabilityTheory.Kernel.parallelComp_id_right_comp_parallelComp, ProbabilityTheory.Kernel.comp_id, ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp
-- 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
Y' : Type u_6
Z' : Type u_7
mY' : MeasurableSpace Y'
mZ' : MeasurableSpace Z'
inst : IsSFiniteKernel κ
η : Kernel Y Z
inst_1 : IsSFiniteKernel η
κ' : Kernel X Y'
inst_2 : IsSFiniteKernel κ'
η' : Kernel Y' Z'
inst_3 : IsSFiniteKernel η'
rw : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ' ∘ₖ copy X) = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
rw₁ : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') ∘ₖ copy X = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
rw₂ : η ∘ₖ κ ∥ₖ (η' ∘ₖ κ') ∘ₖ copy X = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
rw₃ rw₄ : η ∘ₖ κ ∥ₖ (η' ∘ₖ κ') ∘ₖ copy X = η ∘ₖ κ ∥ₖ (η' ∘ₖ κ') ∘ₖ copy X
⊢ η ∥ₖ η' ∘ₖ (κ ×ₖ κ') = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')

Tactic:
rw [← parallelComp_comp_copy, ← comp_assoc, parallelComp_comp_parallelComp,
    ← parallelComp_comp_copy]

Premises used: ProbabilityTheory.Kernel.parallelComp_comp_parallelComp, ProbabilityTheory.Kernel.comp_assoc, ProbabilityTheory.Kernel.parallelComp_comp_copy
-- 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 κ), Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
neg : ∀ (hκ : ¬IsSFiniteKernel κ), Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ 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
η : Kernel Z T
hκ : ¬IsSFiniteKernel κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (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
η : Kernel Z T
hκ : IsSFiniteKernel κ
pos : ∀ (hη : IsSFiniteKernel η), Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
neg : ∀ (hη : ¬IsSFiniteKernel η), Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ 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
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (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
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
pos : η ∥ₖ (κ ∘ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
pos₁ : η ∥ₖ (κ ∘ₖ Kernel.id) = η ∘ₖ Kernel.id ∥ₖ κ
pos₂ : η ∥ₖ κ = η ∘ₖ Kernel.id ∥ₖ κ
pos₃ pos₄ : η ∥ₖ κ = η ∥ₖ κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)

Tactic:
rw [parallelComp_id_left_comp_parallelComp, parallelComp_id_right_comp_parallelComp,
    comp_id, comp_id]

Premises used: ProbabilityTheory.Kernel.parallelComp_id_right_comp_parallelComp, ProbabilityTheory.Kernel.comp_id, ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp
-- 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
inst : IsSFiniteKernel κ
rw : η ∥ₖ (κ ∘ₖ Kernel.id) = η ∥ₖ κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ κ

Tactic:
rw [parallelComp_id_left_comp_parallelComp]

Premises used: ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp
-- 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
inst : IsSFiniteKernel κ
e_η : κ ∘ₖ Kernel.id = κ
⊢ η ∥ₖ (κ ∘ₖ Kernel.id) = η ∥ₖ κ

Tactic:
congr
-- 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
inst : IsSFiniteKernel κ
⊢ κ ∘ₖ Kernel.id = κ

Tactic:
comp_id κ

Premises used: ProbabilityTheory.Kernel.comp_id
-- 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
inst : IsSFiniteKernel κ
⊢ κ ∘ₖ Kernel.id = κ

Tactic:
exact comp_id κ

Premises used: ProbabilityTheory.Kernel.comp_id
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
h :
  ∀ (ω : γ) (s : Set (δ × β')) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
            (a : Set (δ × β')) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
              Measure (δ × β')) :
            (a : Set (δ × β')) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf) = ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf)

Tactic:
ext ω s hs
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
        s ∂(κ : (a : γ) → Measure β) ω =
    ∫⁻ (b : β),
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) ∂(κ : (a : γ) → Measure β) ω
h₁ :
  Measurable (β := ℝ≥0∞) fun (b : β × ε) ↦
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) b
h₂ :
  Measurable (β := ℝ≥0∞) fun (b : δ) ↦
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞) (Prod.mk b ⁻¹' s)
h₃ :
  Measurable (β := ℝ≥0∞) fun (b : β × ε) ↦
    (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) b : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    ((((ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
            Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_prod_deterministic,
    lintegral_comp, lintegral_prod_deterministic]

Premises used: ProbabilityTheory.Kernel.prod_apply', ProbabilityTheory.Kernel.lintegral_prod_deterministic, ProbabilityTheory.Kernel.lintegral_comp, ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
h :
  ∀ (b : β),
    (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
        s =
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
⊢ ∫⁻ (b : β),
      (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
        s ∂(κ : (a : γ) → Measure β) ω =
    ∫⁻ (b : β),
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) ∂(κ : (a : γ) → Measure β) ω

Tactic:
congr with b
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
h :
  ∫⁻ (b_1 : δ),
      (((prodMkLeft β η : (a : β × ε) → Measure β') (b, f ω) : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
h₁ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (b, f ω).2 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
h₂ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (b, f ω).2 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
    ∫⁻ (c : δ),
      (((η.comap f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
h₃ h₄ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (b, f ω).2 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω) =
    ∫⁻ (c : δ),
      (((η : (a : ε) → Measure β') (f ω) : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)
⊢ (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) (b, f ω) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) (b, f ω)

Tactic:
rw [prod_apply' _ _ _ hs, prodMkLeft_apply, comp_deterministic_eq_comap, comap_apply]

Premises used: ProbabilityTheory.Kernel.prod_apply', ProbabilityTheory.Kernel.prodMkLeft_apply, ProbabilityTheory.Kernel.comap_apply, ProbabilityTheory.Kernel.comp_deterministic_eq_comap
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : β × ε) ↦
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) b

Tactic:
(measurable_measure_prodMk_left hs).lintegral_kernel

Premises used: Measurable.lintegral_kernel, measurable_measure_prodMk_left