mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
h : IsSFiniteKernel (prodMkRight γ κ)
⊢ IsSFiniteKernel ((prodMkRight γ κ).sectL default)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
h : IsSFiniteKernel (prodMkRight γ κ)
⊢ IsSFiniteKernel ((prodMkRight γ κ).sectL default)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ 0 ≪ ν ⊗ₘ η

Tactic:
]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ 0 ≪ ν ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

Tactic:
rw [compProd_of_not_sfinite _ _ hμ]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ 0 ≪ ν ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : IsSFiniteKernel η'
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = ((κ ⊗ₖ η') a) s

Tactic:
compProd_apply hs

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : IsSFiniteKernel η'
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = ∫⁻ (b : β), (η' (a, b)) (Prod.mk b ⁻¹' s) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : IsSFiniteKernel η'
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = ∫⁻ (b : β), (η' (a, b)) (Prod.mk b ⁻¹' s) ∂κ a

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : IsSFiniteKernel η'
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = ∫⁻ (b : β), (η' (a, b)) (Prod.mk b ⁻¹' s) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : ∀ᵐ (a : α) ∂ν, ∀ᵐ (b : β) ∂η a, (a, b) ∉ s
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂η a, (a, b) ∉ s

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : ∀ᵐ (a : α) ∂ν, ∀ᵐ (b : β) ∂η a, (a, b) ∉ s
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂η a, (a, b) ∉ s
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
η : Kernel Y Z
inst✝¹ : IsSFiniteKernel η
κ : Kernel X Y
inst✝ : IsSFiniteKernel κ
a : X
s : Set Z
hs : MeasurableSet s
⊢ ∫⁻ (b : Y), (η b) s ∂κ a = ∫⁻ (b : Y), ((prodMkLeft X η) (a, b)) (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂κ a

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
η : Kernel Y Z
inst✝¹ : IsSFiniteKernel η
κ : Kernel X Y
inst✝ : IsSFiniteKernel κ
a : X
s : Set Z
hs : MeasurableSet s
⊢ ∫⁻ (b : Y), (η b) s ∂κ a = ∫⁻ (b : Y), ((prodMkLeft X η) (a, b)) (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
⊢ ∫⁻ (b : Y), ((prodMkLeft X η) (a, b)) (Prod.mk b ⁻¹' s) ∂κ a =
    ∫⁻ (b : Y), ((prodMkLeft X (Kernel.id ×ₖ η)) (a, b)) (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂κ a

pp: case hs
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
⊢ ∫⁻ (b : Y), ((prodMkLeft X η) (a, b)) (Prod.mk b ⁻¹' s) ∂κ a =
    ∫⁻ (b : Y), ((prodMkLeft X (Kernel.id ×ₖ η)) (a, b)) (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂κ a

case hs
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case e_f
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
b : Y
⊢ (η b) (Prod.mk b ⁻¹' s) = (η b) (Prod.mk b ⁻¹' s)

pp: case e_f.hf
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
b : Y
⊢ Measurable fun b_1 ↦ (η b) (Prod.mk b_1 ⁻¹' s)

Tactic:
]

Goal state after:
case e_f.hf
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
b : Y
⊢ Measurable fun b_1 ↦ (η b) (Prod.mk b_1 ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsFiniteKernel κ
η : Kernel α γ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (κ ∥ₖ η ∘ₖ copy α)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsFiniteKernel κ
η : Kernel α γ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (κ ∥ₖ η ∘ₖ copy α)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : ¬SFinite μ
⊢ 0 ⟂ₘ ν ⊗ₘ η

Tactic:
]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : ¬SFinite μ
⊢ 0 ⟂ₘ ν ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : ¬SFinite μ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
rw [compProd_of_not_sfinite _ _ hμ]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : ¬SFinite μ
⊢ 0 ⟂ₘ ν ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel α γ
⊢ IsSFiniteKernel (κ ∥ₖ η ∘ₖ copy α)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel α γ
⊢ IsSFiniteKernel (κ ∥ₖ η ∘ₖ copy α)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : ¬SFinite ν
⊢ μ ⊗ₘ κ ⟂ₘ 0

Tactic:
]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : ¬SFinite ν
⊢ μ ⊗ₘ κ ⟂ₘ 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : IsSFiniteKernel η'
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
b : β
hb : η (a, b) = η' (a, b)
⊢ (η' (a, b)) (Prod.mk b ⁻¹' s) = (η' (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : ¬IsSFiniteKernel κ
⊢ 0 ⟂ₘ ν ⊗ₘ η

Tactic:
]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : ¬IsSFiniteKernel κ
⊢ 0 ⟂ₘ ν ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ (κ ∥ₖ η).fst ∘ₖ copy α = κ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ (κ ∥ₖ η).fst ∘ₖ copy α = κ
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (κ (a, b)) (Prod.mk b ⁻¹' s) ∂0 a = (0 a) s

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (κ (a, b)) (Prod.mk b ⁻¹' s) ∂0 a = (0 a) s
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ μ ⊗ₘ κ ⟂ₘ 0

Tactic:
]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ μ ⊗ₘ κ ⟂ₘ 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : ¬IsSFiniteKernel κ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (0 (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = (0 a) s

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (0 (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = (0 a) s
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
h : ¬IsSFiniteKernel κ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
a : α
⊢ Measure.map Prod.fst ((κ (a, a).1).prod (η (a, a).2)) = κ a

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
a : α
⊢ Measure.map Prod.fst ((κ (a, a).1).prod (η (a, a).2)) = κ a
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ ∫⁻ (a : α) in hμν.nullSet, (κ a) univ ∂μ = 0 ∧ (ν ⊗ₘ η) (hμν.nullSetᶜ ×ˢ univ ∪ univ ×ˢ univᶜ) = 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ ∫⁻ (a : α) in hμν.nullSet, (κ a) univ ∂μ = 0 ∧ (ν ⊗ₘ η) (hμν.nullSetᶜ ×ˢ univ ∪ univ ×ˢ univᶜ) = 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ (0 a) (Set.univ ×ˢ Set.univ) = 0

Tactic:
]

Goal state after:
case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ (0 a) (Set.univ ×ˢ Set.univ) = 0
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ ∫⁻ (a : α) in hμν.nullSetᶜ, (η a) univ ∂ν = 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ ∫⁻ (a : α) in hμν.nullSetᶜ, (η a) univ ∂ν = 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0
⊢ κ ⊗ₖ η = κ ⊗ₖ 0

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0
⊢ κ ⊗ₖ η = κ ⊗ₖ 0
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ ∫⁻ (y : T), ∫⁻ (x : Y), (Measure.dirac (x, y).swap) s ∂κ ac.1 ∂η ac.2 = ∫⁻ (b : T), (κ ac.1) (Prod.mk b ⁻¹' s) ∂η ac.2

pp: case pos.hf
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ AEMeasurable (fun a ↦ (Measure.dirac a.swap) s) ((κ ac.1).prod (η ac.2))

Tactic:
]

Goal state after:
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ ∫⁻ (y : T), ∫⁻ (x : Y), (Measure.dirac (x, y).swap) s ∂κ ac.1 ∂η ac.2 = ∫⁻ (b : T), (κ ac.1) (Prod.mk b ⁻¹' s) ∂η ac.2

case pos.hf
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ AEMeasurable (fun a ↦ (Measure.dirac a.swap) s) ((κ ac.1).prod (η ac.2))
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
η : Kernel β δ
inst✝ : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
⊢ (κ (f x)).prod (η (f x)) = (κ (f x)).prod (η (f x))

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
this : ∀ (b : β), (η (x, b)) {_c | b ∈ s} = s.indicator (fun x ↦ 1) b
⊢ (κ x) s = (κ x) s

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
⊢ ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂κ x +
      ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂κ x =
    (κ x) {b | (b, f (x, b)) ∈ s}

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
⊢ ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂κ x +
      ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂κ x =
    (κ x) {b | (b, f (x, b)) ∈ s}
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0
hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0
⊢ MeasurableSet h.nullSet

Tactic:
exact hs

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
this : ∀ b ∈ tᶜ, (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α δ
inst✝ : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
⊢ (Measure.map f (κ x)).prod (Measure.map g (η x)) = (Measure.map f (κ x)).prod (Measure.map g (η x))

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) = 0
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
⊢ ∫⁻ (x : Y), ∫⁻ (y : Z), ((Kernel.id ∥ₖ ξ) (x, y)) s ∂η a.2 ∂κ a.1 = ((κ ∥ₖ (ξ ∘ₖ η)) a) s

Tactic:
]

Goal state after:
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
⊢ ∫⁻ (x : Y), ∫⁻ (y : Z), ((Kernel.id ∥ₖ ξ) (x, y)) s ∂η a.2 ∂κ a.1 = ((κ ∥ₖ (ξ ∘ₖ η)) a) s