no goals
α : Type u_1
β : Type u_2
γ : Type ?u.812913
δ : Type ?u.812916
inst✝¹ : MeasurableSpace α
K : Type ?u.812922
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
t : Set β
ht : ¬0 ∈ t
⊢ ↑(restrict f s) ⁻¹' t = s ∩ ↑f ⁻¹' t
simp [hs, indicator_preimage_of_not_mem _ _ ht, inter_comm]