mathlib

b7808a99 - chore(set_theory/ordinal_arithmetic): Golf `lsub_typein` and `blsub_id` (#12203)