chore(set_theory/ordinal/arithmetic): review cast API (#14757)
This PR does the following:
- swap the direction of `nat_cast_succ` to match `nat.cast_succ`.
- make various arguments explicit.
- remove `lift_type_fin`, as it's a trivial consequence of `type_fin` and `lift_nat_cast`.
- tag various theorems as `norm_cast`.
- golf or otherwise cleanup various proofs.
