awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y Z : SFinKer
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))
      ⋯ =
    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)
      ⋯
⊢ 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) ⋯

Tactic:
repeat rw [Kernel.deterministic_comp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
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)) ∘
        Prod.map id Prod.swap)
      ⋯

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
h :
  Hom.hom
      (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 := ⋯ })) =
    Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y))
⊢ 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)

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
⊢ Hom.hom
      (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 := ⋯ })) =
    Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y))

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
⊢ IsSFiniteKernel.{u_1, u_1} (α := X.carrier) (β := (𝟙_ SFinKer) (𝒞 := instLargeCategory).carrier) (mα := X.str) (mβ :=
    (𝟙_ SFinKer) (𝒞 := instLargeCategory).str) (Kernel.deterministic (fun (x : X.carrier) ↦ PUnit.unit) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
⊢ IsSFiniteKernel.{u_1, u_1} (α := X.carrier) (mα := X.str) (Kernel.deterministic (fun (x : X.carrier) ↦ (x, x)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
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 := ⋯ } ({ hom := Kernel.discard X.carrier, property := ⋯ } ▷ X)))
    (Hom.hom (Iso.inv (λ_ X)))
⊢ 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))

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
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))
⊢ 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)))

Tactic:
dsimp
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
⊢ Measurable (β := PUnit.{u_1 + 1} × X.carrier) fun (x : X.carrier) ↦ (PUnit.unit, x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
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))
      ⋯)
    (Kernel.deterministic ((fun (x : X.carrier) ↦ (PUnit.unit, x)) ∘ id) ⋯)
⊢ 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))

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic,
      Kernel.deterministic_comp_deterministic, Kernel.deterministic_map measurable_id (by fun_prop)]

Premises used: ProbabilityTheory.Kernel.deterministic_map, measurable_id, ProbabilityTheory.Kernel.deterministic_comp_deterministic, ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
⊢ 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))
      ⋯)
    (Kernel.deterministic ((fun (x : X.carrier) ↦ (PUnit.unit, x)) ∘ id) ⋯)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
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 := ⋯ } (X ◁ { hom := Kernel.discard X.carrier, property := ⋯ })))
    (Hom.hom (Iso.inv (ρ_ X)))
⊢ 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))

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
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))
⊢ 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)))

Tactic:
dsimp
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
⊢ Measurable (β := X.carrier × PUnit.{u_1 + 1}) fun (x : X.carrier) ↦ (x, PUnit.unit)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
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))
      ⋯)
    (Kernel.deterministic ((fun (x : X.carrier) ↦ (x, PUnit.unit)) ∘ id) ⋯)
⊢ 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))

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic,
      Kernel.deterministic_comp_deterministic, Kernel.deterministic_map measurable_id (by fun_prop)]

Premises used: ProbabilityTheory.Kernel.deterministic_map, measurable_id, ProbabilityTheory.Kernel.deterministic_comp_deterministic, ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
⊢ 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))
      ⋯)
    (Kernel.deterministic ((fun (x : X.carrier) ↦ (x, PUnit.unit)) ∘ id) ⋯)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
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 := ⋯ } (X ◁ { hom := Kernel.copy X.carrier, property := ⋯ })))
    (Hom.hom
      (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))))
⊢ 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)))

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
h :
  Kernel.deterministic
      (Function.comp (β := X.carrier × X.carrier) (Prod.map id fun (x : X.carrier) ↦ (x, x)) fun (x : X.carrier) ↦
        (x, x))
      ⋯ =
    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))
      ⋯
⊢ 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

Tactic:
simp [Kernel.copy, Kernel.id, Kernel.deterministic_comp_deterministic,
      Kernel.deterministic_parallelComp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic, ProbabilityTheory.Kernel.id, ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic, ProbabilityTheory.Kernel.copy
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
⊢ Kernel.deterministic
      (Function.comp (β := X.carrier × X.carrier) (Prod.map id fun (x : X.carrier) ↦ (x, x)) fun (x : X.carrier) ↦
        (x, x))
      ⋯ =
    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))
      ⋯

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
h : (Δ ≫ Iso.hom (β_ X X)).hom = Hom.hom Δ
⊢ Δ ≫ Iso.hom (β_ X X) = Δ

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
⊢ Eq.{u + 1} (α := Kernel X.carrier (X.carrier × X.carrier)) (Kernel.swap X.carrier X.carrier ∘ₖ Kernel.copy X.carrier)
    (Kernel.copy X.carrier)

Tactic:
Kernel.swap_copy

Premises used: ProbabilityTheory.Kernel.swap_copy
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
⊢ Eq.{u + 1} (α := Kernel X.carrier (X.carrier × X.carrier)) (Kernel.swap X.carrier X.carrier ∘ₖ Kernel.copy X.carrier)
    (Kernel.copy X.carrier)

Tactic:
exact Kernel.swap_copy

Premises used: ProbabilityTheory.Kernel.swap_copy
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
h : Hom.hom Δ = ((Δ ⊗ₘ Δ) ≫ MonoidalCategory.tensorμ X X Y Y).hom
⊢ Δ = (Δ ⊗ₘ Δ) ≫ MonoidalCategory.tensorμ X X Y Y

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
h :
  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 ⋯))
⊢ 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 ⋯))

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
h :
  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 ⋯))
⊢ 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 ⋯))

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
h :
  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 ⋯))
⊢ 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 ⋯))

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic