mathlib-initiative/mathlib-tactics huggingface dataset:
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:
dsimp

Goal state after:
case refine_1
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ = Kernel.id
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:
dsimp

Goal state after:
case refine_2
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc.symm ⋯ = Kernel.id
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:
dsimp

Goal state after:
case refine_1
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ Kernel.id.map f₁ ∘ₖ Kernel.id.map Prod.snd = Kernel.id
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:
dsimp

Goal state after:
case refine_2
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ Kernel.id.map Prod.snd ∘ₖ Kernel.id.map f₁ = Kernel.id
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:
dsimp

Goal state after:
case refine_1
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ Kernel.id.map f₁ ∘ₖ Kernel.id.map Prod.fst = Kernel.id
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:
dsimp

Goal state after:
case refine_2
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ Kernel.id.map Prod.fst ∘ₖ Kernel.id.map f₁ = Kernel.id
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:
dsimp

Goal state after:
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η₁ : Y₁✝ ⟶ Z₁✝
η₂ : Y₂✝ ⟶ Z₂✝
⊢ Kernel.id ∥ₖ η₂.hom ∘ₖ (η₁.hom ∥ₖ Kernel.id) ∘ₖ (Kernel.id ∥ₖ κ₂.hom ∘ₖ (κ₁.hom ∥ₖ Kernel.id)) =
    Kernel.id ∥ₖ (η₂.hom ∘ₖ κ₂.hom) ∘ₖ (η₁.hom ∘ₖ κ₁.hom ∥ₖ Kernel.id)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
⊢ (((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ })
            ((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₁ X₂✝ ≫
              (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₁✝ X₂✝ Y₂✝ κ₂)
            X₃✝ ≫
          (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ })
            { carrier := Y₁✝.carrier × Y₂✝.carrier, str := Prod.instMeasurableSpace } X₃✝ Y₃✝ η) ≫
        { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
            inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom).hom =
    ({ hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
            inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        (fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₁
            { carrier := X₂✝.carrier × X₃✝.carrier, str := Prod.instMeasurableSpace } ≫
          (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₁✝
            { carrier := X₂✝.carrier × X₃✝.carrier, str := Prod.instMeasurableSpace }
            { carrier := Y₂✝.carrier × Y₃✝.carrier, str := Prod.instMeasurableSpace }
            ((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₂ X₃✝ ≫
              (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₂✝ X₃✝ Y₃✝ η)).hom

Tactic:
dsimp

Goal state after:
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
⊢ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      (Kernel.id ∥ₖ η.hom ∘ₖ (Kernel.id ∥ₖ κ₂.hom ∘ₖ (κ₁.hom ∥ₖ Kernel.id) ∥ₖ Kernel.id)) =
    Kernel.id ∥ₖ (Kernel.id ∥ₖ η.hom ∘ₖ (κ₂.hom ∥ₖ Kernel.id)) ∘ₖ (κ₁.hom ∥ₖ Kernel.id) ∘ₖ
      Kernel.deterministic ⇑prodAssoc ⋯
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f' : ℕ → X → ℝ≥0∞
hf'_meas : ∀ (n : ℕ), Measurable (f' n)
hf'_mono : Monotone f'
hf' : ∀ (n : ℕ), ∫⁻ (x : X), B.indicator 1 x * f' n x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂π x₀
⊢ ∫⁻ (x : X), B.indicator 1 x * (fun x ↦ ⨆ n, f' n x) x ∂π x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), (fun x ↦ ⨆ n, f' n x) x ∂π x₀

Tactic:
simp_rw [ENNReal.mul_iSup]

Goal state after:
case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f' : ℕ → X → ℝ≥0∞
hf'_meas : ∀ (n : ℕ), Measurable (f' n)
hf'_mono : Monotone f'
hf' : ∀ (n : ℕ), ∫⁻ (x : X), B.indicator 1 x * f' n x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂π x₀
⊢ ∫⁻ (x : X), ⨆ i, B.indicator 1 x * f' i x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), ⨆ n, f' n x ∂π x₀
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:
dsimp

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ Kernel.id.map Prod.snd ∘ₖ (Kernel.id ∥ₖ κ.hom) = κ.hom ∘ₖ Kernel.id.map Prod.snd
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndep m' m₁ m₂ hm' μ ↔ CondIndepSets m' hm' {s | MeasurableSet s} {s | MeasurableSet s} μ

Tactic:
simp only [CondIndep, CondIndepSets, Kernel.Indep]

Goal state after:
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:
dsimp

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ Kernel.id.map Prod.fst ∘ₖ (κ.hom ∥ₖ Kernel.id) = κ.hom ∘ₖ Kernel.id.map Prod.fst
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:
dsimp

Goal state after:
W X Y Z : SFinKer
⊢ Kernel.id ∥ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic ⇑prodAssoc ⋯ ∥ₖ Kernel.id) =
    Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯
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:
dsimp

Goal state after:
X Y : SFinKer
⊢ Kernel.id ∥ₖ Kernel.id.map Prod.snd ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ = Kernel.id.map Prod.fst ∥ₖ Kernel.id
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:
dsimp

Goal state after:
X Y Z : SFinKer
κ : Y ⟶ Z
⊢ Kernel.swap X.carrier Z.carrier ∘ₖ (Kernel.id ∥ₖ κ.hom) = κ.hom ∥ₖ Kernel.id ∘ₖ Kernel.swap X.carrier Y.carrier
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:
dsimp

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
X : SFinKer
⊢ Kernel.swap Y✝.carrier X.carrier ∘ₖ (κ.hom ∥ₖ Kernel.id) = Kernel.id ∥ₖ κ.hom ∘ₖ Kernel.swap X✝.carrier X.carrier
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:
dsimp

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.swap X.carrier (Y.carrier × Z.carrier) ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.id ∥ₖ Kernel.swap X.carrier Z.carrier ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.swap X.carrier Y.carrier ∥ₖ Kernel.id)
Module: Mathlib.Probability.Kernel.Category.SFinKer

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

Tactic:
dsimp

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.swap (X.carrier × Y.carrier) Z.carrier ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.swap X.carrier Z.carrier ∥ₖ Kernel.id ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      (Kernel.id ∥ₖ Kernel.swap Y.carrier Z.carrier)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ ({ hom := Kernel.copy X.carrier, property := ⋯ } ≫ { hom := Kernel.discard X.carrier, property := ⋯ } ▷ X).hom =
    (λ_ X).inv.hom

Tactic:
dsimp

Goal state after:
X : SFinKer
⊢ Kernel.discard X.carrier ∥ₖ Kernel.id ∘ₖ Kernel.copy X.carrier = Kernel.id.map fun x ↦ (PUnit.unit, x)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ ({ hom := Kernel.copy X.carrier, property := ⋯ } ≫ X ◁ { hom := Kernel.discard X.carrier, property := ⋯ }).hom =
    (ρ_ X).inv.hom

Tactic:
dsimp

Goal state after:
X : SFinKer
⊢ Kernel.id ∥ₖ Kernel.discard X.carrier ∘ₖ Kernel.copy X.carrier = Kernel.id.map fun x ↦ (x, PUnit.unit)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ ({ hom := Kernel.copy X.carrier, property := ⋯ } ≫ X ◁ { hom := Kernel.copy X.carrier, property := ⋯ }).hom =
    ({ hom := Kernel.copy X.carrier, property := ⋯ } ≫
        { hom := Kernel.copy X.carrier, property := ⋯ } ▷ X ≫ (α_ X X X).hom).hom

Tactic:
dsimp

Goal state after:
X : SFinKer
⊢ Kernel.id ∥ₖ Kernel.copy X.carrier ∘ₖ Kernel.copy X.carrier =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ (Kernel.copy X.carrier ∥ₖ Kernel.id) ∘ₖ Kernel.copy X.carrier
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ (Δ ≫ (β_ X X).hom).hom = Δ.hom

Tactic:
dsimp

Goal state after:
X : SFinKer
⊢ Kernel.swap X.carrier X.carrier ∘ₖ Kernel.copy X.carrier = Kernel.copy X.carrier
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case e'_2
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun ω ↦ (f ω, g ω)) = Measure.map (fun ω ↦ (ω, f ω, g ω)) μ

Tactic:
rw [Measure.compProd_map (by fun_prop), compProd_trim_condExpKernel]
    exact Measure.map_map (by fun_prop) ((measurable_id.mono le_rfl hm').prodMk measurable_id)

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ ε.hom = ((ε ⊗ₘ ε) ≫ (λ_ (𝟙_ SFinKer)).hom).hom

Tactic:
dsimp

Goal state after:
X Y : SFinKer
⊢ Kernel.discard (X.carrier × Y.carrier) =
    Kernel.id.map Prod.snd ∘ₖ (Kernel.id ∥ₖ Kernel.discard Y.carrier ∘ₖ (Kernel.discard X.carrier ∥ₖ Kernel.id))
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: ⊢ Δ.hom = (λ_ (𝟙_ SFinKer)).inv.hom

Tactic:
dsimp

Goal state after:
⊢ Kernel.copy PUnit.{u + 1} = Kernel.id.map fun x ↦ (PUnit.unit, x)
Module: Mathlib.Probability.Kernel.Category.SFinKer

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

Tactic:
dsimp

Goal state after:
X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst✝¹ : IsDeterministic κ
inst✝ : IsMarkovKernel κ
⊢ Kernel.copy Y.carrier ∘ₖ κ = Kernel.id ∥ₖ κ ∘ₖ (κ ∥ₖ Kernel.id) ∘ₖ Kernel.copy X.carrier
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] =ᵐ[μ] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
refine ae_of_ae_restrict_of_ae_restrict_compl {x | σ x ≤ τ x} ?_ ?_

Goal state after:
case refine_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x | σ x ≤ τ x},
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

case refine_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x | σ x ≤ τ x}ᶜ,
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case e'_2
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u)
h_right :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u) =
            (⇑(Kernel.id ×ₖ
                    ((condExpKernel μ (MeasurableSpace.comap k mγ)).map f ×ₖ
                      (condExpKernel μ (MeasurableSpace.comap k mγ)).map g)) ∘ₘ
                μ.trim ⋯)
              ((k ⁻¹' s) ×ˢ t ×ˢ u)
h :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u)
t : Set β
u : Set β'
s : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u) =
    (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u)

Tactic:
exact (h_left hs ht hu).symm

Goal state after: