mathlib3

ad7000b9 - feat(set_theory/cardinal): cardinal.to_nat_congr (#9726)

feat(set_theory/cardinal): cardinal.to_nat_congr (#9726) If `e : α ≃ β`, then `(cardinal.mk α).to_nat = (cardinal.mk β).to_nat`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>