chore(set_theory/zfc): split long lines (#4641)
chore(set_theory/zfc): split long lines (#4641)

Also add `Set.subset_def` and rewrite `Set.mem_pair_sep` in tactic mode





leanprover-community/mathlib,leanprover-community/mathlib