mathlib3
39afa0b3 - chore(*): remove after the fact attribute [irreducible] at several places (2) (#18180)
