mathlib

mathlib copied to clipboard

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