awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y Z : SFinKer
h :
  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.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)
⊢ 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 id ⋯ ∥ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × X.carrier) × Z.carrier) → Y.carrier × X.carrier × Z.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic Prod.swap ⋯ ∥ₖ 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 Z : SFinKer
h :
  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) ⋯
⊢ 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.swap ⋯ ∥ₖ 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 Z : SFinKer
h :
  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) ⋯
⊢ 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 id ⋯ ∥ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
        Kernel.deterministic
          (⇑MeasurableEquiv.prodAssoc : (a : (Y.carrier × X.carrier) × Z.carrier) → Y.carrier × X.carrier × Z.carrier)
          ⋯ ∘ₖ
      (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)

Tactic:
repeat rw [Kernel.deterministic_parallelComp_deterministic]

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

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.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)) ∘
        Prod.map Prod.swap id)
      ⋯

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

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

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

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

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

Tactic:
repeat rw [Kernel.deterministic_parallelComp_deterministic]

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

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic
-- 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) ⋯ ∘ₖ
        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) ⋯
⊢ 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) ⋯

Tactic:
rw [Kernel.deterministic_comp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic
-- 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))
        ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
⊢ 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) ⋯

Tactic:
rw [Kernel.deterministic_comp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic
-- 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
      (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) ⋯

Tactic:
rw [Kernel.deterministic_comp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic