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

I am happy to remove some nolints for you!

scripts/nolints.txt

@@ -1,6 +1,11 @@
 import .all
 run_cmd tactic.skip
 
+-- algebra/big_operators/fin.lean
+apply_nolint fin.prod_univ_cast_succ to_additive_doc
+apply_nolint fin.prod_univ_succ to_additive_doc
+apply_nolint fin.prod_univ_succ_above to_additive_doc
+
 -- algebra/category/Group/limits.lean
 apply_nolint CommGroup.category_theory.forget₂.category_theory.creates_limit to_additive_doc
 apply_nolint CommGroup.forget_preserves_limits to_additive_doc
@@ -213,10 +218,7 @@ apply_nolint locally_finite.realizer doc_blame has_inhabited_instance
 apply_nolint finset.noncomm_prod_union_of_disjoint to_additive_doc
 
 -- data/fintype/card.lean
-apply_nolint fin.prod_univ_cast_succ to_additive_doc
 apply_nolint fin.prod_univ_eq_prod_range to_additive_doc
-apply_nolint fin.prod_univ_succ to_additive_doc
-apply_nolint fin.prod_univ_succ_above to_additive_doc
 
 -- data/fp/basic.lean
 apply_nolint fp.div_nat_lt_two_pow doc_blame unused_arguments