mathlib3

dce5dd4c - feat(order/well_founded, set_theory/ordinal_arithmetic): `eq_strict_mono_iff_eq_range` (#11882)

feat(order/well_founded, set_theory/ordinal_arithmetic): `eq_strict_mono_iff_eq_range` (#11882) Two strict monotonic functions with well-founded domains are equal iff their ranges are. We use this to golf `eq_enum_ord`.