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

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 × (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))
      ⋯
⊢ 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:
repeat rw [Kernel.deterministic_comp_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
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 × (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))
      ⋯

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
h :
  Eq (α :=
    Kernel (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).carrier
      (𝟙_ SFinKer) (𝒞 := instLargeCategory).carrier)
    (Hom.hom ε) (Hom.hom ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ ((𝟙_ SFinKer) (𝒞 := instLargeCategory)))))
⊢ Eq (α := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y ⟶ (𝟙_ SFinKer) (𝒞 := instLargeCategory)) ε
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ ((𝟙_ SFinKer) (𝒞 := instLargeCategory))))

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

Tactic:
simp only [Kernel.id_parallelComp_comp_parallelComp_id]

Premises used: ProbabilityTheory.Kernel.id_parallelComp_comp_parallelComp_id
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
⊢ Measurable.{u, u} (α := PUnit.{u + 1} × PUnit.{u + 1}) Prod.snd

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
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)
⊢ 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:
rw [Kernel.id_map (by fun_prop), Kernel.deterministic_comp_eq_map]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_eq_map, ProbabilityTheory.Kernel.id_map
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
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)
⊢ 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:
ext
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
a : X.carrier × Y.carrier
s : Set PUnit.{u + 1}
h : MeasurableSet s
⊢ Measurable.{u, u} (α := PUnit.{u + 1} × PUnit.{u + 1}) Prod.snd

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
a : X.carrier × Y.carrier
s : Set PUnit.{u + 1}
h_1 : MeasurableSet s
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)
⊢ 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:
rw [Kernel.map_apply _ (by fun_prop), Kernel.parallelComp_apply]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
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)
    (((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:
simp [Kernel.discard_apply]

Premises used: ProbabilityTheory.Kernel.discard_apply
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
h :
  Eq (α :=
    Kernel (𝟙_ SFinKer) (𝒞 := instLargeCategory).carrier
      (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) ((𝟙_ SFinKer) (𝒞 := instLargeCategory))
          ((𝟙_ SFinKer) (𝒞 := instLargeCategory))).carrier)
    (Hom.hom Δ) (Hom.hom (Iso.inv (λ_ ((𝟙_ SFinKer) (𝒞 := instLargeCategory)))))
⊢ Δ = Iso.inv (λ_ ((𝟙_ SFinKer) (𝒞 := instLargeCategory)))

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

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
a : PUnit.{u + 1}
s : Set (PUnit.{u + 1} × PUnit.{u + 1})
h : MeasurableSet s
⊢ Measurable (β := PUnit.{u + 1} × PUnit.{u + 1}) fun (x : PUnit.{u + 1}) ↦ (PUnit.unit, x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
a : PUnit.{u + 1}
s : Set (PUnit.{u + 1} × PUnit.{u + 1})
h_1 : MeasurableSet s
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)) ⋯ :
                (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)
⊢ 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:
rw [Kernel.id_map (by fun_prop)]

Premises used: ProbabilityTheory.Kernel.id_map
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
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.deterministic (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:
simp [Kernel.copy_apply, Kernel.deterministic_apply]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, ProbabilityTheory.Kernel.copy_apply
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst : IsDeterministic κ
inst_1 : IsMarkovKernel κ
h :
  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 })))
⊢ 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 }))

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst : IsDeterministic κ
inst_1 : IsMarkovKernel κ
h : Kernel.copy Y.carrier ∘ₖ κ = Kernel.id ∥ₖ κ ∘ₖ (κ ∥ₖ Kernel.id) ∘ₖ Kernel.copy X.carrier
⊢ 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 })))

Tactic:
dsimp
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst : IsDeterministic κ
inst_1 : IsMarkovKernel κ
h : Kernel.copy Y.carrier ∘ₖ κ = κ ∥ₖ κ ∘ₖ Kernel.copy X.carrier
⊢ Kernel.copy Y.carrier ∘ₖ κ = Kernel.id ∥ₖ κ ∘ₖ (κ ∥ₖ Kernel.id) ∘ₖ Kernel.copy X.carrier

Tactic:
rw [Kernel.id_parallelComp_comp_parallelComp_id]

Premises used: ProbabilityTheory.Kernel.id_parallelComp_comp_parallelComp_id
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst : IsDeterministic κ
inst_1 : IsMarkovKernel κ
⊢ Kernel.copy Y.carrier ∘ₖ κ = κ ∥ₖ κ ∘ₖ Kernel.copy X.carrier

Tactic:
(Kernel.parallelComp_self_comp_copy).symm

Premises used: ProbabilityTheory.Kernel.parallelComp_self_comp_copy, Eq.symm
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst : IsDeterministic κ
inst_1 : IsMarkovKernel κ
⊢ Kernel.copy Y.carrier ∘ₖ κ = κ ∥ₖ κ ∘ₖ Kernel.copy X.carrier

Tactic:
exact (Kernel.parallelComp_self_comp_copy).symm

Premises used: ProbabilityTheory.Kernel.parallelComp_self_comp_copy, Eq.symm
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y Z : SFinKer
⊢ Deterministic (X :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory)
      (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y) Z)
    (Iso.hom (α_ X Y Z))

Tactic:
deterministic_deterministic ((X ⊗ Y) ⊗ Z)
    (X ⊗ Y ⊗ Z) (Kernel.deterministic MeasurableEquiv.prodAssoc (MeasurableEquiv.measurable _))

Premises used: SFinKer.deterministic_deterministic, ProbabilityTheory.Kernel.deterministic, MeasurableEquiv.prodAssoc, CategoryTheory.MonoidalCategoryStruct.tensorObj, MeasurableEquiv.measurable, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
Y : SFinKer
Z : SFinKer
⊢ Measurable.{u_1, u_1} (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) ((𝟙_ SFinKer) (𝒞 := instLargeCategory)) X).carrier)
    Prod.snd

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
Y : SFinKer
Z : SFinKer
⊢ Measurable.{u_1, u_1} (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X ((𝟙_ SFinKer) (𝒞 := instLargeCategory))).carrier)
    Prod.fst

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
Z : SFinKer
⊢ Measurable.{u_1, u_1} (α := (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).carrier) Prod.swap

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
Y : SFinKer
Z : SFinKer
⊢ Measurable (β := (𝟙_ SFinKer) (𝒞 := instLargeCategory).carrier) fun (x : X.carrier) ↦ PUnit.unit

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X : SFinKer
Y : SFinKer
Z : SFinKer
⊢ Measurable (β := (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X X).carrier) fun (x : X.carrier) ↦ (x, x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X : SFinKer
⊢ IsMarkovKernel.{u_1, u_1} (α := X.carrier) (mα := X.str) Kernel.id

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y Z : SFinKer
κ : X ⟶ Y
η : Y ⟶ Z
hκ : StochHom κ
hη : StochHom η
⊢ IsMarkovKernel (η.hom ∘ₖ κ.hom)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y Z : SFinKer
κ : Y ⟶ Z
hκ : StochHom κ
⊢ IsMarkovKernel (α := X.carrier × Y.carrier) (mα :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := SFinKer.instLargeCategory) X Y).str) (Kernel.id ∥ₖ κ.hom)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X₁ X₂ : SFinKer
κ : X₁ ⟶ X₂
hκ : StochHom κ
Y : SFinKer
⊢ IsMarkovKernel (α := X₁.carrier × Y.carrier) (mα :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := SFinKer.instLargeCategory) X₁ Y).str) (κ.hom ∥ₖ Kernel.id)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X : SFinKer
⊢ Measurable.{u_1, u_1} (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := SFinKer.instLargeCategory) ((𝟙_ SFinKer) (𝒞 := SFinKer.instLargeCategory))
        X).carrier)
    Prod.snd

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X : SFinKer
⊢ Measurable (β :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := SFinKer.instLargeCategory) ((𝟙_ SFinKer) (𝒞 := SFinKer.instLargeCategory))
        X).carrier)
    fun (x : X.carrier) ↦ (PUnit.unit, x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X : SFinKer
⊢ Measurable.{u_1, u_1} (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := SFinKer.instLargeCategory) X
        ((𝟙_ SFinKer) (𝒞 := SFinKer.instLargeCategory))).carrier)
    Prod.fst

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X : SFinKer
⊢ Measurable (β :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := SFinKer.instLargeCategory) X
        ((𝟙_ SFinKer) (𝒞 := SFinKer.instLargeCategory))).carrier)
    fun (x : X.carrier) ↦ (x, PUnit.unit)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X : SFinKer
⊢ IsMarkovKernel.{u_1, u_1} (α := X.carrier) (mα := X.str) (Kernel.discard X.carrier)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X : SFinKer
⊢ IsMarkovKernel.{u_1, u_1} (α := X.carrier) (mα := X.str) (copy X.carrier)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ : X ⟶ Y
h :
  Eq.{u_1 + 1} (α :=
    X.obj (_P := StochHom) ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := WideSubcategory.category StochHom)
            ((𝟙_ Stoch) (𝒞 := WideSubcategory.category StochHom))
            ((𝟙_ Stoch) (𝒞 := WideSubcategory.category StochHom))).obj
        (_P := StochHom))
    (InducedWideCategory.Hom.hom (P := StochHom) (ε ≫ Δ)) (InducedWideCategory.Hom.hom (P := StochHom) (Δ ≫ (ε ⊗ₘ ε)))
⊢ Eq.{u_1 + 1} (α :=
    X ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WideSubcategory.category StochHom)
        ((𝟙_ Stoch) (𝒞 := WideSubcategory.category StochHom)) ((𝟙_ Stoch) (𝒞 := WideSubcategory.category StochHom)))
    (ε ≫ Δ) (Δ ≫ (ε ⊗ₘ ε))

Tactic:
ext : 1