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

I am happy to remove some nolints for you!

scripts/nolints.txt

@@ -9,43 +9,6 @@ apply_nolint monoid_hom.ext_iff to_additive_doc
 apply_nolint mul_hom.ext_iff to_additive_doc
 apply_nolint one_hom.comp_assoc to_additive_doc
 
--- analysis/box_integral/box/basic.lean
-apply_nolint box_integral.box.Union_Ioo_of_tendsto fintype_finite
-
--- analysis/box_integral/partition/additive.lean
-apply_nolint box_integral.box_additive_map.sum_boxes_congr fintype_finite
-
--- analysis/box_integral/partition/measure.lean
-apply_nolint box_integral.box.measurable_set_Icc fintype_finite
-apply_nolint box_integral.box.measurable_set_Ioo fintype_finite
-apply_nolint box_integral.box.measurable_set_coe fintype_finite
-apply_nolint box_integral.prepartition.measure_Union_to_real fintype_finite
-
--- analysis/box_integral/partition/split.lean
-apply_nolint box_integral.prepartition.eventually_not_disjoint_imp_le_of_mem_split_many fintype_finite
-apply_nolint box_integral.prepartition.eventually_split_many_inf_eq_filter fintype_finite
-apply_nolint box_integral.prepartition.exists_Union_eq_diff fintype_finite
-apply_nolint box_integral.prepartition.exists_split_many_inf_eq_filter_of_finite fintype_finite
-apply_nolint box_integral.prepartition.is_partition.exists_split_many_le fintype_finite
-
--- analysis/calculus/lagrange_multipliers.lean
-apply_nolint is_local_extr_on.linear_dependent_of_has_strict_fderiv_at fintype_finite
-
--- analysis/calculus/tangent_cone.lean
-apply_nolint unique_diff_on.pi fintype_finite
-apply_nolint unique_diff_on.univ_pi fintype_finite
-apply_nolint unique_diff_within_at.pi fintype_finite
-apply_nolint unique_diff_within_at.univ_pi fintype_finite
-
--- analysis/normed_space/add_torsor_bases.lean
-apply_nolint interior_convex_hull_aff_basis fintype_finite
-
--- analysis/normed_space/finite_dimension.lean
-apply_nolint basis.exists_op_nnnorm_le fintype_finite
-apply_nolint basis.exists_op_norm_le fintype_finite
-apply_nolint is_open_set_of_linear_independent fintype_finite
-apply_nolint linear_independent.eventually fintype_finite
-
 -- category_theory/limits/filtered_colimit_commutes_finite_limit.lean
 apply_nolint category_theory.limits.colimit_limit_to_limit_colimit_injective fintype_finite
 apply_nolint category_theory.limits.colimit_limit_to_limit_colimit_is_iso fails_quickly
@@ -492,13 +455,6 @@ apply_nolint basis.eval_range fintype_finite
 apply_nolint basis.to_dual_range fintype_finite
 apply_nolint basis.total_coord fintype_finite
 
--- linear_algebra/finite_dimensional.lean
-apply_nolint finite_dimensional.finite_dimensional_pi fintype_finite
-apply_nolint finite_dimensional.finite_dimensional_pi' fintype_finite
-apply_nolint finite_dimensional.of_fintype_basis fintype_finite
-apply_nolint finite_dimensional_finsupp fintype_finite
-apply_nolint submodule.finite_dimensional_supr fintype_finite
-
 -- linear_algebra/finsupp_vector_space.lean
 apply_nolint cardinal_lt_aleph_0_of_finite_dimensional fintype_finite
 
@@ -537,13 +493,6 @@ apply_nolint module.free.multilinear_map fintype_finite
 -- linear_algebra/orientation.lean
 apply_nolint basis.map_orientation_eq_det_inv_smul fintype_finite
 
--- linear_algebra/pi.lean
-apply_nolint linear_map.pi_ext fintype_finite
-apply_nolint linear_map.pi_ext' fintype_finite
-apply_nolint linear_map.pi_ext'_iff fintype_finite
-apply_nolint linear_map.pi_ext_iff fintype_finite
-apply_nolint submodule.supr_map_single fintype_finite
-
 -- linear_algebra/std_basis.lean
 apply_nolint linear_map.supr_range_std_basis fintype_finite
 
@@ -559,60 +508,6 @@ apply_nolint relator.lift_fun doc_blame
 apply_nolint relator.right_total doc_blame
 apply_nolint relator.right_unique doc_blame
 
--- measure_theory/constructions/borel_space.lean
-apply_nolint pi.borel_space_fintype fintype_finite
-apply_nolint pi.opens_measurable_space_fintype fintype_finite
-
--- measure_theory/constructions/pi.lean
-apply_nolint generate_from_eq_pi fintype_finite
-apply_nolint generate_from_pi fintype_finite
-apply_nolint generate_from_pi_eq fintype_finite
-apply_nolint is_countably_spanning.pi fintype_finite
-
--- measure_theory/constructions/prod.lean
-apply_nolint measure_theory.measure.prod_sum fintype_finite
-apply_nolint measure_theory.measure.sum_prod fintype_finite
-
--- measure_theory/group/prod.lean
-apply_nolint measure_theory.map_prod_inv_mul_eq to_additive_doc
-apply_nolint measure_theory.map_prod_inv_mul_eq_swap to_additive_doc
-apply_nolint measure_theory.map_prod_mul_inv_eq to_additive_doc
-apply_nolint measure_theory.measure_lintegral_div_measure to_additive_doc
-apply_nolint measure_theory.measure_mul_lintegral_eq to_additive_doc
-
--- measure_theory/integral/integrable_on.lean
-apply_nolint measure_theory.integrable_on_fintype_Union fintype_finite
-
--- measure_theory/measurable_space.lean
-apply_nolint measurable_of_fintype fintype_finite
-apply_nolint measurable_set.pi_fintype fintype_finite
-apply_nolint measurable_set.univ_pi_fintype fintype_finite
-
--- measure_theory/measurable_space_def.lean
-apply_nolint measurable_set.Inter_fintype fintype_finite
-apply_nolint measurable_set.Union_fintype fintype_finite
-
--- measure_theory/measure/haar.lean
-apply_nolint measure_theory.measure.haar.haar_content_self to_additive_doc
-apply_nolint measure_theory.measure.haar.index_defined to_additive_doc
-apply_nolint measure_theory.measure.haar.is_left_invariant_haar_content to_additive_doc
-apply_nolint measure_theory.measure.haar_measure_unique to_additive_doc
-apply_nolint measure_theory.measure.is_haar_measure_haar_measure to_additive_doc
-apply_nolint measure_theory.measure.map_haar_inv to_additive_doc
-apply_nolint measure_theory.measure.regular_haar_measure to_additive_doc
-apply_nolint measure_theory.measure.regular_of_is_mul_left_invariant to_additive_doc
-apply_nolint measure_theory.measure.sigma_finite_haar_measure to_additive_doc
-
--- measure_theory/measure/haar_lebesgue.lean
-apply_nolint measure_theory.measure.map_linear_map_add_haar_pi_eq_smul_add_haar fintype_finite
-
--- measure_theory/measure/measure_space.lean
-apply_nolint measure_theory.sum.sigma_finite fintype_finite
-
--- measure_theory/measure/null_measurable.lean
-apply_nolint measure_theory.null_measurable_set.Inter_fintype fintype_finite
-apply_nolint measure_theory.null_measurable_set.Union_fintype fintype_finite
-
 -- meta/coinductive_predicates.lean
 apply_nolint monotonicity doc_blame
 apply_nolint tactic.add_coinductive_predicate doc_blame
@@ -676,12 +571,6 @@ apply_nolint ideal.mv_polynomial.mv_polynomial.ideal.is_jacobson fintype_finite
 -- ring_theory/localization/integer.lean
 apply_nolint is_localization.exist_integer_multiples_of_fintype fintype_finite
 
--- ring_theory/noetherian.lean
-apply_nolint is_noetherian_pi fintype_finite
-apply_nolint is_noetherian_pi' fintype_finite
-apply_nolint submodule.fg_pi fintype_finite
-apply_nolint submodule.fg_supr fintype_finite
-
 -- ring_theory/norm.lean
 apply_nolint algebra.norm_eq_zero_iff_of_basis fintype_finite
 apply_nolint algebra.norm_ne_zero_iff_of_basis fintype_finite