no goals
α : Type u_1
β : Type u_2
ι : Type ?u.1443714
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
s t : Set β
κ : { x // x ∈ kernel α β }
hs : MeasurableSet s
a : α
ht : MeasurableSet t
⊢ ↑↑(↑(kernel.restrict κ hs) a) t = ↑↑(↑κ a) (t ∩ s)
rw [restrict_apply κ hs a, Measure.restrict_apply ht]