chore(scripts): update nolints.txt (#9079)

I am happy to remove some nolints for you!

scripts/nolints.txt

@@ -2,12 +2,8 @@ import .all
 run_cmd tactic.skip
 
 -- algebra/free_algebra.lean
-apply_nolint free_algebra.ring check_reducibility
 apply_nolint free_algebra.semiring check_reducibility
 
--- algebra/free_non_unital_non_assoc_algebra.lean
-apply_nolint free_non_unital_non_assoc_algebra.add_comm_group check_reducibility
-
 -- algebra/ordered_monoid.lean
 apply_nolint with_zero.canonically_ordered_add_monoid check_reducibility
 
@@ -16,9 +12,6 @@ apply_nolint set.set_semiring.comm_semiring check_reducibility
 apply_nolint set.set_semiring.non_assoc_semiring check_reducibility
 apply_nolint set.set_semiring.non_unital_non_assoc_semiring check_reducibility
 
--- category_theory/monoidal/skeleton.lean
-apply_nolint category_theory.skeleton.monoid check_reducibility
-
 -- computability/partrec.lean
 apply_nolint computable doc_blame
 apply_nolint computable₂ doc_blame
@@ -238,15 +231,6 @@ apply_nolint list.sublists_aux doc_blame
 apply_nolint list.sublists_aux₁ doc_blame
 apply_nolint list.traverse doc_blame
 
--- data/list/func.lean
-apply_nolint list.func.add doc_blame
-apply_nolint list.func.equiv doc_blame
-apply_nolint list.func.get doc_blame
-apply_nolint list.func.neg doc_blame
-apply_nolint list.func.pointwise doc_blame
-apply_nolint list.func.set doc_blame
-apply_nolint list.func.sub doc_blame
-
 -- data/list/sigma.lean
 apply_nolint list.kextract doc_blame
 apply_nolint list.kreplace doc_blame
@@ -386,10 +370,6 @@ apply_nolint is_subfield doc_blame
 -- deprecated/subring.lean
 apply_nolint ring.closure doc_blame
 
--- field_theory/algebraic_closure.lean
-apply_nolint algebraic_closure.adjoin_monic.field check_reducibility
-apply_nolint algebraic_closure.field check_reducibility
-
 -- field_theory/finite/polynomial.lean
 apply_nolint mv_polynomial.R doc_blame unused_arguments
 apply_nolint mv_polynomial.evalᵢ doc_blame
@@ -399,9 +379,6 @@ apply_nolint mv_polynomial.indicator doc_blame
 -- group_theory/sylow.lean
 apply_nolint sylow.fixed_points_mul_left_cosets_equiv_quotient doc_blame
 
--- linear_algebra/pi_tensor_product.lean
-apply_nolint pi_tensor_product.add_comm_group check_reducibility
-
 -- logic/embedding.lean
 apply_nolint function.embedding.Pi_congr_right doc_blame
 apply_nolint function.embedding.arrow_congr_left doc_blame
@@ -448,9 +425,6 @@ apply_nolint tactic.mono doc_blame
 -- number_theory/dioph.lean
 apply_nolint poly has_inhabited_instance
 
--- number_theory/padics/padic_numbers.lean
-apply_nolint padic.field check_reducibility
-
 -- number_theory/pell.lean
 apply_nolint pell.az unused_arguments
 apply_nolint pell.x_sub_y_dvd_pow_lem unused_arguments
@@ -475,16 +449,6 @@ apply_nolint fixed_points.next_fixed doc_blame
 apply_nolint fixed_points.prev doc_blame
 apply_nolint fixed_points.prev_fixed doc_blame
 
--- ring_theory/adjoin_root.lean
-apply_nolint adjoin_root.field check_reducibility
-
--- ring_theory/ideal/local_ring.lean
-apply_nolint local_ring.residue_field.field check_reducibility
-
--- ring_theory/localization.lean
-apply_nolint fraction_ring.field check_reducibility
-apply_nolint is_localization.integral_domain_of_local_at_prime check_reducibility
-
 -- ring_theory/witt_vector/basic.lean
 apply_nolint witt_vector.comm_ring check_reducibility
 
@@ -496,18 +460,6 @@ apply_nolint pgame.inv_ty has_inhabited_instance
 
 -- set_theory/lists.lean
 apply_nolint finsets doc_blame
-apply_nolint lists doc_blame
-apply_nolint lists' doc_blame
-apply_nolint lists'.cons doc_blame
-apply_nolint lists'.of_list doc_blame
-apply_nolint lists'.to_list doc_blame
-apply_nolint lists.atom doc_blame
-apply_nolint lists.induction_mut doc_blame
-apply_nolint lists.is_list doc_blame
-apply_nolint lists.mem doc_blame
-apply_nolint lists.of' doc_blame
-apply_nolint lists.of_list doc_blame
-apply_nolint lists.to_list doc_blame
 
 -- set_theory/pgame.lean
 apply_nolint pgame.left_moves has_inhabited_instance

scripts/style-exceptions.txt

@@ -1,4 +1,3 @@
-src/algebra/ordered_ring.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/adjunction/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/adjunction/fully_faithful.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/adjunction/limits.lean : line 9 : ERR_MOD : Module docstring missing, or too late
@@ -39,9 +38,6 @@ src/data/array/lemmas.lean : line 9 : ERR_MOD : Module docstring missing, or too
 src/data/bitvec/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/data/buffer/basic.lean : line 12 : ERR_MOD : Module docstring missing, or too late
 src/data/dlist/instances.lean : line 12 : ERR_MOD : Module docstring missing, or too late
-src/data/list/func.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/data/list/of_fn.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/data/list/sigma.lean : line 12 : ERR_MOD : Module docstring missing, or too late
 src/data/pfunctor/multivariate/M.lean : line 43 : ERR_LIN : Line has more than 100 characters
 src/data/pfunctor/multivariate/W.lean : line 42 : ERR_LIN : Line has more than 100 characters
 src/data/pnat/intervals.lean : line 9 : ERR_MOD : Module docstring missing, or too late
@@ -58,7 +54,6 @@ src/deprecated/subfield.lean : line 8 : ERR_MOD : Module docstring missing, or t
 src/deprecated/subring.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/meta/coinductive_predicates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/set_theory/lists.lean : line 13 : ERR_MOD : Module docstring missing, or too late
 src/tactic/algebra.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/apply_fun.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/auto_cases.lean : line 8 : ERR_MOD : Module docstring missing, or too late