-- Mathlib/Probability/Kernel/Composition/CompProd.lean
lemma compProd_preimage_fst {s : Set β} (hs : MeasurableSet s) (κ : Kernel α β)
    (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsMarkovKernel η] (x : α) :
    (κ ⊗ₖ η) x (Prod.fst ⁻¹' s) = κ x s

Proof state:
α : 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 : α
⊢ ∫⁻ (b : β), (η (x, b)) {c | b ∈ s} ∂κ x = (κ x) s

Tactic:
have : ∀ b : β, η (x, b) {_c | b ∈ s} = s.indicator (fun _ ↦ 1) b := by
  intro b
  by_cases hb : b ∈ s <;> simp [hb]

Result:
α : 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
⊢ ∫⁻ (b : β), (η (x, b)) {c | b ∈ s} ∂κ x = (κ x) s

Proof state:
α : 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 : α
⊢ ∀ (b : β), (η (x, b)) {_c | b ∈ s} = s.indicator (fun x => 1) b

Tactic:
intro b

Result:
α : 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 : α
b : β
⊢ (η (x, b)) {_c | b ∈ s} = s.indicator (fun x => 1) b

Proof state:
α : 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
⊢ ∫⁻ (b : β), (η (x, b)) {c | b ∈ s} ∂κ x = (κ x) s

Tactic:
simp_rw [this]

Result:
α : 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
⊢ ∫⁻ (b : β), s.indicator (fun x => 1) b ∂κ x = (κ x) s

Proof state:
α : 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 : α
⊢ ((κ ⊗ₖ η) x) (Prod.fst ⁻¹' s) = (κ x) s

Tactic:
rw [compProd_apply (measurable_fst hs)]

Result:
α : 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 : α
⊢ ∫⁻ (b : β), (η (x, b)) {c | (b, c) ∈ Prod.fst ⁻¹' s} ∂κ x = (κ x) s

Proof state:
α : 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 : α
⊢ ∫⁻ (b : β), (η (x, b)) {c | b ∈ s} ∂κ x = (κ x) s

Tactic:
classical
have : ∀ b : β, η (x, b) {_c | b ∈ s} = s.indicator (fun _ ↦ 1) b := by
  intro b
  by_cases hb : b ∈ s <;> simp [hb]
simp_rw [this]
rw [lintegral_indicator_const hs, one_mul]

Result:
no goals

Proof state:
α : 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 : α
⊢ ∫⁻ (b : β), (η (x, b)) {c | (b, c) ∈ Prod.fst ⁻¹' s} ∂κ x = (κ x) s

Tactic:
simp only [Set.mem_preimage]

Result:
α : 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 : α
⊢ ∫⁻ (b : β), (η (x, b)) {c | b ∈ s} ∂κ x = (κ x) s

Proof state:
α : 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 : α
b : β
⊢ (η (x, b)) {_c | b ∈ s} = s.indicator (fun x => 1) b

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

Result:
no goals

Proof state:
α : 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
⊢ ∫⁻ (b : β), s.indicator (fun x => 1) b ∂κ x = (κ x) s

Tactic:
rw [lintegral_indicator_const hs, one_mul]

Result:
no goals