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
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)
⊢ 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₂ : 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∞)
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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ))
have simp_rw : ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = swap Y T ∘ₖ swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)
Tactic: simp_rw [← comp_assoc, swap_swap, id_comp]
-- 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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
simp_rw : ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = swap Y T ∘ₖ swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ))
have simp_rw₁ : ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = Kernel.id ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)
Tactic: simp_rw [← comp_assoc, swap_swap, id_comp]
-- 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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ))
have rw : swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ))
Tactic: rw [this]
-- 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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)) = ξ ∘ₖ η ∥ₖ κ
have simp_rw : swap Y T ∘ₖ swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ
Tactic: simp_rw [← comp_assoc, swap_swap, id_comp]
-- 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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
simp_rw : swap Y T ∘ₖ swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ
⊢ swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)) = ξ ∘ₖ η ∥ₖ κ
have simp_rw₁ : Kernel.id ∘ₖ (ξ ∘ₖ η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ
Tactic: simp_rw [← comp_assoc, swap_swap, id_comp]
-- 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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ
have calc : ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = 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]
-- 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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
calc : ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ))
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ
have calc₁ : swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ))
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]
-- 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 ξ
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 ∘ₖ (ξ ∘ₖ η ∥ₖ κ))
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ
have calc₂ : swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)) = ξ ∘ₖ η ∥ₖ κ
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]
-- 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 suffices : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
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]
-- 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 ξ
⊢ swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
have simp_rw : Kernel.id ∥ₖ ξ ∘ₖ swap Z Y ∘ₖ (η ∥ₖ κ) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
Tactic: simp_rw [swap_parallelComp, comp_assoc, swap_parallelComp, ← comp_assoc,
    parallelComp_id_left_comp_parallelComp]
-- 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 ξ
simp_rw : Kernel.id ∥ₖ ξ ∘ₖ swap Z Y ∘ₖ (η ∥ₖ κ) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
⊢ swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
have simp_rw₁ : Kernel.id ∥ₖ ξ ∘ₖ (swap Z Y ∘ₖ (η ∥ₖ κ)) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
Tactic: simp_rw [swap_parallelComp, comp_assoc, swap_parallelComp, ← comp_assoc,
    parallelComp_id_left_comp_parallelComp]
-- 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 ξ
simp_rw : Kernel.id ∥ₖ ξ ∘ₖ swap Z Y ∘ₖ (η ∥ₖ κ) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
simp_rw₁ : Kernel.id ∥ₖ ξ ∘ₖ (swap Z Y ∘ₖ (η ∥ₖ κ)) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
⊢ swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
have simp_rw₂ : Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η ∘ₖ swap X' X) = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
Tactic: simp_rw [swap_parallelComp, comp_assoc, swap_parallelComp, ← comp_assoc,
    parallelComp_id_left_comp_parallelComp]
-- 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 ξ
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
⊢ swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
have simp_rw₃ : Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) ∘ₖ swap X' X = κ ∥ₖ (ξ ∘ₖ η) ∘ₖ swap X' X
Tactic: simp_rw [swap_parallelComp, comp_assoc, swap_parallelComp, ← comp_assoc,
    parallelComp_id_left_comp_parallelComp]
-- 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
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 η'
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∘ₖ κ ∥ₖ (η' ∘ₖ κ')
have rw : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = Kernel.id ∥ₖ η' ∘ₖ (η ∘ₖ κ ∥ₖ κ')
Tactic: rw [← parallelComp_id_left_comp_parallelComp, ← parallelComp_id_right_comp_parallelComp,
    ← comp_assoc, parallelComp_id_left_comp_parallelComp, comp_id]
-- 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
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 ∥ₖ η' ∘ₖ (η ∘ₖ κ ∥ₖ κ')
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∘ₖ κ ∥ₖ (η' ∘ₖ κ')
have rw₁ : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = Kernel.id ∥ₖ η' ∘ₖ (η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ κ'))
Tactic: rw [← parallelComp_id_left_comp_parallelComp, ← parallelComp_id_right_comp_parallelComp,
    ← comp_assoc, parallelComp_id_left_comp_parallelComp, comp_id]
-- 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
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 ∘ₖ (κ ∥ₖ κ'))
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∘ₖ κ ∥ₖ (η' ∘ₖ κ')
have rw₂ : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = Kernel.id ∥ₖ η' ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ (κ ∥ₖ κ')
Tactic: rw [← parallelComp_id_left_comp_parallelComp, ← parallelComp_id_right_comp_parallelComp,
    ← comp_assoc, parallelComp_id_left_comp_parallelComp, comp_id]
-- 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
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) ∘ₖ (κ ∥ₖ κ')
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∘ₖ κ ∥ₖ (η' ∘ₖ κ')
have rw₃ : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∥ₖ (η' ∘ₖ Kernel.id) ∘ₖ (κ ∥ₖ κ')
Tactic: rw [← parallelComp_id_left_comp_parallelComp, ← parallelComp_id_right_comp_parallelComp,
    ← comp_assoc, parallelComp_id_left_comp_parallelComp, comp_id]
-- 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
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) ∘ₖ (κ ∥ₖ κ')
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∘ₖ κ ∥ₖ (η' ∘ₖ κ')
have rw₄ : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∥ₖ η' ∘ₖ (κ ∥ₖ κ')
Tactic: rw [← parallelComp_id_left_comp_parallelComp, ← parallelComp_id_right_comp_parallelComp,
    ← comp_assoc, parallelComp_id_left_comp_parallelComp, comp_id]
-- 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
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 η'
⊢ η ∥ₖ η' ∘ₖ (κ ×ₖ κ') = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
have rw : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ' ∘ₖ copy X) = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
Tactic: rw [← parallelComp_comp_copy, ← comp_assoc, parallelComp_comp_parallelComp,
    ← parallelComp_comp_copy]
-- 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
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) = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
⊢ η ∥ₖ η' ∘ₖ (κ ×ₖ κ') = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
have rw₁ : η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') ∘ₖ copy X = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
Tactic: rw [← parallelComp_comp_copy, ← comp_assoc, parallelComp_comp_parallelComp,
    ← parallelComp_comp_copy]
-- 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
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 = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
⊢ η ∥ₖ η' ∘ₖ (κ ×ₖ κ') = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
have rw₂ : η ∘ₖ κ ∥ₖ (η' ∘ₖ κ') ∘ₖ copy X = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
Tactic: rw [← parallelComp_comp_copy, ← comp_assoc, parallelComp_comp_parallelComp,
    ← parallelComp_comp_copy]
-- 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
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 = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
⊢ η ∥ₖ η' ∘ₖ (κ ×ₖ κ') = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')
have rw₃ : η ∘ₖ κ ∥ₖ (η' ∘ₖ κ') ∘ₖ copy X = η ∘ₖ κ ∥ₖ (η' ∘ₖ κ') ∘ₖ copy X
Tactic: rw [← parallelComp_comp_copy, ← comp_assoc, parallelComp_comp_parallelComp,
    ← parallelComp_comp_copy]
-- 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
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
have pos : ∀ (hκ : IsSFiniteKernel κ), Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (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
η : Kernel Z T
pos : ∀ (hκ : IsSFiniteKernel κ), Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
have neg : ∀ (hκ : ¬IsSFiniteKernel κ), Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (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
η : Kernel Z T
hκ : IsSFiniteKernel κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
have pos : ∀ (hη : IsSFiniteKernel η), Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (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
η : Kernel Z T
hκ : IsSFiniteKernel κ
pos : ∀ (hη : IsSFiniteKernel η), Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
have neg : ∀ (hη : ¬IsSFiniteKernel η), Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (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
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
have pos : η ∥ₖ (κ ∘ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
Tactic: rw [parallelComp_id_left_comp_parallelComp, parallelComp_id_right_comp_parallelComp,
    comp_id, comp_id]
-- 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 η
pos : η ∥ₖ (κ ∘ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
have pos₁ : η ∥ₖ (κ ∘ₖ Kernel.id) = η ∘ₖ Kernel.id ∥ₖ κ
Tactic: rw [parallelComp_id_left_comp_parallelComp, parallelComp_id_right_comp_parallelComp,
    comp_id, comp_id]
-- 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 η
pos : η ∥ₖ (κ ∘ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
pos₁ : η ∥ₖ (κ ∘ₖ Kernel.id) = η ∘ₖ Kernel.id ∥ₖ κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
have pos₂ : η ∥ₖ κ = η ∘ₖ Kernel.id ∥ₖ κ
Tactic: rw [parallelComp_id_left_comp_parallelComp, parallelComp_id_right_comp_parallelComp,
    comp_id, comp_id]
-- 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 η
pos : η ∥ₖ (κ ∘ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
pos₁ : η ∥ₖ (κ ∘ₖ Kernel.id) = η ∘ₖ Kernel.id ∥ₖ κ
pos₂ : η ∥ₖ κ = η ∘ₖ Kernel.id ∥ₖ κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
have pos₃ : η ∥ₖ κ = η ∥ₖ κ
Tactic: rw [parallelComp_id_left_comp_parallelComp, parallelComp_id_right_comp_parallelComp,
    comp_id, comp_id]