mathlib3
565eb991 - chore(*): remove after the fact `attribute [irreducible]` at several places (#18168)
