no goals
α : Type u_1
β : Type u_2
γ : Type ?u.812591
δ : Type ?u.812594
inst✝¹ : MeasurableSpace α
K : Type ?u.812600
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
a : α
⊢ ↑(restrict f s) a = indicator s (↑f) a
simp only [f.coe_restrict hs]