mathlib

f32fda7c - feat(set_theory/ordinal_arithmetic): More `lsub` and `blsub` lemmas (#11848)

feat(set_theory/ordinal_arithmetic): More `lsub` and `blsub` lemmas (#11848) We prove variants of `sup_typein`, which serve as analogs for `blsub_id`. We also prove `sup_eq_lsub_or_sup_succ_eq_lsub`, which combines `sup_le_lsub` and `lsub_le_sup_succ`.