mathlib3

5931c5cb - lint(set_theory/ordinal): fix def/lemma (#6369)