awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
        ((⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × Z.carrier) × X.carrier) → Y.carrier × Z.carrier × X.carrier) ∘
          Prod.swap)
        ⋯ ∘ₖ
      Kernel.deterministic
        (⇑MeasurableEquiv.prodAssoc : (a : (X.carrier × Y.carrier) × Z.carrier) → X.carrier × Y.carrier × Z.carrier) ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × X.carrier) × Z.carrier) → Y.carrier × X.carrier × Z.carrier)
          ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
have h : Kernel.deterministic
    (Function.comp (β := X.carrier × Y.carrier × Z.carrier)
      ((⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × Z.carrier) × X.carrier) → Y.carrier × Z.carrier × X.carrier) ∘
        Prod.swap)
      (⇑MeasurableEquiv.prodAssoc : (a : (X.carrier × Y.carrier) × Z.carrier) → X.carrier × Y.carrier × Z.carrier))
    sorry =
  Kernel.deterministic (Prod.map id Prod.swap) sorry ∘ₖ
      Kernel.deterministic
        (⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × X.carrier) × Z.carrier) → Y.carrier × X.carrier × Z.carrier)
        sorry ∘ₖ
    Kernel.deterministic (Prod.map Prod.swap id) sorry
Tactic: rw [Kernel.deterministic_comp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
      (Function.comp (β := X.carrier × Y.carrier × Z.carrier)
        ((⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × Z.carrier) × X.carrier) → Y.carrier × Z.carrier × X.carrier) ∘
          Prod.swap)
        (⇑MeasurableEquiv.prodAssoc : (a : (X.carrier × Y.carrier) × Z.carrier) → X.carrier × Y.carrier × Z.carrier))
      ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × X.carrier) × Z.carrier) → Y.carrier × X.carrier × Z.carrier)
          ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
have h : Kernel.deterministic
    (Function.comp (β := X.carrier × Y.carrier × Z.carrier)
      ((⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × Z.carrier) × X.carrier) → Y.carrier × Z.carrier × X.carrier) ∘
        Prod.swap)
      (⇑MeasurableEquiv.prodAssoc : (a : (X.carrier × Y.carrier) × Z.carrier) → X.carrier × Y.carrier × Z.carrier))
    sorry =
  Kernel.deterministic
      (Prod.map id Prod.swap ∘
        (⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × X.carrier) × Z.carrier) → Y.carrier × X.carrier × Z.carrier))
      sorry ∘ₖ
    Kernel.deterministic (Prod.map Prod.swap id) sorry
Tactic: rw [Kernel.deterministic_comp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
      (Function.comp (β := X.carrier × Y.carrier × Z.carrier)
        ((⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × Z.carrier) × X.carrier) → Y.carrier × Z.carrier × X.carrier) ∘
          Prod.swap)
        (⇑MeasurableEquiv.prodAssoc : (a : (X.carrier × Y.carrier) × Z.carrier) → X.carrier × Y.carrier × Z.carrier))
      ⋯ =
    Kernel.deterministic
        (Prod.map id Prod.swap ∘
          (⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × X.carrier) × Z.carrier) → Y.carrier × X.carrier × Z.carrier))
        ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
have h : Kernel.deterministic
    (Function.comp (β := X.carrier × Y.carrier × Z.carrier)
      ((⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × Z.carrier) × X.carrier) → Y.carrier × Z.carrier × X.carrier) ∘
        Prod.swap)
      (⇑MeasurableEquiv.prodAssoc : (a : (X.carrier × Y.carrier) × Z.carrier) → X.carrier × Y.carrier × Z.carrier))
    sorry =
  Kernel.deterministic
    ((Prod.map id Prod.swap ∘
        (⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × X.carrier) × Z.carrier) → Y.carrier × X.carrier × Z.carrier)) ∘
      Prod.map Prod.swap id)
    sorry
Tactic: rw [Kernel.deterministic_comp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × Z.carrier) × X.carrier) → Y.carrier × Z.carrier × X.carrier)
          ⋯ ∘ₖ
        Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic
        (⇑MeasurableEquiv.prodAssoc : (a : (X.carrier × Y.carrier) × Z.carrier) → X.carrier × Y.carrier × Z.carrier) ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × X.carrier) × Z.carrier) → Y.carrier × X.carrier × Z.carrier)
          ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
have h : Kernel.deterministic
    (Function.comp (β := X.carrier × Y.carrier × Z.carrier)
      ((⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × Z.carrier) × X.carrier) → Y.carrier × Z.carrier × X.carrier) ∘
        Prod.swap)
      (⇑MeasurableEquiv.prodAssoc : (a : (X.carrier × Y.carrier) × Z.carrier) → X.carrier × Y.carrier × Z.carrier))
    sorry =
  Kernel.deterministic
    ((Prod.map id Prod.swap ∘
        (⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × X.carrier) × Z.carrier) → Y.carrier × X.carrier × Z.carrier)) ∘
      Prod.map Prod.swap id)
    sorry
Tactic: repeat rw [Kernel.deterministic_comp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier)
          ⋯ ∘ₖ
        Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier)
        ⋯ =
    Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯ ∘ₖ
        Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Prod.swap ⋯)
have h : Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier)
        sorry ∘ₖ
      Kernel.deterministic Prod.swap sorry ∘ₖ
    Kernel.deterministic
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
        (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier)
      sorry =
  Kernel.deterministic (Prod.map Prod.swap id) sorry ∘ₖ
      Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
        sorry ∘ₖ
    (Kernel.deterministic id sorry ∥ₖ Kernel.deterministic Prod.swap sorry)
Tactic: rw [Kernel.deterministic_parallelComp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier)
          ⋯ ∘ₖ
        Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier)
        ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ
        Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Prod.swap ⋯)
have h : Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier)
        sorry ∘ₖ
      Kernel.deterministic Prod.swap sorry ∘ₖ
    Kernel.deterministic
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
        (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier)
      sorry =
  Kernel.deterministic (Prod.map Prod.swap id) sorry ∘ₖ
      Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
        sorry ∘ₖ
    Kernel.deterministic (Prod.map id Prod.swap) sorry
Tactic: rw [Kernel.deterministic_parallelComp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier)
          ⋯ ∘ₖ
        Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier)
        ⋯ =
    Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯ ∘ₖ
        Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Prod.swap ⋯)
have h : Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier)
        sorry ∘ₖ
      Kernel.deterministic Prod.swap sorry ∘ₖ
    Kernel.deterministic
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
        (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier)
      sorry =
  Kernel.deterministic (Prod.map Prod.swap id) sorry ∘ₖ
      Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
        sorry ∘ₖ
    Kernel.deterministic (Prod.map id Prod.swap) sorry
Tactic: repeat rw [Kernel.deterministic_parallelComp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier)
          ⋯ ∘ₖ
        Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier)
        ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ
        Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
          ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
have h : Kernel.deterministic
      ((⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier) ∘
        Prod.swap)
      sorry ∘ₖ
    Kernel.deterministic
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
        (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier)
      sorry =
  Kernel.deterministic (Prod.map Prod.swap id) sorry ∘ₖ
      Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
        sorry ∘ₖ
    Kernel.deterministic (Prod.map id Prod.swap) sorry
Tactic: rw [Kernel.deterministic_comp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
        ((⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier) ∘
          Prod.swap)
        ⋯ ∘ₖ
      Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier)
        ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ
        Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
          ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
have h : Kernel.deterministic
    (Function.comp (β := (X.carrier × Y.carrier) × Z.carrier)
      ((⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier) ∘
        Prod.swap)
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
        (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier))
    sorry =
  Kernel.deterministic (Prod.map Prod.swap id) sorry ∘ₖ
      Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
        sorry ∘ₖ
    Kernel.deterministic (Prod.map id Prod.swap) sorry
Tactic: rw [Kernel.deterministic_comp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
      (Function.comp (β := (X.carrier × Y.carrier) × Z.carrier)
        ((⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier) ∘
          Prod.swap)
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier))
      ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ
        Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
          ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
have h : Kernel.deterministic
    (Function.comp (β := (X.carrier × Y.carrier) × Z.carrier)
      ((⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier) ∘
        Prod.swap)
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
        (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier))
    sorry =
  Kernel.deterministic
      (Prod.map Prod.swap id ∘
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier))
      sorry ∘ₖ
    Kernel.deterministic (Prod.map id Prod.swap) sorry
Tactic: rw [Kernel.deterministic_comp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
      (Function.comp (β := (X.carrier × Y.carrier) × Z.carrier)
        ((⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier) ∘
          Prod.swap)
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier))
      ⋯ =
    Kernel.deterministic
        (Prod.map Prod.swap id ∘
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier))
        ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
have h : Kernel.deterministic
    (Function.comp (β := (X.carrier × Y.carrier) × Z.carrier)
      ((⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier) ∘
        Prod.swap)
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
        (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier))
    sorry =
  Kernel.deterministic
    ((Prod.map Prod.swap id ∘
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)) ∘
      Prod.map id Prod.swap)
    sorry
Tactic: rw [Kernel.deterministic_comp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier)
          ⋯ ∘ₖ
        Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier)
        ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ
        Kernel.deterministic
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
            (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)
          ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
have h : Kernel.deterministic
    (Function.comp (β := (X.carrier × Y.carrier) × Z.carrier)
      ((⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : Z.carrier × X.carrier × Y.carrier) → (Z.carrier × X.carrier) × Y.carrier) ∘
        Prod.swap)
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
        (a : X.carrier × Y.carrier × Z.carrier) → (X.carrier × Y.carrier) × Z.carrier))
    sorry =
  Kernel.deterministic
    ((Prod.map Prod.swap id ∘
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
          (a : X.carrier × Z.carrier × Y.carrier) → (X.carrier × Z.carrier) × Y.carrier)) ∘
      Prod.map id Prod.swap)
    sorry
Tactic: repeat rw [Kernel.deterministic_comp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X)
      (Iso.hom
        { hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
          inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ })
      (Iso.hom
        { hom := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ },
          inv := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }) =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y)
have h : Hom.hom
    (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X)
      (Iso.hom
        { hom := { hom := Kernel.swap X.carrier Y.carrier, property := sorry },
          inv := { hom := Kernel.swap Y.carrier X.carrier, property := sorry }, hom_inv_id := sorry, inv_hom_id := sorry })
      (Iso.hom
        { hom := { hom := Kernel.swap Y.carrier X.carrier, property := sorry },
          inv := { hom := Kernel.swap X.carrier Y.carrier, property := sorry }, hom_inv_id := sorry, inv_hom_id := sorry })) =
  Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X : SFinKer
⊢ Eq (α := X ⟶ MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) ((𝟙_ SFinKer) (𝒞 := instLargeCategory)) X)
    (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X)
      { hom := Kernel.copy X.carrier, property := ⋯ } ({ hom := Kernel.discard X.carrier, property := ⋯ } ▷ X))
    (Iso.inv (λ_ X))
have h : Eq (α :=
  Kernel X.carrier
    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) ((𝟙_ SFinKer) (𝒞 := instLargeCategory)) X).carrier)
  (Hom.hom
    (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X)
      { hom := Kernel.copy X.carrier, property := sorry } ({ hom := Kernel.discard X.carrier, property := sorry } ▷ X)))
  (Hom.hom (Iso.inv (λ_ X)))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X : SFinKer
⊢ Eq (α :=
    Kernel X.carrier
      (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) ((𝟙_ SFinKer) (𝒞 := instLargeCategory)) X).carrier)
    (Hom.hom
      (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X)
        { hom := Kernel.copy X.carrier, property := ⋯ } ({ hom := Kernel.discard X.carrier, property := ⋯ } ▷ X)))
    (Hom.hom (Iso.inv (λ_ X)))
have h : Eq.{u_1 + 1} (α := Kernel X.carrier (PUnit.{u_1 + 1} × X.carrier))
  (Kernel.discard X.carrier ∥ₖ Kernel.id ∘ₖ Kernel.copy X.carrier)
  (Kernel.map Kernel.id fun (x : X.carrier) ↦ (PUnit.unit, x))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X : SFinKer
⊢ Eq.{u_1 + 1} (α := Kernel X.carrier (PUnit.{u_1 + 1} × X.carrier))
    (Kernel.deterministic (fun (x : X.carrier) ↦ PUnit.unit) ⋯ ∥ₖ Kernel.deterministic id ⋯ ∘ₖ
      Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) ⋯)
    (Kernel.map (Kernel.deterministic id ⋯) fun (x : X.carrier) ↦ (PUnit.unit, x))
have h : Eq.{u_1 + 1} (α := Kernel X.carrier (PUnit.{u_1 + 1} × X.carrier))
  (Kernel.deterministic
    (Function.comp (β := X.carrier × X.carrier) (Prod.map (fun (x : X.carrier) ↦ PUnit.unit) id) fun (x : X.carrier) ↦
      (x, x))
    sorry)
  (Kernel.deterministic ((fun (x : X.carrier) ↦ (PUnit.unit, x)) ∘ id) sorry)
Tactic: rw [Kernel.deterministic_parallelComp_deterministic,
      Kernel.deterministic_comp_deterministic, Kernel.deterministic_map measurable_id (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X : SFinKer
⊢ Eq (α := X ⟶ MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X ((𝟙_ SFinKer) (𝒞 := instLargeCategory)))
    (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X)
      { hom := Kernel.copy X.carrier, property := ⋯ } (X ◁ { hom := Kernel.discard X.carrier, property := ⋯ }))
    (Iso.inv (ρ_ X))
have h : Eq (α :=
  Kernel X.carrier
    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X ((𝟙_ SFinKer) (𝒞 := instLargeCategory))).carrier)
  (Hom.hom
    (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X)
      { hom := Kernel.copy X.carrier, property := sorry } (X ◁ { hom := Kernel.discard X.carrier, property := sorry })))
  (Hom.hom (Iso.inv (ρ_ X)))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X : SFinKer
⊢ Eq (α :=
    Kernel X.carrier
      (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X ((𝟙_ SFinKer) (𝒞 := instLargeCategory))).carrier)
    (Hom.hom
      (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X)
        { hom := Kernel.copy X.carrier, property := ⋯ } (X ◁ { hom := Kernel.discard X.carrier, property := ⋯ })))
    (Hom.hom (Iso.inv (ρ_ X)))
have h : Eq.{u_1 + 1} (α := Kernel X.carrier (X.carrier × PUnit.{u_1 + 1}))
  (Kernel.id ∥ₖ Kernel.discard X.carrier ∘ₖ Kernel.copy X.carrier)
  (Kernel.map Kernel.id fun (x : X.carrier) ↦ (x, PUnit.unit))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X : SFinKer
⊢ Eq.{u_1 + 1} (α := Kernel X.carrier (X.carrier × PUnit.{u_1 + 1}))
    (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (fun (x : X.carrier) ↦ PUnit.unit) ⋯ ∘ₖ
      Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) ⋯)
    (Kernel.map (Kernel.deterministic id ⋯) fun (x : X.carrier) ↦ (x, PUnit.unit))
have h : Eq.{u_1 + 1} (α := Kernel X.carrier (X.carrier × PUnit.{u_1 + 1}))
  (Kernel.deterministic
    (Function.comp (β := X.carrier × X.carrier) (Prod.map id fun (x : X.carrier) ↦ PUnit.unit) fun (x : X.carrier) ↦
      (x, x))
    sorry)
  (Kernel.deterministic ((fun (x : X.carrier) ↦ (x, PUnit.unit)) ∘ id) sorry)
Tactic: rw [Kernel.deterministic_parallelComp_deterministic,
      Kernel.deterministic_comp_deterministic, Kernel.deterministic_map measurable_id (by fun_prop)]