mathlib3

a7c50973 - feat(set_theory/cardinal/cofinality): Cofinality of normal functions (#12384)

feat(set_theory/cardinal/cofinality): Cofinality of normal functions (#12384) If `f` is normal and `a` is limit, then `cof (f a) = cof a`. We use this to golf `cof_add` from 24 lines down to 6.