mathlib

98f747f8 - chore(set_theory/zfc): better def-eqs (#15210)

chore(set_theory/zfc): better def-eqs (#15210) We sidestep the equation compiler when not strictly needed, thus improving the definitional equalities on some basic definitions. This also allows us to inline many instances.