chore(scripts): update nolints.txt

scripts/nolints.txt

@@ -954,17 +954,12 @@ apply_nolint real.tanh doc_blame
 -- data/dfinsupp.lean
 apply_nolint decidable_zero_symm doc_blame
 apply_nolint dfinsupp doc_blame
-apply_nolint dfinsupp.decidable_eq unused_arguments
 apply_nolint dfinsupp.erase doc_blame
 apply_nolint dfinsupp.lmk doc_blame
 apply_nolint dfinsupp.lsingle doc_blame
-apply_nolint dfinsupp.map_range_def unused_arguments
-apply_nolint dfinsupp.map_range_single unused_arguments
 apply_nolint dfinsupp.mk doc_blame
-apply_nolint dfinsupp.pre doc_blame has_inhabited_instance
+apply_nolint dfinsupp.pre doc_blame
 apply_nolint dfinsupp.single doc_blame
-apply_nolint dfinsupp.subtype_domain_sum unused_arguments
-apply_nolint dfinsupp.sum_apply unused_arguments
 apply_nolint dfinsupp.support doc_blame
 apply_nolint dfinsupp.to_has_scalar doc_blame
 apply_nolint dfinsupp.to_module doc_blame
@@ -1237,8 +1232,6 @@ apply_nolint int.shift2 doc_blame
 
 -- data/hash_map.lean
 apply_nolint hash_map has_inhabited_instance
-apply_nolint hash_map.mk_as_list unused_arguments
-apply_nolint hash_map.valid.modify ge_or_gt
 
 -- data/holor.lean
 apply_nolint holor.assoc_left doc_blame
@@ -1251,8 +1244,6 @@ apply_nolint holor_index.take doc_blame
 
 -- data/int/basic.lean
 apply_nolint int.bit_cases_on doc_blame
-apply_nolint int.div_eq_div_of_mul_eq_mul unused_arguments
-apply_nolint int.eq_mul_div_of_mul_eq_mul_of_dvd_left unused_arguments
 apply_nolint int.induction_on' doc_blame
 apply_nolint int.range doc_blame
 apply_nolint int.to_nat' doc_blame
@@ -1322,7 +1313,6 @@ apply_nolint list.traverse doc_blame
 apply_nolint list.erase_dupkeys doc_blame
 apply_nolint list.kextract doc_blame
 apply_nolint list.kreplace doc_blame
-apply_nolint list.mem_ext unused_arguments
 apply_nolint list.nodupkeys doc_blame
 
 -- data/matrix/basic.lean
@@ -1345,12 +1335,6 @@ apply_nolint matrix.transpose doc_blame
 apply_nolint matrix.vec_mul doc_blame
 apply_nolint matrix.vec_mul_vec doc_blame
 
--- data/matrix/pequiv.lean
-apply_nolint pequiv.matrix_mul_apply unused_arguments
-apply_nolint pequiv.mul_matrix_apply unused_arguments
-apply_nolint pequiv.single_mul_single_right unused_arguments
-apply_nolint pequiv.to_matrix unused_arguments
-
 -- data/mllist.lean
 apply_nolint tactic.mllist doc_blame
 apply_nolint tactic.mllist.append doc_blame unused_arguments
@@ -1385,9 +1369,6 @@ apply_nolint multiset.choose doc_blame
 apply_nolint multiset.choose_x doc_blame
 apply_nolint multiset.decidable_exists_multiset doc_blame
 apply_nolint multiset.decidable_forall_multiset doc_blame
-apply_nolint multiset.le_inf unused_arguments
-apply_nolint multiset.length_ndinsert_of_mem unused_arguments
-apply_nolint multiset.length_ndinsert_of_not_mem unused_arguments
 apply_nolint multiset.pi.cons doc_blame
 apply_nolint multiset.pi.empty doc_blame unused_arguments
 apply_nolint multiset.powerset doc_blame
@@ -1400,7 +1381,6 @@ apply_nolint multiset.sections doc_blame
 apply_nolint multiset.strong_induction_on doc_blame
 apply_nolint multiset.subsingleton_equiv doc_blame
 apply_nolint multiset.sum doc_blame
-apply_nolint multiset.sup_le unused_arguments
 apply_nolint multiset.traverse doc_blame
 
 -- data/nat/enat.lean
@@ -1580,7 +1560,6 @@ apply_nolint pequiv.refl doc_blame
 apply_nolint pequiv.single doc_blame
 apply_nolint pequiv.symm doc_blame
 apply_nolint pequiv.trans doc_blame
-apply_nolint pequiv.trans_single_of_eq_none unused_arguments
 
 -- data/pfun.lean
 apply_nolint pfun.core doc_blame
@@ -1862,7 +1841,6 @@ apply_nolint gaussian_int.to_complex doc_blame
 
 -- field_theory/finite.lean
 apply_nolint finite_field.field_of_integral_domain doc_blame
-apply_nolint subgroup_units_cyclic unused_arguments
 
 -- field_theory/mv_polynomial.lean
 apply_nolint mv_polynomial.R doc_blame unused_arguments
@@ -1971,14 +1949,9 @@ apply_nolint mul_action.stabilizer doc_blame
 apply_nolint mul_action.to_perm doc_blame
 
 -- group_theory/order_of_element.lean
-apply_nolint card_subgroup_dvd_card unused_arguments
-apply_nolint card_trivial unused_arguments
-apply_nolint exists_gpow_eq_one unused_arguments
 apply_nolint exists_pow_eq_one ge_or_gt
 apply_nolint is_cyclic doc_blame
 apply_nolint is_cyclic.comm_group doc_blame
-apply_nolint order_of_pos ge_or_gt
-apply_nolint quotient_group.fintype unused_arguments
 
 -- group_theory/perm/cycles.lean
 apply_nolint equiv.perm.cycle_factors doc_blame
@@ -2076,10 +2049,8 @@ apply_nolint finsupp.lsubtype_domain doc_blame
 apply_nolint finsupp.lsum doc_blame
 apply_nolint finsupp.restrict_dom doc_blame
 apply_nolint finsupp.supported doc_blame
-apply_nolint finsupp.supported_eq_span_single unused_arguments
 apply_nolint finsupp.supported_equiv_finsupp doc_blame
 apply_nolint finsupp.total_on doc_blame
-apply_nolint linear_map.map_finsupp_total unused_arguments
 
 -- linear_algebra/finsupp_vector_space.lean
 apply_nolint equiv_of_dim_eq_dim doc_blame
@@ -2366,8 +2337,6 @@ apply_nolint pi.lex doc_blame
 apply_nolint pilex doc_blame
 
 -- ring_theory/adjoin.lean
-apply_nolint algebra.adjoin_eq_range unused_arguments
-apply_nolint algebra.adjoin_singleton_eq_range unused_arguments
 apply_nolint subalgebra.fg doc_blame
 
 -- ring_theory/algebra.lean
@@ -2453,7 +2422,6 @@ apply_nolint localization.away.inv_self doc_blame
 apply_nolint localization.away.lift doc_blame
 apply_nolint localization.away_to_away_right doc_blame
 apply_nolint localization.equiv_of_equiv doc_blame
-apply_nolint localization.fraction_ring.eq_zero_of_ne_zero_of_mul_eq_zero unused_arguments
 apply_nolint localization.fraction_ring.equiv_of_equiv doc_blame
 apply_nolint localization.fraction_ring.inv_aux doc_blame
 apply_nolint localization.fraction_ring.map doc_blame
@@ -2463,7 +2431,7 @@ apply_nolint localization.lift' doc_blame
 apply_nolint localization.map doc_blame
 apply_nolint localization.mk doc_blame
 apply_nolint localization.non_zero_divisors doc_blame
-apply_nolint localization.r doc_blame unused_arguments
+apply_nolint localization.r doc_blame
 
 -- ring_theory/maps.lean
 apply_nolint comm_ring.anti_equiv_to_equiv doc_blame
@@ -2476,7 +2444,6 @@ apply_nolint ring_invo.to_ring_anti_equiv doc_blame
 
 -- ring_theory/multiplicity.lean
 apply_nolint multiplicity.finite doc_blame
-apply_nolint multiplicity.finite_mul_aux unused_arguments
 
 -- ring_theory/noetherian.lean
 apply_nolint is_noetherian_iff_well_founded ge_or_gt
@@ -2503,13 +2470,9 @@ apply_nolint principal_ideal_domain.factors doc_blame
 apply_nolint ring.closure doc_blame
 
 -- ring_theory/unique_factorization_domain.lean
-apply_nolint associates.factor_set unused_arguments
-apply_nolint associates.factor_set.coe_add unused_arguments
-apply_nolint associates.factor_set.prod doc_blame unused_arguments
+apply_nolint associates.factor_set.prod doc_blame
 apply_nolint associates.factors doc_blame
-apply_nolint associates.factors' doc_blame unused_arguments
-apply_nolint associates.unique' unused_arguments
-apply_nolint unique_factorization_domain.exists_mem_factors_of_dvd unused_arguments
+apply_nolint associates.factors' doc_blame
 apply_nolint unique_factorization_domain.of_unique_irreducible_factorization doc_blame
 apply_nolint unique_irreducible_factorization doc_blame has_inhabited_instance