awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X : SFinKer
⊢ Eq (α :=
    X ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X
        (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X))
    (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X)
      { hom := Kernel.copy X.carrier, property := ⋯ } (X ◁ { hom := Kernel.copy X.carrier, property := ⋯ }))
    (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X)
      { hom := Kernel.copy X.carrier, property := ⋯ }
      ({ hom := Kernel.copy X.carrier, property := ⋯ } ▷ X ≫ Iso.hom (α_ X X X)))
have h : Eq (α :=
  Kernel X.carrier
    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X
        (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X)).carrier)
  (Hom.hom
    (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X)
      { hom := Kernel.copy X.carrier, property := sorry } (X ◁ { hom := Kernel.copy X.carrier, property := sorry })))
  (Hom.hom
    (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X)
      { hom := Kernel.copy X.carrier, property := sorry }
      ({ hom := Kernel.copy X.carrier, property := sorry } ▷ X ≫ Iso.hom (α_ X X X))))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X : SFinKer
⊢ Kernel.id ∥ₖ Kernel.copy X.carrier ∘ₖ Kernel.copy X.carrier =
    Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc : (a : (X.carrier × X.carrier) × X.carrier) → X.carrier × X.carrier × X.carrier)
          ⋯ ∘ₖ
        (Kernel.copy X.carrier ∥ₖ Kernel.id) ∘ₖ
      Kernel.copy X.carrier
have h : Kernel.deterministic
    (Function.comp (β := X.carrier × X.carrier) (Prod.map id fun (x : X.carrier) ↦ (x, x)) fun (x : X.carrier) ↦ (x, x))
    sorry =
  Kernel.deterministic
    (Function.comp (β := X.carrier × X.carrier)
      (Function.comp (β := (X.carrier × X.carrier) × X.carrier)
        (⇑MeasurableEquiv.prodAssoc : (a : (X.carrier × X.carrier) × X.carrier) → X.carrier × X.carrier × X.carrier)
        (Prod.map (fun (x : X.carrier) ↦ (x, x)) id))
      fun (x : X.carrier) ↦ (x, x))
    sorry
Tactic: simp [Kernel.copy, Kernel.id, Kernel.deterministic_comp_deterministic,
      Kernel.deterministic_parallelComp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X : SFinKer
⊢ Δ ≫ Iso.hom (β_ X X) = Δ
have h : (Δ ≫ Iso.hom (β_ X X)).hom = Hom.hom Δ
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Δ = (Δ ⊗ₘ Δ) ≫ MonoidalCategory.tensorμ X X Y Y
have h : Hom.hom Δ = ((Δ ⊗ₘ Δ) ≫ MonoidalCategory.tensorμ X X Y Y).hom
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
                (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                  (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
                ⋯ ∘ₖ
              (Kernel.deterministic id ⋯ ∥ₖ
                Kernel.deterministic
                  (⇑MeasurableEquiv.prodAssoc :
                    (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier)
                  ⋯) ∘ₖ
            (Kernel.deterministic id ⋯ ∥ₖ (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)) ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ
            Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier)
              ⋯) ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc :
            (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (fun (x : Y.carrier) ↦ (x, x)) ⋯ ∘ₖ
        (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) ⋯ ∥ₖ Kernel.deterministic id ⋯))
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
              sorry ∘ₖ
            Kernel.deterministic
              (Prod.map id
                (⇑MeasurableEquiv.prodAssoc :
                  (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
              sorry ∘ₖ
          (Kernel.deterministic id sorry ∥ₖ (Kernel.deterministic Prod.swap sorry ∥ₖ Kernel.deterministic id sorry)) ∘ₖ
        (Kernel.deterministic id sorry ∥ₖ
          Kernel.deterministic
            (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
              (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier)
            sorry) ∘ₖ
      Kernel.deterministic
        (⇑MeasurableEquiv.prodAssoc :
          (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
        sorry ∘ₖ
    (Kernel.deterministic id sorry ∥ₖ Kernel.deterministic (fun (x : Y.carrier) ↦ (x, x)) sorry ∘ₖ
      (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) sorry ∥ₖ Kernel.deterministic id sorry))
Tactic: rw [Kernel.deterministic_parallelComp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
                (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                  (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
                ⋯ ∘ₖ
              Kernel.deterministic
                (Prod.map id
                  (⇑MeasurableEquiv.prodAssoc :
                    (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
                ⋯ ∘ₖ
            (Kernel.deterministic id ⋯ ∥ₖ (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)) ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ
            Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier)
              ⋯) ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc :
            (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (fun (x : Y.carrier) ↦ (x, x)) ⋯ ∘ₖ
        (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) ⋯ ∥ₖ Kernel.deterministic id ⋯))
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
              sorry ∘ₖ
            Kernel.deterministic
              (Prod.map id
                (⇑MeasurableEquiv.prodAssoc :
                  (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
              sorry ∘ₖ
          (Kernel.deterministic id sorry ∥ₖ Kernel.deterministic (Prod.map Prod.swap id) sorry) ∘ₖ
        (Kernel.deterministic id sorry ∥ₖ
          Kernel.deterministic
            (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
              (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier)
            sorry) ∘ₖ
      Kernel.deterministic
        (⇑MeasurableEquiv.prodAssoc :
          (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
        sorry ∘ₖ
    (Kernel.deterministic id sorry ∥ₖ Kernel.deterministic (fun (x : Y.carrier) ↦ (x, x)) sorry ∘ₖ
      (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) sorry ∥ₖ Kernel.deterministic id sorry))
Tactic: rw [Kernel.deterministic_parallelComp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
                (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                  (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
                ⋯ ∘ₖ
              Kernel.deterministic
                (Prod.map id
                  (⇑MeasurableEquiv.prodAssoc :
                    (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
                ⋯ ∘ₖ
            (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (Prod.map Prod.swap id) ⋯) ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ
            Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier)
              ⋯) ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc :
            (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (fun (x : Y.carrier) ↦ (x, x)) ⋯ ∘ₖ
        (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) ⋯ ∥ₖ Kernel.deterministic id ⋯))
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
              sorry ∘ₖ
            Kernel.deterministic
              (Prod.map id
                (⇑MeasurableEquiv.prodAssoc :
                  (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
              sorry ∘ₖ
          Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) sorry ∘ₖ
        (Kernel.deterministic id sorry ∥ₖ
          Kernel.deterministic
            (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
              (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier)
            sorry) ∘ₖ
      Kernel.deterministic
        (⇑MeasurableEquiv.prodAssoc :
          (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
        sorry ∘ₖ
    (Kernel.deterministic id sorry ∥ₖ Kernel.deterministic (fun (x : Y.carrier) ↦ (x, x)) sorry ∘ₖ
      (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) sorry ∥ₖ Kernel.deterministic id sorry))
Tactic: rw [Kernel.deterministic_parallelComp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
                (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                  (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
                ⋯ ∘ₖ
              Kernel.deterministic
                (Prod.map id
                  (⇑MeasurableEquiv.prodAssoc :
                    (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
                ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ
            Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier)
              ⋯) ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc :
            (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (fun (x : Y.carrier) ↦ (x, x)) ⋯ ∘ₖ
        (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) ⋯ ∥ₖ Kernel.deterministic id ⋯))
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
              sorry ∘ₖ
            Kernel.deterministic
              (Prod.map id
                (⇑MeasurableEquiv.prodAssoc :
                  (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
              sorry ∘ₖ
          Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) sorry ∘ₖ
        Kernel.deterministic
          (Prod.map id
            (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
              (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier))
          sorry ∘ₖ
      Kernel.deterministic
        (⇑MeasurableEquiv.prodAssoc :
          (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
        sorry ∘ₖ
    (Kernel.deterministic id sorry ∥ₖ Kernel.deterministic (fun (x : Y.carrier) ↦ (x, x)) sorry ∘ₖ
      (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) sorry ∥ₖ Kernel.deterministic id sorry))
Tactic: rw [Kernel.deterministic_parallelComp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
                (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                  (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
                ⋯ ∘ₖ
              Kernel.deterministic
                (Prod.map id
                  (⇑MeasurableEquiv.prodAssoc :
                    (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
                ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic
            (Prod.map id
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier))
            ⋯ ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc :
            (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (fun (x : Y.carrier) ↦ (x, x)) ⋯ ∘ₖ
        (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) ⋯ ∥ₖ Kernel.deterministic id ⋯))
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
              sorry ∘ₖ
            Kernel.deterministic
              (Prod.map id
                (⇑MeasurableEquiv.prodAssoc :
                  (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
              sorry ∘ₖ
          Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) sorry ∘ₖ
        Kernel.deterministic
          (Prod.map id
            (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
              (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier))
          sorry ∘ₖ
      Kernel.deterministic
        (⇑MeasurableEquiv.prodAssoc :
          (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
        sorry ∘ₖ
    (Kernel.deterministic (Prod.map id fun (x : Y.carrier) ↦ (x, x)) sorry ∘ₖ
      (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) sorry ∥ₖ Kernel.deterministic id sorry))
Tactic: rw [Kernel.deterministic_parallelComp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
                (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                  (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
                ⋯ ∘ₖ
              Kernel.deterministic
                (Prod.map id
                  (⇑MeasurableEquiv.prodAssoc :
                    (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
                ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic
            (Prod.map id
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier))
            ⋯ ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc :
            (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id fun (x : Y.carrier) ↦ (x, x)) ⋯ ∘ₖ
        (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) ⋯ ∥ₖ Kernel.deterministic id ⋯))
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
              sorry ∘ₖ
            Kernel.deterministic
              (Prod.map id
                (⇑MeasurableEquiv.prodAssoc :
                  (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
              sorry ∘ₖ
          Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) sorry ∘ₖ
        Kernel.deterministic
          (Prod.map id
            (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
              (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier))
          sorry ∘ₖ
      Kernel.deterministic
        (⇑MeasurableEquiv.prodAssoc :
          (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
        sorry ∘ₖ
    (Kernel.deterministic (Prod.map id fun (x : Y.carrier) ↦ (x, x)) sorry ∘ₖ
      Kernel.deterministic (Prod.map (fun (x : X.carrier) ↦ (x, x)) id) sorry)
Tactic: rw [Kernel.deterministic_parallelComp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
                (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                  (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
                ⋯ ∘ₖ
              (Kernel.deterministic id ⋯ ∥ₖ
                Kernel.deterministic
                  (⇑MeasurableEquiv.prodAssoc :
                    (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier)
                  ⋯) ∘ₖ
            (Kernel.deterministic id ⋯ ∥ₖ (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)) ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ
            Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier)
              ⋯) ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc :
            (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (fun (x : Y.carrier) ↦ (x, x)) ⋯ ∘ₖ
        (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) ⋯ ∥ₖ Kernel.deterministic id ⋯))
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  Kernel.deterministic
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
              sorry ∘ₖ
            Kernel.deterministic
              (Prod.map id
                (⇑MeasurableEquiv.prodAssoc :
                  (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
              sorry ∘ₖ
          Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) sorry ∘ₖ
        Kernel.deterministic
          (Prod.map id
            (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
              (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier))
          sorry ∘ₖ
      Kernel.deterministic
        (⇑MeasurableEquiv.prodAssoc :
          (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
        sorry ∘ₖ
    (Kernel.deterministic (Prod.map id fun (x : Y.carrier) ↦ (x, x)) sorry ∘ₖ
      Kernel.deterministic (Prod.map (fun (x : X.carrier) ↦ (x, x)) id) sorry)
Tactic: repeat rw [Kernel.deterministic_parallelComp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
                (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                  (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
                ⋯ ∘ₖ
              Kernel.deterministic
                (Prod.map id
                  (⇑MeasurableEquiv.prodAssoc :
                    (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier))
                ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic
            (Prod.map id
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier))
            ⋯ ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc :
            (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id fun (x : Y.carrier) ↦ (x, x)) ⋯ ∘ₖ
        Kernel.deterministic (Prod.map (fun (x : X.carrier) ↦ (x, x)) id) ⋯)
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  Kernel.deterministic
            (Function.comp (β := X.carrier × Y.carrier × X.carrier × Y.carrier)
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × X.carrier × Y.carrier) → (X.carrier × Y.carrier) × X.carrier × Y.carrier)
              (Prod.map id
                (⇑MeasurableEquiv.prodAssoc :
                  (a : (Y.carrier × X.carrier) × Y.carrier) → Y.carrier × X.carrier × Y.carrier)))
            sorry ∘ₖ
          Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) sorry ∘ₖ
        Kernel.deterministic
          (Prod.map id
            (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
              (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier))
          sorry ∘ₖ
      Kernel.deterministic
        (⇑MeasurableEquiv.prodAssoc :
          (a : (X.carrier × X.carrier) × Y.carrier × Y.carrier) → X.carrier × X.carrier × Y.carrier × Y.carrier)
        sorry ∘ₖ
    (Kernel.deterministic (Prod.map id fun (x : Y.carrier) ↦ (x, x)) sorry ∘ₖ
      Kernel.deterministic (Prod.map (fun (x : X.carrier) ↦ (x, x)) id) sorry)
Tactic: rw [Kernel.deterministic_comp_deterministic]