-- Mathlib/Probability/Kernel/Composition/CompProd.lean
/-- If `η` is a Markov kernel, use instead `fst_compProd` to get `(κ ⊗ₖ η).fst = κ`. -/
lemma fst_compProd_apply (κ : Kernel α β) (η : Kernel (α × β) γ)
    [IsSFiniteKernel κ] [IsSFiniteKernel η] (x : α) {s : Set β} (hs : MeasurableSet s) :
    (κ ⊗ₖ η).fst x s = ∫⁻ b, s.indicator (fun b ↦ η (x, b) Set.univ) b ∂(κ x)

Proof state:
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}

Tactic:
exact measurable_fst hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (x, b)) {c | (b, c) ∈ {p | p.1 ∈ s}} ∂κ x =
    ∫⁻ (b : β), s.indicator (fun b => (η (x, b)) Set.univ) b ∂κ x

Tactic:
have h_eq b : η (x, b) {c | b ∈ s} = s.indicator (fun b ↦ η (x, b) Set.univ) b := by
  by_cases hb : b ∈ s <;> simp [hb]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
h_eq : ∀ (b : β), (η (x, b)) {c | b ∈ s} = s.indicator (fun b => (η (x, b)) Set.univ) b
⊢ ∫⁻ (b : β), (η (x, b)) {c | (b, c) ∈ {p | p.1 ∈ s}} ∂κ x =
    ∫⁻ (b : β), s.indicator (fun b => (η (x, b)) Set.univ) b ∂κ x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η).fst x) s = ∫⁻ (b : β), s.indicator (fun b => (η (x, b)) Set.univ) b ∂κ x

Tactic:
rw [Kernel.fst_apply' _ _ hs, Kernel.compProd_apply]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (x, b)) {c | (b, c) ∈ {p | p.1 ∈ s}} ∂κ x =
    ∫⁻ (b : β), s.indicator (fun b => (η (x, b)) Set.univ) b ∂κ x

case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
h_eq : ∀ (b : β), (η (x, b)) {c | b ∈ s} = s.indicator (fun b => (η (x, b)) Set.univ) b
⊢ ∫⁻ (b : β), (η (x, b)) {c | (b, c) ∈ {p | p.1 ∈ s}} ∂κ x =
    ∫⁻ (b : β), s.indicator (fun b => (η (x, b)) Set.univ) b ∂κ x

Tactic:
simp_rw [Set.mem_setOf_eq, h_eq]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (x, b)) {c | (b, c) ∈ {p | p.1 ∈ s}} ∂κ x =
    ∫⁻ (b : β), s.indicator (fun b => (η (x, b)) Set.univ) b ∂κ x

case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}

Tactic:
swap

Result:
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}

α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (x, b)) {c | (b, c) ∈ {p | p.1 ∈ s}} ∂κ x =
    ∫⁻ (b : β), s.indicator (fun b => (η (x, b)) Set.univ) b ∂κ x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
b : β
⊢ (η (x, b)) {c | b ∈ s} = s.indicator (fun b => (η (x, b)) Set.univ) b

Tactic:
by_cases hb : b ∈ s <;> simp [hb]

Result:
no goals