Tracking: attribute semireducible/irreducible

[jcommelin]

As part of the porting process to Lean 4, we should refactor mathlib to remove occurences of

local attribute [semireducible] foobar
attribute [irreducible] xyzzy

The following data is generated using the script in #18165.

---

https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/algebra/free_algebra.lean#L283
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/algebra/lie/free.lean#L239
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/algebra/ring_quot.lean#L402
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/algebraic_geometry/Gamma_Spec_adjunction.lean#L281
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/algebraic_geometry/Gamma_Spec_adjunction.lean#L293
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/algebraic_geometry/Gamma_Spec_adjunction.lean#L308
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/algebraic_geometry/Gamma_Spec_adjunction.lean#L329
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/algebraic_geometry/elliptic_curve/weierstrass.lean#L377
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/algebraic_topology/simplex_category.lean#L48
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/algebraic_topology/simplex_category.lean#L74
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/analysis/inner_product_space/pi_L2.lean#L719
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/analysis/inner_product_space/spectrum.lean#L217
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/category_theory/abelian/injective_resolution.lean#L100
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/category_theory/abelian/injective_resolution.lean#L160
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/category_theory/monoidal/opposite.lean#L45
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/category_theory/preadditive/projective_resolution.lean#L179
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/category_theory/preadditive/projective_resolution.lean#L243
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/category_theory/triangulated/rotate.lean#L53
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/data/complex/exponential.lean#L432
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/data/fin/basic.lean#L1912
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/data/polynomial/eval.lean#L743
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/data/rat/meta_defs.lean#L50
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/data/zmod/basic.lean#L490
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/data/zmod/quotient.lean#L101
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/field_theory/polynomial_galois_group.lean#L110
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/geometry/euclidean/angle/oriented/basic.lean#L612
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/group_theory/monoid_localization.lean#L214
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/group_theory/monoid_localization.lean#L258
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/group_theory/monoid_localization.lean#L1354
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/group_theory/monoid_localization.lean#L1364
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/group_theory/monoid_localization.lean#L1374
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/linear_algebra/clifford_algebra/basic.lean#L142
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/linear_algebra/determinant.lean#L146
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/linear_algebra/dimension.lean#L791
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/linear_algebra/finsupp.lean#L963
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/linear_algebra/tensor_algebra/basic.lean#L113
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/measure_theory/integral/bochner.lean#L1525
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/number_theory/padics/ring_homs.lean#L385
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/ring_theory/class_group.lean#L57
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/ring_theory/dedekind_domain/selmer_group.lean#L125
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/ring_theory/derivation.lean#L1025
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/ring_theory/fractional_ideal.lean#L431
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/ring_theory/fractional_ideal.lean#L1075
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/ring_theory/localization/fraction_ring.lean#L115
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/ring_theory/power_basis.lean#L341
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/ring_theory/valuation/basic.lean#L806
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/topology/algebra/group/basic.lean#L1133
https://github.com/leanprover-community/mathlib/blob/f69a62edd1bd8631558609ea19a317d67e1611b1/src/topology/omega_complete_partial_order.lean#L36