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

Goal state before:
pp: case inl
α : 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 δ
f : β → γ
g : γ → α
hg : Measurable g
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel 0

Tactic:
;

Goal state after:
case inl
α : 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 δ
f : β → γ
g : γ → α
hg : Measurable g
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel 0
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case inr
α : 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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
hg : Measurable g
h : IsMarkovKernel κ
this : IsMarkovKernel (κ.comap g hg)
⊢ IsZeroOrMarkovKernel (κ.comap g hg)

Tactic:
;

Goal state after:
case inr
α : 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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
hg : Measurable g
h : IsMarkovKernel κ
this : IsMarkovKernel (κ.comap g hg)
⊢ IsZeroOrMarkovKernel (κ.comap g hg)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
g : γ → α
κ : Kernel α β
f : δ → γ
hf : Measurable f
hg : Measurable g
a✝¹ : δ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.comap (g ∘ f) ⋯) a✝¹) s✝ = (((κ.comap g hg).comap f hf) a✝¹) s✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
g : γ → α
κ : Kernel α β
f : δ → γ
hf : Measurable f
hg : Measurable g
a✝¹ : δ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.comap (g ∘ f) ⋯) a✝¹) s✝ = (((κ.comap g hg).comap f hf) a✝¹) s✝
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 γ
x : α × β
s : Set γ
a✝ : MeasurableSet s
⊢ ((prodMkLeft α 0) x) s = (0 x) s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α × β
s : Set γ
a✝ : MeasurableSet s
⊢ ((prodMkLeft α 0) x) s = (0 x) s
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 γ
x : β × α
s : Set γ
a✝ : MeasurableSet s
⊢ ((prodMkRight α 0) x) s = (0 x) s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : β × α
s : Set γ
a✝ : MeasurableSet s
⊢ ((prodMkRight α 0) x) s = (0 x) s
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 γ
κ η : Kernel α β
a✝¹ : γ × α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((prodMkLeft γ (κ + η)) a✝¹) s✝ = ((prodMkLeft γ κ + prodMkLeft γ η) a✝¹) s✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
a✝¹ : γ × α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((prodMkLeft γ (κ + η)) a✝¹) s✝ = ((prodMkLeft γ κ + prodMkLeft γ η) a✝¹) s✝
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 γ
κ η : Kernel α β
a✝¹ : α × γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((prodMkRight γ (κ + η)) a✝¹) s✝ = ((prodMkRight γ κ + prodMkRight γ η) a✝¹) s✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
a✝¹ : α × γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((prodMkRight γ (κ + η)) a✝¹) s✝ = ((prodMkRight γ κ + prodMkRight γ η) a✝¹) s✝
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap Prod.snd ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap Prod.snd ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap Prod.fst ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap Prod.fst ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap Prod.snd ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap Prod.snd ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap Prod.fst ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap Prod.fst ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap Prod.snd ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap Prod.snd ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap Prod.fst ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap Prod.fst ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap Prod.snd ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap Prod.snd ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap Prod.fst ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap Prod.fst ⋯)
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
g : γ → α
hf : Measurable f
hg : Measurable g
a✝¹ : β
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((deterministic g hg ∘ₖ deterministic f hf) a✝¹) s✝ = ((deterministic (g ∘ f) ⋯) a✝¹) s✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
g : γ → α
hf : Measurable f
hg : Measurable g
a✝¹ : β
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((deterministic g hg ∘ₖ deterministic f hf) a✝¹) s✝ = ((deterministic (g ∘ f) ⋯) a✝¹) s✝
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap Prod.swap ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap Prod.swap ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap Prod.swap ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap Prod.swap ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap Prod.swap ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap Prod.swap ⋯)
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 γ
κ : Kernel α (β × γ)
a : α
s : Set (γ × β)
hs : MeasurableSet s
⊢ (κ a) (Prod.swap ⁻¹' s) = (κ a) {p | p.swap ∈ s}

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set (γ × β)
hs : MeasurableSet s
⊢ (κ a) (Prod.swap ⁻¹' s) = (κ a) {p | p.swap ∈ s}
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst✝ : IsSFiniteKernel κ
s : Set (Unit × β)
hs : MeasurableSet s
⊢ (dirac () ⊗ₘ κ) s = (map (Prod.mk ()) (κ ())) s

Tactic:
;

Goal state after:
β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst✝ : IsSFiniteKernel κ
s : Set (Unit × β)
hs : MeasurableSet s
⊢ (dirac () ⊗ₘ κ) s = (map (Prod.mk ()) (κ ())) s
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.swap)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.swap)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map Prod.swap)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map Prod.swap)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
⊢ SFinite ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
⊢ SFinite ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.map Prod.swap)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.map Prod.swap)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.map Prod.swap)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.map Prod.swap)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteMeasure ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteMeasure ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())
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 γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) (Prod.fst ⁻¹' s) = (κ a) {p | p.1 ∈ s}

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) (Prod.fst ⁻¹' s) = (κ a) {p | p.1 ∈ s}
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsMarkovKernel κ
⊢ IsProbabilityMeasure ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsMarkovKernel κ
⊢ IsProbabilityMeasure ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : ¬SFinite μ
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
;

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : ¬SFinite μ
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.fst)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.fst)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : ¬IsSFiniteKernel κ
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
;

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : ¬IsSFiniteKernel κ
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map Prod.fst)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map Prod.fst)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.map Prod.fst)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.map Prod.fst)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.map Prod.fst)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.map Prod.fst)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
;

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable fun x ↦ (f x, g x)
⊢ Measurable f

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable fun x ↦ (f x, g x)
⊢ Measurable f
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.snd)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.snd)