mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case inr
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv : ∀ (k M n : ℕ), a n ≤ M → lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n)
anti_lma : ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x
k : ℕ
x : (n : ℕ) → X n
h : ∃ l, Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 l)
⊢ ∃ l, Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 l)

Tactic:
exact h

Goal state after:
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ : Kernel α γ
inst✝ : IsFiniteKernel κ
⊢ κ.singularPart κ = 0

Tactic:
ext : 1

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ : Kernel α γ
inst✝ : IsFiniteKernel κ
a✝ : α
⊢ (κ.singularPart κ) a✝ = 0 a✝
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 : ∀ (a : α), (η a) (Prod.mk a ⁻¹' s) = 0
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (Prod.mk a ⁻¹' s)ᶜ = 0

Tactic:
filter_upwards [hκη] with a ha

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 : ∀ (a : α), (η a) (Prod.mk a ⁻¹' s) = 0
a : α
ha : κ a ⟂ₘ η a
⊢ (κ a) (Prod.mk a ⁻¹' s)ᶜ = 0
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a✝ : ∀ (a : α), IsZeroOneMeasure (κ a)
⊢ κ ∥ₖ κ ∘ₖ copy α = copy β ∘ₖ κ

Tactic:
ext : 1

Goal state after:
case mpr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a✝¹ : ∀ (a : α), IsZeroOneMeasure (κ a)
a✝ : α
⊢ (κ ∥ₖ κ ∘ₖ copy α) a✝ = (copy β ∘ₖ κ) a✝
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsMarkovKernel κ
this : ⇑κ =ᵐ[μ] ⇑((κ†μ)†(⇑κ ∘ₘ μ))
⊢ ⇑((κ†μ)†(⇑κ ∘ₘ μ)) =ᵐ[μ] ⇑κ

Tactic:
filter_upwards [this] with a h using h.symm

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (y : 𝓧) in t, ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ ∂⇑κ ∘ₘ μ =
    (⇑(Kernel.swap 𝓧 Ω) ∘ₘ (⇑κ ∘ₘ μ) ⊗ₘ κ†μ) (s ×ˢ t)

Tactic:
Measure.swap_comp,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (y : 𝓧) in t, ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ ∂⇑κ ∘ₘ μ =
    (Measure.map Prod.swap ((⇑κ ∘ₘ μ) ⊗ₘ κ†μ)) (s ×ˢ t)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
⊢ map (⇑(piCurry X)) (infinitePi fun p ↦ μ p.fst p.snd) = infinitePi fun i ↦ infinitePi fun j ↦ μ i j

Tactic:
MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq,

Goal state after:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
⊢ (infinitePi fun p ↦ μ p.fst p.snd) = map (⇑(piCurry X).symm) (infinitePi fun i ↦ infinitePi fun j ↦ μ i j)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ map (⇑(MeasurableEquiv.curry ι κ X)) (infinitePi fun p ↦ μ p.1 p.2) = infinitePi fun i ↦ infinitePi fun j ↦ μ i j

Tactic:
MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq,

Goal state after:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ (infinitePi fun p ↦ μ p.1 p.2) =
    map (⇑(MeasurableEquiv.curry ι κ X).symm) (infinitePi fun i ↦ infinitePi fun j ↦ μ i j)
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝¹ : Subsingleton 𝓧
inst✝ : Nonempty 𝓨
⊢ bayesRisk ℓ P π = ⨅ μ, ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π

Tactic:
rcases isEmpty_or_nonempty 𝓧 with hX | hX
  · simp [iInf_subtype']
  obtain x := hX.some
  rw [bayesRisk, iInf_subtype', iInf_subtype']
  let e : {κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ} ≃ {μ : Measure 𝓨 // IsProbabilityMeasure μ} :=
    { toFun κ := ⟨κ.1 x, κ.2.isProbabilityMeasure x⟩
      invFun μ := ⟨Kernel.const 𝓧 μ, ⟨fun _ ↦ μ.2⟩⟩
      left_inv κ := by ext y; simp only [Kernel.const_apply, Subsingleton.elim x y]
      right_inv μ := by simp }
  rw [← Equiv.iInf_comp e.symm]
  rfl

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝¹ : IsSFiniteKernel P
π : Measure Θ
η : Kernel (Θ × 𝓧) 𝓧'
inst✝ : IsMarkovKernel η
this : P = Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)
⊢ bayesRisk ℓ (P ⊗ₖ η) π ≤ bayesRisk ℓ P π

Tactic:
nth_rw 2 [this]

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝¹ : IsSFiniteKernel P
π : Measure Θ
η : Kernel (Θ × 𝓧) 𝓧'
inst✝ : IsMarkovKernel η
this : P = Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)
⊢ bayesRisk ℓ (P ⊗ₖ η) π ≤ bayesRisk ℓ (Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)) π
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ μ.toPMF.toMeasure s = μ s

Tactic:
rw [μ.toPMF.toMeasure_apply hs, ← μ.tsum_indicator_apply_singleton s hs]

Goal state after:
α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), s.indicator (⇑μ.toPMF) x = ∑' (x : α), s.indicator (fun x ↦ μ {x}) x
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
⊢ (map (s.restrict ∘ fun ω i ↦ X i ω) P) (Set.univ.pi fun i ↦ t ↑i) = ∏ i ∈ s, (map (X i) P) (t i)

Tactic:
have : s.restrict ∘ (fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω := by ext; simp

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝¹ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this✝ : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ (map (s.restrict ∘ fun ω i ↦ X i ω) P) (Set.univ.pi fun i ↦ t ↑i) = ∏ i ∈ s, (map (X i) P) (t i)
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ map (fun ω i ↦ s.restrict X i ω) P = Measure.pi fun i ↦ map (s.restrict X i) P

Tactic:
have : s.restrict ∘ (fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω := by ext; simp

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ map (fun ω i ↦ s.restrict X i ω) P = Measure.pi fun i ↦ map (s.restrict X i) P
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h✝ : Nonempty Ω
h : (fun a ↦ ((condDistrib id id μ) a).real s) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m ⊓ mΩ]
⊢ (fun ω ↦ ((condDistrib id id μ) (id ω)).real s) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m ⊓ mΩ]

Tactic:
exact h

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

Goal state before:
pp: X Y : Stoch
κ : X ⟶ Y
⊢ ε ≫ Δ = Δ ≫ (ε ⊗ₘ ε)

Tactic:
ext : 1

Goal state after:
X Y : Stoch
κ : X ⟶ Y
⊢ (ε ≫ Δ).hom = (Δ ≫ (ε ⊗ₘ ε)).hom
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 := κ, property := ⋯ }, property := ⋯ } ⊗ₘ { hom := { hom := κ, property := ⋯ }, property := ⋯ })

Tactic:
ext : 1

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.SFinKer

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

Tactic:
ext : 1

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 := ⋯ } =
    𝟙
      { carrier := X.carrier × { carrier := Y.carrier × Z.carrier, str := Prod.instMeasurableSpace }.carrier,
        str := Prod.instMeasurableSpace }

Tactic:
ext : 1

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 := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ { hom := Kernel.id.map Prod.snd, property := ⋯ } ≫ { hom := Kernel.id.map f₁, property := ⋯ } =
    𝟙
      { carrier := { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier × X.carrier,
        str := Prod.instMeasurableSpace }

Tactic:
ext : 1

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_1
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ Kernel.deterministic (f₁ ∘ Prod.snd) ⋯ = Kernel.id

Tactic:
ext : 1

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
a✝ : PUnit.{u + 1} × X.carrier
⊢ (Kernel.deterministic (f₁ ∘ Prod.snd) ⋯) a✝ = Kernel.id a✝
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: 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
⊢ { hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.snd, property := ⋯ } = 𝟙 X

Tactic:
ext : 1

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.Category.SFinKer

Goal state before:
pp: 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.deterministic (Prod.snd ∘ f₁) ⋯ = Kernel.id

Tactic:
ext : 1

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
a✝ : X.carrier
⊢ (Kernel.deterministic (Prod.snd ∘ f₁) ⋯) a✝ = Kernel.id a✝
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: 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
⊢ { hom := Kernel.id.map Prod.fst, property := ⋯ } ≫ { hom := Kernel.id.map f₁, property := ⋯ } =
    𝟙
      { carrier := X.carrier × { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier,
        str := Prod.instMeasurableSpace }

Tactic:
ext : 1

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_1
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ Kernel.deterministic (f₁ ∘ Prod.fst) ⋯ = Kernel.id

Tactic:
ext : 1

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
a✝ : X.carrier × PUnit.{u + 1}
⊢ (Kernel.deterministic (f₁ ∘ Prod.fst) ⋯) a✝ = Kernel.id a✝
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: 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
⊢ { hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.fst, property := ⋯ } = 𝟙 X

Tactic:
ext : 1

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: 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.deterministic (Prod.fst ∘ f₁) ⋯ = Kernel.id

Tactic:
ext : 1

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
a✝ : X.carrier
⊢ (Kernel.deterministic (Prod.fst ∘ f₁) ⋯) a✝ = Kernel.id a✝
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₂✝ η₂ =
    (fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) (κ₁ ≫ η₁) X₂✝ ≫
      (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Z₁✝ X₂✝ Z₂✝ (κ₂ ≫ η₂)

Tactic:
ext : 1

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₁✝ 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 := 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₃✝ η)

Tactic:
ext : 1

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