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 γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ (κ a) {p | p.swap ∈ {p | p.1 ∈ s}} = (κ a) (Prod.snd ⁻¹' s)

pp: case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {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) {p | p.swap ∈ {p | p.1 ∈ s}} = (κ a) (Prod.snd ⁻¹' s)

case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}
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 γ
μ : Measure β
inst✝¹ : SFinite μ
ν : Measure γ
inst✝ : SFinite ν
x : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ (μ.prod ν) s✝ = (μ.prod ν) s✝

Tactic:
]

Goal state after:
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κη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (fun a ↦ (η a) (Prod.mk a ⁻¹' s)) =ᵐ[μ] 0
⊢ (fun a ↦ (κ a) (Prod.mk a ⁻¹' s)) =ᵐ[μ] 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (fun a ↦ (η a) (Prod.mk a ⁻¹' s)) =ᵐ[μ] 0
⊢ (fun a ↦ (κ a) (Prod.mk a ⁻¹' s)) =ᵐ[μ] 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
⊢ (((η ∥ₖ Kernel.id) (MeasurableEquiv.prodAssoc.symm (((a, a).1, b).1, ((a, a).1, b).2, ((a, a).1, b).2))).bind
        ⇑(swap γ β))
      s =
    (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
]

Goal state after:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
⊢ (((η ∥ₖ Kernel.id) (MeasurableEquiv.prodAssoc.symm (((a, a).1, b).1, ((a, a).1, b).2, ((a, a).1, b).2))).bind
        ⇑(swap γ β))
      s =
    (η (a, b)) (Prod.mk b ⁻¹' 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 β
hs : MeasurableSet s
⊢ (κ a) {p | p.swap ∈ Prod.snd ⁻¹' s} = (κ a) {p | p.1 ∈ s}

pp: case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' 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) {p | p.swap ∈ Prod.snd ⁻¹' s} = (κ a) {p | p.1 ∈ s}

case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)
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✝ : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η) (a, a) = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ 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✝ : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η) (a, a) = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap (fun a ↦ (a, b)) ⋯)

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 (α × β) γ
b : β
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap (fun a ↦ (a, b)) ⋯)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
⊢ ∫⁻ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac ((a, b), b).2 ∂η ((a, b), b).1 =
    (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
]

Goal state after:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
⊢ ∫⁻ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac ((a, b), b).2 ∂η ((a, b), b).1 =
    (η (a, b)) (Prod.mk b ⁻¹' 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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap (fun a ↦ (a, b)) ⋯)

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 (α × β) γ
b : β
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap (fun a ↦ (a, b)) ⋯)
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap (fun a ↦ (a, b)) ⋯)

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 (α × β) γ
b : β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap (fun a ↦ (a, b)) ⋯)
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✝ : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (y : γ), ∫⁻ (x : β), g (x, y) ∂κ a ∂η a = ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂κ a ∂η a

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 α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
x : γ
⊢ ((swap γ β) (x, b)) s = (Prod.mk b ⁻¹' s).indicator 1 x

pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
x : γ
⊢ Measurable fun y ↦ ((swap γ β) (x, y)) s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
x : γ
⊢ ((swap γ β) (x, b)) s = (Prod.mk b ⁻¹' s).indicator 1 x

case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
x : γ
⊢ Measurable fun y ↦ ((swap γ β) (x, y)) 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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap (fun a ↦ (a, b)) ⋯)

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 (α × β) γ
b : β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap (fun a ↦ (a, b)) ⋯)
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
b : β
inst✝ : NeZero (κ (a, b))
⊢ NeZero (κ (a, b))

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 (α × β) γ
a : α
b : β
inst✝ : NeZero (κ (a, b))
⊢ NeZero (κ (a, b))
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 γ
f : α → β
hf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (y : γ), g (f a, y) ∂κ a = ∫⁻ (c : γ), g (f a, c) ∂κ a

Tactic:
]

Goal state after:
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_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : IsSFiniteKernel η
⊢ ∫⁻ (a : α) in s, (η a) univ ∂ν = 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : IsSFiniteKernel η
⊢ ∫⁻ (a : α) in s, (η a) univ ∂ν = 0
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : ∀ (b : β), IsMarkovKernel (κ.sectL b)
x✝ : α × β
⊢ 1 = 1

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 γ
f : α → γ
hf : Measurable f
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (x : β), g (x, f a) ∂κ a = ∫⁻ (b : β), g (b, f a) ∂κ a

Tactic:
]

Goal state after:
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 δ
κ : Kernel (α × β) γ
b : β
f : δ → α
hf : Measurable f
d : δ
s : Set γ
a✝ : MeasurableSet s
⊢ (κ (f d, b)) s = (κ (f d, b)) s

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✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (fun a ↦ (κ a) univ) =ᵐ[μ.restrict s] 0
⊢ μ s = 0

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : ∫⁻ (a : α) in s, (κ a) univ ∂μ = 0
⊢ Measurable fun a ↦ (κ a) univ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (fun a ↦ (κ a) univ) =ᵐ[μ.restrict s] 0
⊢ μ s = 0

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : ∫⁻ (a : α) in s, (κ a) univ ∂μ = 0
⊢ Measurable fun a ↦ (κ a) univ
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap (fun b ↦ (a, b)) ⋯)

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 (α × β) γ
a : α
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap (fun b ↦ (a, b)) ⋯)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
h_int : ∀ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x
⊢ (η (a, b)) (Prod.mk b ⁻¹' s) = (η (a, b)) (Prod.mk b ⁻¹' s)

pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
h_int : ∀ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x
⊢ MeasurableSet (Prod.mk b ⁻¹' s)

Tactic:
]

Goal state after:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
h_int : ∀ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x
⊢ MeasurableSet (Prod.mk b ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a : α
⊢ ∫⁻ (c : β), f (a, c) ∂κ a = ∫⁻ (b : β), f (a, b) ∂κ a

Tactic:
]

Goal state after:
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap (fun b ↦ (a, b)) ⋯)

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 (α × β) γ
a : α
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap (fun b ↦ (a, b)) ⋯)
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap (fun b ↦ (a, b)) ⋯)

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 (α × β) γ
a : α
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap (fun b ↦ (a, b)) ⋯)
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel β α
inst✝ : IsSFiniteKernel κ
b : β
⊢ ∫⁻ (b_1 : α), f (b_1, b) ∂κ b = ∫⁻ (a : α), f (a, b) ∂κ b

Tactic:
]

Goal state after:
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap (fun b ↦ (a, b)) ⋯)

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 (α × β) γ
a : α
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap (fun b ↦ (a, b)) ⋯)
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✝ : IsMarkovKernel η
a : α
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' Set.univ) ∂κ a = (κ a) Set.univ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
a : α
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' Set.univ) ∂κ a = (κ a) Set.univ
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 γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ (κ a) (Prod.mk (f a) ⁻¹' s) = (κ a) (Prod.mk (f a) ⁻¹' s)

pp: case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Measurable fun b ↦ (κ a) (Prod.mk b ⁻¹' s)

Tactic:
]

Goal state after:
case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Measurable fun b ↦ (κ a) (Prod.mk b ⁻¹' 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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : ∀ (b : α), IsMarkovKernel (κ.sectR b)
x✝ : α × β
⊢ 1 = 1

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 γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s ×ˢ t) ∂κ a = ∫⁻ (a_1 : β), s.indicator (fun b ↦ (η (a, b)) t) a_1 ∂κ a

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s ×ˢ t) ∂κ a = ∫⁻ (a_1 : β), s.indicator (fun b ↦ (η (a, b)) t) a_1 ∂κ a
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a : α
s : Set (α × β)
hs : MeasurableSet s
⊢ (κ a) (Prod.mk a ⁻¹' s) = (κ a) (Prod.mk a ⁻¹' s)

Tactic:
]

Goal state after:
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 δ
κ : Kernel (α × β) γ
a : α
f : δ → β
hf : Measurable f
d : δ
s : Set γ
a✝ : MeasurableSet s
⊢ (κ (a, f d)) s = (κ (a, f d)) s

Tactic:
]

Goal state after:
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✝¹ : IsMarkovKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ IsMarkovKernel (κ ∥ₖ η ∘ₖ 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✝¹ : IsMarkovKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ IsMarkovKernel (κ ∥ₖ η ∘ₖ copy α)
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 (prodMkLeft γ κ)
⊢ IsSFiniteKernel ((prodMkLeft γ κ).sectR 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 (prodMkLeft γ κ)
⊢ IsSFiniteKernel ((prodMkLeft γ κ).sectR default)