mathlib3

24cfb883 - chore(set_theory/ordinal_arithmetic): Golf some instances of `lt_irrefl _ h` down to `h.false` (#11699)