awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
            (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 ⋯))
⊢ 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 ⋯))

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
            (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 ⋯))
⊢ 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 ⋯))

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
            (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) ⋯)
⊢ 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 ⋯))

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
            (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) ⋯)
⊢ 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:
repeat 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
              (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)))
              ⋯ ∘ₖ
            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) ⋯)
⊢ 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) ⋯)

Tactic:
rw [Kernel.deterministic_comp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
h :
  Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    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)) ∘
              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) ⋯)
⊢ Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    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)))
              ⋯ ∘ₖ
            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) ⋯)

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
h :
  Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
        (Function.comp (β := X.carrier × X.carrier × Y.carrier × Y.carrier)
          (Function.comp (β := X.carrier × (X.carrier × Y.carrier) × Y.carrier)
            (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)) ∘
              Prod.map id (Prod.map Prod.swap id))
            (Prod.map id
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier)))
          (⇑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) ⋯)
⊢ Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
          (Function.comp (β := X.carrier × (X.carrier × Y.carrier) × Y.carrier)
            (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)) ∘
              Prod.map id (Prod.map Prod.swap id))
            (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) ⋯)

Tactic:
rw [Kernel.deterministic_comp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
h :
  Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
        (Function.comp (β := X.carrier × X.carrier × Y.carrier × Y.carrier)
          (Function.comp (β := X.carrier × (X.carrier × Y.carrier) × Y.carrier)
            (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)) ∘
              Prod.map id (Prod.map Prod.swap id))
            (Prod.map id
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier)))
          (⇑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)) ∘ Prod.map (fun (x : X.carrier) ↦ (x, x)) id) ⋯
⊢ Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) ⋯ =
    Kernel.deterministic
        (Function.comp (β := X.carrier × X.carrier × Y.carrier × Y.carrier)
          (Function.comp (β := X.carrier × (X.carrier × Y.carrier) × Y.carrier)
            (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)) ∘
              Prod.map id (Prod.map Prod.swap id))
            (Prod.map id
              (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) :
                (a : X.carrier × Y.carrier × Y.carrier) → (X.carrier × Y.carrier) × Y.carrier)))
          (⇑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) ⋯)

Tactic:
rw [Kernel.deterministic_comp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic