mathlib-initiative/mathlib-tactics huggingface dataset:
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 =
    (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 ≫
      κ

Tactic:
ext : 1

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.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndep m' hm' m μ ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (f i)) →
        μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']

Tactic:
rw [iCondIndep_iff_iCondIndepSets, iCondIndepSets_iff]
  · rfl
  · exact hm

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 =
    (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 ≫
      κ

Tactic:
ext : 1

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 := 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

Tactic:
ext : 1

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 :=
        (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 := ⋯ }

Tactic:
ext : 1

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: case refine_1
X Y : SFinKer
⊢ { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ } ≫
      { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ } =
    𝟙 (X ⊗ Y)

Tactic:
ext : 1

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 := ⋯ } =
    𝟙 (Y ⊗ X)

Tactic:
ext : 1

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 := Kernel.swap X.carrier Y.carrier, property := ⋯ },
          inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      κ ▷ X

Tactic:
ext : 1

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 := Kernel.swap X✝.carrier X.carrier, property := ⋯ },
          inv := { hom := Kernel.swap X.carrier X✝.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      X ◁ κ

Tactic:
ext : 1

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 := 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

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).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 =
    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

Tactic:
ext : 1

Goal state after:
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
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ { 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 ≫
      { 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 =
    𝟙 (X ⊗ Y)

Tactic:
ext : 1

Goal state after:
X Y : SFinKer
⊢ ({ 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 ≫
        { 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 =
    (𝟙 (X ⊗ Y)).hom
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 = (λ_ X).inv

Tactic:
ext : 1

Goal state after:
X : SFinKer
⊢ ({ hom := Kernel.copy X.carrier, property := ⋯ } ≫ { hom := Kernel.discard X.carrier, property := ⋯ } ▷ X).hom =
    (λ_ X).inv.hom
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 := ⋯ } = (ρ_ X).inv

Tactic:
ext : 1

Goal state after:
X : SFinKer
⊢ ({ hom := Kernel.copy X.carrier, property := ⋯ } ≫ X ◁ { hom := Kernel.discard X.carrier, property := ⋯ }).hom =
    (ρ_ X).inv.hom
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 := Kernel.copy X.carrier, property := ⋯ } ≫
      { hom := Kernel.copy X.carrier, property := ⋯ } ▷ X ≫ (α_ X X X).hom

Tactic:
ext : 1

Goal state after:
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
Module: Mathlib.Probability.Kernel.Category.SFinKer

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

Tactic:
ext : 1

Goal state after:
X : SFinKer
⊢ (Δ ≫ (β_ X X).hom).hom = Δ.hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Δ = (Δ ⊗ₘ Δ) ≫ MonoidalCategory.tensorμ X X Y Y

Tactic:
ext : 1

Goal state after:
X Y : SFinKer
⊢ Δ.hom = ((Δ ⊗ₘ Δ) ≫ MonoidalCategory.tensorμ X X Y Y).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

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

Tactic:
ext : 1

Goal state after:
X Y : SFinKer
⊢ ε.hom = ((ε ⊗ₘ ε) ≫ (λ_ (𝟙_ SFinKer)).hom).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

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

Tactic:
ext : 1

Goal state after:
⊢ Δ.hom = (λ_ (𝟙_ SFinKer)).inv.hom
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 := κ, property := ⋯ } ⊗ₘ { hom := κ, property := ⋯ })

Tactic:
ext : 1

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

Goal state before:
pp: Ω : 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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
⊢ Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map id (Measure.map (fun a ↦ (k a, g a, f a)) μ)

Tactic:
Measure.map_id

Goal state after:
Ω : 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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
⊢ Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (fun a ↦ (k a, g a, f a)) μ
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : 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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
⊢ ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map id (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)

Tactic:
Measure.map_id

Goal state after:
Ω : 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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
⊢ ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
t : ℝ
ω : Ω
hω : X ω = Y ω
⊢ rexp (t * Y ω) = rexp (t * X ω)

Tactic:
rw [hω]

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
ω' : Ω'
h : (κ ω') Set.univ ≤ 1
⊢ (κ ω') {ω | ε ≤ X ω} ≤ 1

Tactic:
exact (measure_mono (Set.subset_univ _)).trans h

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
x✝ : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
h : (ρ g) (ρ.asModuleEquiv w) ∈ N
⊢ (ρ g) w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }

Tactic:
exact h

Goal state after:
Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic

Goal state before:
pp: A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
a : A
w : V
hw : w ∈ (k ∙ v).carrier
t : k
ht : (algebraMap k (Module.End A V)) t = (Module.toModuleEnd A V) a
⊢ a • w ∈ (k ∙ v).carrier

Tactic:
simpa only [← show _ = a • w from congr($ht w)] using! (k ∙ v).smul_mem t hw

Goal state after: