mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X₁✝ X₂✝ : SFinKer
κ : X₁✝ ⟶ X₂✝
hκ : StochHom κ
Y : SFinKer
⊢ IsMarkovKernel (κ.hom ∥ₖ Kernel.id)

Tactic:
;

Goal state after:
X₁✝ X₂✝ : SFinKer
κ : X₁✝ ⟶ X₂✝
hκ : StochHom κ
Y : SFinKer
⊢ IsMarkovKernel (κ.hom ∥ₖ Kernel.id)
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X : SFinKer
⊢ IsMarkovKernel (Kernel.discard X.carrier)

Tactic:
;

Goal state after:
X : SFinKer
⊢ IsMarkovKernel (Kernel.discard X.carrier)
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X : SFinKer
⊢ IsMarkovKernel (copy X.carrier)

Tactic:
;

Goal state after:
X : SFinKer
⊢ IsMarkovKernel (copy X.carrier)
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X✝ Y✝ : Stoch
κ✝ : X✝ ⟶ Y✝
X Y : Stoch
κ : Kernel X.obj.carrier Y.obj.carrier
inst✝¹ : IsDeterministic κ
inst✝ : IsMarkovKernel κ
⊢ ({ hom := { hom := κ, property := ⋯ }, property := ⋯ } ≫ Δ).hom =
    (Δ ≫
        ({ hom := { hom := κ, property := ⋯ }, property := ⋯ } ⊗ₘ
          { hom := { hom := κ, property := ⋯ }, property := ⋯ })).hom

Tactic:
;

Goal state after:
X✝ Y✝ : Stoch
κ✝ : X✝ ⟶ Y✝
X Y : Stoch
κ : Kernel X.obj.carrier Y.obj.carrier
inst✝¹ : IsDeterministic κ
inst✝ : IsMarkovKernel κ
⊢ ({ hom := { hom := κ, property := ⋯ }, property := ⋯ } ≫ Δ).hom =
    (Δ ≫
        ({ hom := { hom := κ, property := ⋯ }, property := ⋯ } ⊗ₘ
          { hom := { hom := κ, property := ⋯ }, property := ⋯ })).hom
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X Y : Stoch
κ✝ : X ⟶ Y
X✝ Y✝ : Stoch
κ : X✝ ⟶ Y✝
⊢ (κ ≫ ε).hom.hom = ε.hom.hom

Tactic:
;

Goal state after:
X Y : Stoch
κ✝ : X ⟶ Y
X✝ Y✝ : Stoch
κ : X✝ ⟶ Y✝
⊢ (κ ≫ ε).hom.hom = ε.hom.hom
Module: Mathlib.Probability.Kernel.Irreducible

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
φ : Measure α
inst✝ : Subsingleton α
s : Set α
hs : MeasurableSet s
hsp : φ s > 0
a : α
⊢ ((Kernel.id ^ 1) a) s > 0

Tactic:
;

Goal state after:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
φ : Measure α
inst✝ : Subsingleton α
s : Set α
hs : MeasurableSet s
hsp : φ s > 0
a : α
⊢ ((Kernel.id ^ 1) a) s > 0
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_1
X Y Z : SFinKer
⊢ ({ hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ } ≫
        { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }).hom =
    (𝟙
        { carrier := { carrier := X.carrier × Y.carrier, str := Prod.instMeasurableSpace }.carrier × Z.carrier,
          str := Prod.instMeasurableSpace }).hom

Tactic:
;

Goal state after:
case refine_1
X Y Z : SFinKer
⊢ ({ hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ } ≫
        { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }).hom =
    (𝟙
        { carrier := { carrier := X.carrier × Y.carrier, str := Prod.instMeasurableSpace }.carrier × Z.carrier,
          str := Prod.instMeasurableSpace }).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X Y Z : SFinKer
⊢ ({ hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ } ≫
        { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ }).hom =
    (𝟙
        { carrier := X.carrier × { carrier := Y.carrier × Z.carrier, str := Prod.instMeasurableSpace }.carrier,
          str := Prod.instMeasurableSpace }).hom

Tactic:
;

Goal state after:
case refine_2
X Y Z : SFinKer
⊢ ({ hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ } ≫
        { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ }).hom =
    (𝟙
        { carrier := X.carrier × { carrier := Y.carrier × Z.carrier, str := Prod.instMeasurableSpace }.carrier,
          str := Prod.instMeasurableSpace }).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_1
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := ⋯
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ ({ hom := Kernel.id.map Prod.snd, property := ⋯ } ≫ { hom := Kernel.id.map f₁, property := ⋯ }).hom =
    (𝟙
        { carrier := { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier × X.carrier,
          str := Prod.instMeasurableSpace }).hom

Tactic:
;

Goal state after:
case refine_1
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := ⋯
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ ({ hom := Kernel.id.map Prod.snd, property := ⋯ } ≫ { hom := Kernel.id.map f₁, property := ⋯ }).hom =
    (𝟙
        { carrier := { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier × X.carrier,
          str := Prod.instMeasurableSpace }).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := ⋯
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ ({ hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.snd, property := ⋯ }).hom = (𝟙 X).hom

Tactic:
;

Goal state after:
case refine_2
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := ⋯
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ ({ hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.snd, property := ⋯ }).hom = (𝟙 X).hom
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ (∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X) (s : Set X),
      MeasurableSet s → ((π.restrict ⋯) x) s = B.indicator (fun x ↦ 1) x * (π x) s) ↔
    ∀ ⦃A : Set X⦄,
      MeasurableSet A → ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A

Tactic:
;

Goal state after:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ (∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X) (s : Set X),
      MeasurableSet s → ((π.restrict ⋯) x) s = B.indicator (fun x ↦ 1) x * (π x) s) ↔
    ∀ ⦃A : Set X⦄,
      MeasurableSet A → ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
⊢ ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A ↔ (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Tactic:
;

Goal state after:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
⊢ ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A ↔ (π x) (A ∩ B) = B.indicator 1 x * (π x) A
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_1
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := ⋯
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ ({ hom := Kernel.id.map Prod.fst, property := ⋯ } ≫ { hom := Kernel.id.map f₁, property := ⋯ }).hom =
    (𝟙
        { carrier := X.carrier × { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier,
          str := Prod.instMeasurableSpace }).hom

Tactic:
;

Goal state after:
case refine_1
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := ⋯
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ ({ hom := Kernel.id.map Prod.fst, property := ⋯ } ≫ { hom := Kernel.id.map f₁, property := ⋯ }).hom =
    (𝟙
        { carrier := X.carrier × { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier,
          str := Prod.instMeasurableSpace }).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := ⋯
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ ({ hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.fst, property := ⋯ }).hom = (𝟙 X).hom

Tactic:
;

Goal state after:
case refine_2
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := ⋯
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ ({ hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.fst, property := ⋯ }).hom = (𝟙 X).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η₁ : Y₁✝ ⟶ Z₁✝
η₂ : Y₂✝ ⟶ Z₂✝
⊢ (((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₁ X₂✝ ≫
          (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₁✝ X₂✝ Y₂✝ κ₂) ≫
        (fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) η₁ Y₂✝ ≫
          (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Z₁✝ Y₂✝ Z₂✝ η₂).hom =
    ((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) (κ₁ ≫ η₁) X₂✝ ≫
        (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Z₁✝ X₂✝ Z₂✝ (κ₂ ≫ η₂)).hom

Tactic:
;

Goal state after:
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η₁ : Y₁✝ ⟶ Z₁✝
η₂ : Y₂✝ ⟶ Z₂✝
⊢ (((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₁ X₂✝ ≫
          (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₁✝ X₂✝ Y₂✝ κ₂) ≫
        (fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) η₁ Y₂✝ ≫
          (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Z₁✝ Y₂✝ Z₂✝ η₂).hom =
    ((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) (κ₁ ≫ η₁) X₂✝ ≫
        (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Z₁✝ X₂✝ Z₂✝ (κ₂ ≫ η₂)).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ ({ hom := Kernel.id ∥ₖ κ.hom, property := ⋯ } ≫
        (let f₁ := fun x ↦ (PUnit.unit, x);
          have hf₁ := ⋯;
          have hf₂ := ⋯;
          { hom := { hom := Kernel.id.map Prod.snd, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom).hom =
    ((let f₁ := fun x ↦ (PUnit.unit, x);
          have hf₁ := ⋯;
          have hf₂ := ⋯;
          { hom := { hom := Kernel.id.map Prod.snd, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom ≫
        κ).hom

Tactic:
;

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ ({ hom := Kernel.id ∥ₖ κ.hom, property := ⋯ } ≫
        (let f₁ := fun x ↦ (PUnit.unit, x);
          have hf₁ := ⋯;
          have hf₂ := ⋯;
          { hom := { hom := Kernel.id.map Prod.snd, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom).hom =
    ((let f₁ := fun x ↦ (PUnit.unit, x);
          have hf₁ := ⋯;
          have hf₂ := ⋯;
          { hom := { hom := Kernel.id.map Prod.snd, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom ≫
        κ).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ ({ hom := κ.hom ∥ₖ Kernel.id, property := ⋯ } ≫
        (let f₁ := fun x ↦ (x, PUnit.unit);
          have hf₁ := ⋯;
          have hf₂ := ⋯;
          { hom := { hom := Kernel.id.map Prod.fst, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom).hom =
    ((let f₁ := fun x ↦ (x, PUnit.unit);
          have hf₁ := ⋯;
          have hf₂ := ⋯;
          { hom := { hom := Kernel.id.map Prod.fst, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom ≫
        κ).hom

Tactic:
;

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ ({ hom := κ.hom ∥ₖ Kernel.id, property := ⋯ } ≫
        (let f₁ := fun x ↦ (x, PUnit.unit);
          have hf₁ := ⋯;
          have hf₂ := ⋯;
          { hom := { hom := Kernel.id.map Prod.fst, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom).hom =
    ((let f₁ := fun x ↦ (x, PUnit.unit);
          have hf₁ := ⋯;
          have hf₂ := ⋯;
          { hom := { hom := Kernel.id.map Prod.fst, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom ≫
        κ).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: W X Y Z : SFinKer
⊢ ({
          hom :=
            { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
                    inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
                    inv_hom_id := ⋯ }.hom.hom ∥ₖ
              Kernel.id,
          property := ⋯ } ≫
        { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
              inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.hom ≫
          {
            hom :=
              Kernel.id ∥ₖ
                { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
                      inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
                      inv_hom_id := ⋯ }.hom.hom,
            property := ⋯ }).hom =
    ({ hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
            inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
            inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom).hom

Tactic:
;

Goal state after:
W X Y Z : SFinKer
⊢ ({
          hom :=
            { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
                    inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
                    inv_hom_id := ⋯ }.hom.hom ∥ₖ
              Kernel.id,
          property := ⋯ } ≫
        { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
              inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.hom ≫
          {
            hom :=
              Kernel.id ∥ₖ
                { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
                      inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
                      inv_hom_id := ⋯ }.hom.hom,
            property := ⋯ }).hom =
    ({ hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
            inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
            inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ ({ hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
            inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        {
          hom :=
            Kernel.id ∥ₖ
              (let f₁ := fun x ↦ (PUnit.unit, x);
                  have hf₁ := ⋯;
                  have hf₂ := ⋯;
                  { hom := { hom := Kernel.id.map Prod.snd, property := ⋯ },
                    inv := { hom := Kernel.id.map f₁, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom.hom,
          property := ⋯ }).hom =
    {
        hom :=
          (let f₁ := fun x ↦ (x, PUnit.unit);
                have hf₁ := ⋯;
                have hf₂ := ⋯;
                { hom := { hom := Kernel.id.map Prod.fst, property := ⋯ },
                  inv := { hom := Kernel.id.map f₁, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom.hom ∥ₖ
            Kernel.id,
        property := ⋯ }.hom

Tactic:
;

Goal state after:
X Y : SFinKer
⊢ ({ hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
            inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        {
          hom :=
            Kernel.id ∥ₖ
              (let f₁ := fun x ↦ (PUnit.unit, x);
                  have hf₁ := ⋯;
                  have hf₂ := ⋯;
                  { hom := { hom := Kernel.id.map Prod.snd, property := ⋯ },
                    inv := { hom := Kernel.id.map f₁, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom.hom,
          property := ⋯ }).hom =
    {
        hom :=
          (let f₁ := fun x ↦ (x, PUnit.unit);
                have hf₁ := ⋯;
                have hf₂ := ⋯;
                { hom := { hom := Kernel.id.map Prod.fst, property := ⋯ },
                  inv := { hom := Kernel.id.map f₁, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom.hom ∥ₖ
            Kernel.id,
        property := ⋯ }.hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic Prod.swap ⋯)

Tactic:
;

Goal state after:
X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic Prod.swap ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_1
X Y : SFinKer
⊢ ({ hom := Kernel.swap X.carrier Y.carrier, property := ⋯ } ≫
        { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }).hom =
    (𝟙 (X ⊗ Y)).hom

Tactic:
;

Goal state after:
case refine_1
X Y : SFinKer
⊢ ({ hom := Kernel.swap X.carrier Y.carrier, property := ⋯ } ≫
        { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }).hom =
    (𝟙 (X ⊗ Y)).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X Y : SFinKer
⊢ ({ hom := Kernel.swap Y.carrier X.carrier, property := ⋯ } ≫
        { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }).hom =
    (𝟙 (Y ⊗ X)).hom

Tactic:
;

Goal state after:
case refine_2
X Y : SFinKer
⊢ ({ hom := Kernel.swap Y.carrier X.carrier, property := ⋯ } ≫
        { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }).hom =
    (𝟙 (Y ⊗ X)).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
κ : Y ⟶ Z
⊢ (X ◁ κ ≫
        { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom).hom =
    ({ hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        κ ▷ X).hom

Tactic:
;

Goal state after:
X Y Z : SFinKer
κ : Y ⟶ Z
⊢ (X ◁ κ ≫
        { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom).hom =
    ({ hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        κ ▷ X).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
X : SFinKer
⊢ (κ ▷ X ≫
        { hom := { hom := Kernel.swap Y✝.carrier X.carrier, property := ⋯ },
            inv := { hom := Kernel.swap X.carrier Y✝.carrier, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom).hom =
    ({ hom := { hom := Kernel.swap X✝.carrier X.carrier, property := ⋯ },
            inv := { hom := Kernel.swap X.carrier X✝.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        X ◁ κ).hom

Tactic:
;

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
X : SFinKer
⊢ (κ ▷ X ≫
        { hom := { hom := Kernel.swap Y✝.carrier X.carrier, property := ⋯ },
            inv := { hom := Kernel.swap X.carrier Y✝.carrier, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom).hom =
    ({ hom := { hom := Kernel.swap X✝.carrier X.carrier, property := ⋯ },
            inv := { hom := Kernel.swap X.carrier X✝.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        X ◁ κ).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ ((α_ X Y Z).hom ≫
        { hom := { hom := Kernel.swap X.carrier (Y ⊗ Z).carrier, property := ⋯ },
              inv := { hom := Kernel.swap (Y ⊗ Z).carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.hom ≫
          (α_ Y Z X).hom).hom =
    ({ hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
              inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ▷
          Z ≫
        (α_ Y X Z).hom ≫
          Y ◁
            { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
                inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯,
                inv_hom_id := ⋯ }.hom).hom

Tactic:
;

Goal state after:
X Y Z : SFinKer
⊢ ((α_ X Y Z).hom ≫
        { hom := { hom := Kernel.swap X.carrier (Y ⊗ Z).carrier, property := ⋯ },
              inv := { hom := Kernel.swap (Y ⊗ Z).carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.hom ≫
          (α_ Y Z X).hom).hom =
    ({ hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
              inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ▷
          Z ≫
        (α_ Y X Z).hom ≫
          Y ◁
            { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
                inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯,
                inv_hom_id := ⋯ }.hom).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ (α_ X Y Z).hom ≫
      { hom := { hom := Kernel.swap X.carrier (Y ⊗ Z).carrier, property := ⋯ },
            inv := { hom := Kernel.swap (Y ⊗ Z).carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        (α_ Y Z X).hom =
    { hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ▷
        Z ≫
      (α_ Y X Z).hom ≫
        Y ◁
          { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
              inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom

Tactic:
ext : 1; dsimp
    simp only [Kernel.id, Kernel.swap]
    repeat rw [Kernel.deterministic_parallelComp_deterministic]
    repeat rw [Kernel.deterministic_comp_deterministic]
    rfl

Goal state after: