no goals
α : Type u_1
β : Type u_2
γ : Type ?u.50828
δ : Type ?u.50831
ε : Type ?u.50834
ι : Type ?u.50837
f✝ f : α →. β
s : Set β
⊢ core f s = preimage f s ∪ Dom fᶜ
rw [preimage_eq, Set.union_distrib_right, Set.union_comm (Dom f), Set.compl_union_self,
  Set.inter_univ, Set.union_eq_self_of_subset_right (f.compl_dom_subset_core s)]