no goals
α : Type u_1
β : Type u_2
ι : Type ?u.1444889
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t : Set β
κ : { x // x ∈ kernel α β }
hs : MeasurableSet s
a : α
f : β → ℝ≥0∞
⊢ (∫⁻ (b : β), f b ∂↑(kernel.restrict κ hs) a) = ∫⁻ (b : β) in s, f b ∂↑κ a
rw [restrict_apply]