no goals
α : Type u_1
β : Type u_2
γ : Type ?u.13942
δ : Type ?u.13945
ε : Type ?u.13948
ι : Type ?u.13951
f : α →. β
s : Set α
h : s ⊆ Dom f
a : α
b : β
⊢ b ∈ restrict f h a ↔ a ∈ s ∧ b ∈ f a
simp [restrict]