no goals
α : Type u_1
β : Type u_2
γ : Type ?u.46763
δ : Type ?u.46766
ε : Type ?u.46769
ι : Type ?u.46772
f✝ : α →. β
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ core (res f s) t ↔ x ∈ s → f x ∈ t
simp [mem_core, mem_res]