no goals
α : Type u_3
β : Type u_2
ι : Type ?u.1446410
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
s t✝ : Set β
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : β → E
a : α
hs : MeasurableSet s
t : Set β
⊢ (∫ (x : β) in t, f x ∂↑(kernel.restrict κ hs) a) = ∫ (x : β) in t ∩ s, f x ∂↑κ a
rw [restrict_apply, Measure.restrict_restrict' hs]