feat(set_theory/zfc/basic): tweak Class hom lemmas (#18295)
This PR renames a bunch of `hom` lemmas to better match the style of the rest of mathlib, and tags them as `norm_cast`. We also add the corresponding lemmas for the union.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
