awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
              (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) ⋯)
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)) ∘
            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]
-- 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
            (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) ⋯)
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  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)))
        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]
-- 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
          (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) ⋯)
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  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))
      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]
-- 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
        (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) ⋯)
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  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))
      sorry ∘ₖ
    Kernel.deterministic ((Prod.map id fun (x : Y.carrier) ↦ (x, x)) ∘ Prod.map (fun (x : X.carrier) ↦ (x, x)) id) sorry
Tactic: rw [Kernel.deterministic_comp_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
        (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) ⋯
have h : Kernel.deterministic (fun (x : X.carrier × Y.carrier) ↦ (x, x)) sorry =
  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 × (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))
      ((Prod.map id fun (x : Y.carrier) ↦ (x, x)) ∘ Prod.map (fun (x : X.carrier) ↦ (x, x)) id))
    sorry
Tactic: rw [Kernel.deterministic_comp_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 × X.carrier) × Y.carrier × Y.carrier)
      (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))
      ((Prod.map id fun (x : Y.carrier) ↦ (x, x)) ∘ Prod.map (fun (x : X.carrier) ↦ (x, x)) id))
    sorry
Tactic: repeat rw [Kernel.deterministic_comp_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Eq (α := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y ⟶ (𝟙_ SFinKer) (𝒞 := instLargeCategory)) ε
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ ((𝟙_ SFinKer) (𝒞 := instLargeCategory))))
have h : Eq (α :=
  Kernel (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).carrier
    (𝟙_ SFinKer) (𝒞 := instLargeCategory).carrier)
  (Hom.hom ε) (Hom.hom ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ ((𝟙_ SFinKer) (𝒞 := instLargeCategory)))))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Eq.{u + 1} (α := Kernel (X.carrier × Y.carrier) PUnit.{u + 1}) (Kernel.discard (X.carrier × Y.carrier))
    (Kernel.map Kernel.id Prod.snd ∘ₖ
      (Kernel.id ∥ₖ Kernel.discard Y.carrier ∘ₖ (Kernel.discard X.carrier ∥ₖ Kernel.id)))
have h : Eq.{u + 1} (α := Kernel (X.carrier × Y.carrier) PUnit.{u + 1}) (Kernel.discard (X.carrier × Y.carrier))
  (Kernel.map Kernel.id Prod.snd ∘ₖ (Kernel.discard X.carrier ∥ₖ Kernel.discard Y.carrier))
Tactic: simp only [Kernel.id_parallelComp_comp_parallelComp_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Eq.{u + 1} (α := Kernel (X.carrier × Y.carrier) PUnit.{u + 1}) (Kernel.discard (X.carrier × Y.carrier))
    (Kernel.map Kernel.id Prod.snd ∘ₖ (Kernel.discard X.carrier ∥ₖ Kernel.discard Y.carrier))
have h : Eq (α := Kernel (X.carrier × Y.carrier) PUnit.{u + 1}) (Kernel.discard (X.carrier × Y.carrier))
  (Kernel.map (Kernel.discard X.carrier ∥ₖ Kernel.discard Y.carrier) Prod.snd)
Tactic: rw [Kernel.id_map (by fun_prop), Kernel.deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
⊢ Eq (α := Kernel (X.carrier × Y.carrier) PUnit.{u + 1}) (Kernel.discard (X.carrier × Y.carrier))
    (Kernel.map (Kernel.discard X.carrier ∥ₖ Kernel.discard Y.carrier) Prod.snd)
have h : ∀ (a : X.carrier × Y.carrier) (s : Set PUnit.{u + 1}),
  MeasurableSet s →
    Eq (α := ENNReal)
      ((((Kernel.discard (X.carrier × Y.carrier) : (a : X.carrier × Y.carrier) → Measure PUnit.{u + 1}) a :
              Measure PUnit.{u + 1}) :
            (a : Set PUnit.{u + 1}) → ENNReal)
          s :
        ENNReal)
      ((((Kernel.map (Kernel.discard X.carrier ∥ₖ Kernel.discard Y.carrier) Prod.snd :
                  (a : X.carrier × Y.carrier) → Measure PUnit.{u + 1})
                a :
              Measure PUnit.{u + 1}) :
            (a : Set PUnit.{u + 1}) → ENNReal)
          s :
        ENNReal)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
a : X.carrier × Y.carrier
s : Set PUnit.{u + 1}
h : MeasurableSet s
⊢ Eq (α := ENNReal)
    ((((Kernel.discard (X.carrier × Y.carrier) : (a : X.carrier × Y.carrier) → Measure PUnit.{u + 1}) a :
            Measure PUnit.{u + 1}) :
          (a : Set PUnit.{u + 1}) → ENNReal)
        s :
      ENNReal)
    ((((Kernel.map (Kernel.discard X.carrier ∥ₖ Kernel.discard Y.carrier) Prod.snd :
                (a : X.carrier × Y.carrier) → Measure PUnit.{u + 1})
              a :
            Measure PUnit.{u + 1}) :
          (a : Set PUnit.{u + 1}) → ENNReal)
        s :
      ENNReal)
have h : Eq (α := ENNReal)
  ((((Kernel.discard (X.carrier × Y.carrier) : (a : X.carrier × Y.carrier) → Measure PUnit.{u + 1}) a :
          Measure PUnit.{u + 1}) :
        (a : Set PUnit.{u + 1}) → ENNReal)
      s :
    ENNReal)
  (((Measure.map (α := PUnit.{u + 1} × PUnit.{u + 1}) Prod.snd
            (Measure.prod ((Kernel.discard X.carrier : (a : X.carrier) → Measure PUnit.{u + 1}) a.1)
              ((Kernel.discard Y.carrier : (a : Y.carrier) → Measure PUnit.{u + 1}) a.2)) :
          Measure PUnit.{u + 1}) :
        (a : Set PUnit.{u + 1}) → ENNReal)
      s :
    ENNReal)
Tactic: rw [Kernel.map_apply _ (by fun_prop), Kernel.parallelComp_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
⊢ Δ = Iso.inv (λ_ ((𝟙_ SFinKer) (𝒞 := instLargeCategory)))
have h : Eq (α :=
  Kernel (𝟙_ SFinKer) (𝒞 := instLargeCategory).carrier
    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) ((𝟙_ SFinKer) (𝒞 := instLargeCategory))
        ((𝟙_ SFinKer) (𝒞 := instLargeCategory))).carrier)
  (Hom.hom Δ) (Hom.hom (Iso.inv (λ_ ((𝟙_ SFinKer) (𝒞 := instLargeCategory)))))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
⊢ Eq (α := Kernel PUnit.{u + 1} (PUnit.{u + 1} × PUnit.{u + 1})) (Kernel.copy PUnit.{u + 1})
    (Kernel.map Kernel.id fun (x : PUnit.{u + 1}) ↦ (PUnit.unit, x))
have h : ∀ (a : PUnit.{u + 1}) (s : Set (PUnit.{u + 1} × PUnit.{u + 1})),
  MeasurableSet s →
    Eq (α := ENNReal)
      ((((Kernel.copy PUnit.{u + 1} : (a : PUnit.{u + 1}) → Measure (PUnit.{u + 1} × PUnit.{u + 1})) a :
              Measure (PUnit.{u + 1} × PUnit.{u + 1})) :
            (a : Set (PUnit.{u + 1} × PUnit.{u + 1})) → ENNReal)
          s :
        ENNReal)
      ((((Kernel.map Kernel.id fun (x : PUnit.{u + 1}) ↦ (PUnit.unit, x) :
                  (a : PUnit.{u + 1}) → Measure (PUnit.{u + 1} × PUnit.{u + 1}))
                a :
              Measure (PUnit.{u + 1} × PUnit.{u + 1})) :
            (a : Set (PUnit.{u + 1} × PUnit.{u + 1})) → ENNReal)
          s :
        ENNReal)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
a : PUnit.{u + 1}
s : Set (PUnit.{u + 1} × PUnit.{u + 1})
h : MeasurableSet s
⊢ Eq (α := ENNReal)
    ((((Kernel.copy PUnit.{u + 1} : (a : PUnit.{u + 1}) → Measure (PUnit.{u + 1} × PUnit.{u + 1})) a :
            Measure (PUnit.{u + 1} × PUnit.{u + 1})) :
          (a : Set (PUnit.{u + 1} × PUnit.{u + 1})) → ENNReal)
        s :
      ENNReal)
    ((((Kernel.map Kernel.id fun (x : PUnit.{u + 1}) ↦ (PUnit.unit, x) :
                (a : PUnit.{u + 1}) → Measure (PUnit.{u + 1} × PUnit.{u + 1}))
              a :
            Measure (PUnit.{u + 1} × PUnit.{u + 1})) :
          (a : Set (PUnit.{u + 1} × PUnit.{u + 1})) → ENNReal)
        s :
      ENNReal)
have h : Eq (α := ENNReal)
  ((((Kernel.copy PUnit.{u + 1} : (a : PUnit.{u + 1}) → Measure (PUnit.{u + 1} × PUnit.{u + 1})) a :
          Measure (PUnit.{u + 1} × PUnit.{u + 1})) :
        (a : Set (PUnit.{u + 1} × PUnit.{u + 1})) → ENNReal)
      s :
    ENNReal)
  ((((Kernel.deterministic (fun (x : PUnit.{u + 1}) ↦ (PUnit.unit, x)) sorry :
              (a : PUnit.{u + 1}) → Measure (PUnit.{u + 1} × PUnit.{u + 1}))
            a :
          Measure (PUnit.{u + 1} × PUnit.{u + 1})) :
        (a : Set (PUnit.{u + 1} × PUnit.{u + 1})) → ENNReal)
      s :
    ENNReal)
Tactic: rw [Kernel.id_map (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst : IsDeterministic κ
inst_1 : IsMarkovKernel κ
⊢ Eq.{u_1 + 1} (α := X ⟶ MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y Y)
    ({ hom := κ, property := ⋯ : X.Hom Y } ≫ Δ)
    (Δ ≫ ({ hom := κ, property := ⋯ : X.Hom Y } ⊗ₘ { hom := κ, property := ⋯ : X.Hom Y }))
have h : Eq.{u_1 + 1} (α := Kernel X.carrier (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y Y).carrier)
  (Hom.hom ({ hom := κ, property := sorry : X.Hom Y } ≫ Δ))
  (Hom.hom (Δ ≫ ({ hom := κ, property := sorry : X.Hom Y } ⊗ₘ { hom := κ, property := sorry : X.Hom Y })))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst : IsDeterministic κ
inst_1 : IsMarkovKernel κ
⊢ Eq.{u_1 + 1} (α := Kernel X.carrier (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y Y).carrier)
    (Hom.hom ({ hom := κ, property := ⋯ : X.Hom Y } ≫ Δ))
    (Hom.hom (Δ ≫ ({ hom := κ, property := ⋯ : X.Hom Y } ⊗ₘ { hom := κ, property := ⋯ : X.Hom Y })))
have h : Kernel.copy Y.carrier ∘ₖ κ = Kernel.id ∥ₖ κ ∘ₖ (κ ∥ₖ Kernel.id) ∘ₖ Kernel.copy X.carrier
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst : IsDeterministic κ
inst_1 : IsMarkovKernel κ
⊢ Kernel.copy Y.carrier ∘ₖ κ = Kernel.id ∥ₖ κ ∘ₖ (κ ∥ₖ Kernel.id) ∘ₖ Kernel.copy X.carrier
have h : Kernel.copy Y.carrier ∘ₖ κ = κ ∥ₖ κ ∘ₖ Kernel.copy X.carrier
Tactic: rw [Kernel.id_parallelComp_comp_parallelComp_id]