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

I am happy to remove some nolints for you!

scripts/copy-mod-doc-exceptions.txt

@@ -7,7 +7,6 @@ archive/100-theorems-list/82_cubing_a_cube.lean : line 294 : ERR_LIN : Line has
 archive/100-theorems-list/83_friendship_graphs.lean : line 215 : ERR_LIN : Line has more than 100 characters
 archive/100-theorems-list/83_friendship_graphs.lean : line 257 : ERR_LIN : Line has more than 100 characters
 archive/imo/imo1959_q1.lean : line 10 : ERR_MOD : Module docstring missing, or too late
-archive/imo/imo1969_q1.lean : line 12 : ERR_MOD : Module docstring missing, or too late
 archive/imo/imo1972_b2.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 archive/miu_language/basic.lean : line 53 : ERR_LIN : Line has more than 100 characters
 archive/sensitivity.lean : line 405 : ERR_LIN : Line has more than 100 characters
@@ -168,7 +167,7 @@ src/analysis/analytic/composition.lean : line 906 : ERR_LIN : Line has more than
 src/analysis/analytic/composition.lean : line 907 : ERR_LIN : Line has more than 100 characters
 src/analysis/analytic/composition.lean : line 910 : ERR_LIN : Line has more than 100 characters
 src/analysis/analytic/composition.lean : line 950 : ERR_LIN : Line has more than 100 characters
-src/analysis/calculus/deriv.lean : line 1073 : ERR_LIN : Line has more than 100 characters
+src/analysis/calculus/deriv.lean : line 1095 : ERR_LIN : Line has more than 100 characters
 src/analysis/calculus/deriv.lean : line 308 : ERR_LIN : Line has more than 100 characters
 src/analysis/calculus/fderiv.lean : line 1865 : ERR_LIN : Line has more than 100 characters
 src/analysis/calculus/fderiv.lean : line 205 : ERR_LIN : Line has more than 100 characters
@@ -773,13 +772,13 @@ src/data/list/sigma.lean : line 559 : ERR_LIN : Line has more than 100 character
 src/data/list/sort.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/data/list/tfae.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/data/list/zip.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/data/matrix/basic.lean : line 326 : ERR_LIN : Line has more than 100 characters
-src/data/matrix/basic.lean : line 329 : ERR_LIN : Line has more than 100 characters
-src/data/matrix/basic.lean : line 488 : ERR_LIN : Line has more than 100 characters
-src/data/matrix/basic.lean : line 76 : ERR_LIN : Line has more than 100 characters
-src/data/matrix/basic.lean : line 843 : ERR_LIN : Line has more than 100 characters
-src/data/matrix/basic.lean : line 845 : ERR_LIN : Line has more than 100 characters
-src/data/matrix/basic.lean : line 898 : ERR_LIN : Line has more than 100 characters
+src/data/matrix/basic.lean : line 332 : ERR_LIN : Line has more than 100 characters
+src/data/matrix/basic.lean : line 335 : ERR_LIN : Line has more than 100 characters
+src/data/matrix/basic.lean : line 494 : ERR_LIN : Line has more than 100 characters
+src/data/matrix/basic.lean : line 82 : ERR_LIN : Line has more than 100 characters
+src/data/matrix/basic.lean : line 866 : ERR_LIN : Line has more than 100 characters
+src/data/matrix/basic.lean : line 868 : ERR_LIN : Line has more than 100 characters
+src/data/matrix/basic.lean : line 921 : ERR_LIN : Line has more than 100 characters
 src/data/matrix/notation.lean : line 375 : ERR_LIN : Line has more than 100 characters
 src/data/matrix/pequiv.lean : line 137 : ERR_LIN : Line has more than 100 characters
 src/data/matrix/pequiv.lean : line 143 : ERR_LIN : Line has more than 100 characters
@@ -855,8 +854,6 @@ src/data/nat/multiplicity.lean : line 15 : ERR_LIN : Line has more than 100 char
 src/data/nat/multiplicity.lean : line 164 : ERR_LIN : Line has more than 100 characters
 src/data/nat/pairing.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/data/nat/parity.lean : line 10 : ERR_MOD : Module docstring missing, or too late
-src/data/nat/prime.lean : line 251 : ERR_LIN : Line has more than 100 characters
-src/data/nat/prime.lean : line 559 : ERR_LIN : Line has more than 100 characters
 src/data/nat/totient.lean : line 61 : ERR_LIN : Line has more than 100 characters
 src/data/nat/totient.lean : line 71 : ERR_LIN : Line has more than 100 characters
 src/data/nat/totient.lean : line 8 : ERR_MOD : Module docstring missing, or too late
@@ -937,7 +934,7 @@ src/data/rat/basic.lean : line 688 : ERR_LIN : Line has more than 100 characters
 src/data/rat/basic.lean : line 694 : ERR_LIN : Line has more than 100 characters
 src/data/rat/denumerable.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/data/rat/sqrt.lean : line 12 : ERR_LIN : Line has more than 100 characters
-src/data/real/basic.lean : line 13 : ERR_MOD : Module docstring missing, or too late
+src/data/real/basic.lean : line 14 : ERR_MOD : Module docstring missing, or too late
 src/data/real/cardinality.lean : line 29 : ERR_LIN : Line has more than 100 characters
 src/data/real/cau_seq_completion.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/data/rel.lean : line 10 : ERR_MOD : Module docstring missing, or too late
@@ -956,11 +953,6 @@ src/data/set/countable.lean : line 122 : ERR_LIN : Line has more than 100 charac
 src/data/set/countable.lean : line 138 : ERR_LIN : Line has more than 100 characters
 src/data/set/disjointed.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/data/set/enumerate.lean : line 10 : ERR_MOD : Module docstring missing, or too late
-src/data/set/finite.lean : line 128 : ERR_LIN : Line has more than 100 characters
-src/data/set/finite.lean : line 210 : ERR_LIN : Line has more than 100 characters
-src/data/set/finite.lean : line 216 : ERR_LIN : Line has more than 100 characters
-src/data/set/finite.lean : line 297 : ERR_LIN : Line has more than 100 characters
-src/data/set/finite.lean : line 420 : ERR_LIN : Line has more than 100 characters
 src/data/set/function.lean : line 409 : ERR_LIN : Line has more than 100 characters
 src/data/set/lattice.lean : line 13 : ERR_MOD : Module docstring missing, or too late
 src/data/set/lattice.lean : line 453 : ERR_LIN : Line has more than 100 characters
@@ -1025,10 +1017,13 @@ src/field_theory/separable.lean : line 219 : ERR_LIN : Line has more than 100 ch
 src/field_theory/separable.lean : line 404 : ERR_LIN : Line has more than 100 characters
 src/field_theory/separable.lean : line 523 : ERR_LIN : Line has more than 100 characters
 src/field_theory/splitting_field.lean : line 15 : ERR_MOD : Module docstring missing, or too late
-src/field_theory/splitting_field.lean : line 440 : ERR_LIN : Line has more than 100 characters
-src/field_theory/splitting_field.lean : line 489 : ERR_LIN : Line has more than 100 characters
-src/field_theory/splitting_field.lean : line 504 : ERR_LIN : Line has more than 100 characters
-src/field_theory/splitting_field.lean : line 580 : ERR_LIN : Line has more than 100 characters
+src/field_theory/splitting_field.lean : line 374 : ERR_LIN : Line has more than 100 characters
+src/field_theory/splitting_field.lean : line 376 : ERR_LIN : Line has more than 100 characters
+src/field_theory/splitting_field.lean : line 379 : ERR_LIN : Line has more than 100 characters
+src/field_theory/splitting_field.lean : line 436 : ERR_LIN : Line has more than 100 characters
+src/field_theory/splitting_field.lean : line 485 : ERR_LIN : Line has more than 100 characters
+src/field_theory/splitting_field.lean : line 500 : ERR_LIN : Line has more than 100 characters
+src/field_theory/splitting_field.lean : line 576 : ERR_LIN : Line has more than 100 characters
 src/field_theory/splitting_field.lean : line 76 : ERR_LIN : Line has more than 100 characters
 src/field_theory/splitting_field.lean : line 77 : ERR_LIN : Line has more than 100 characters
 src/field_theory/subfield.lean : line 449 : ERR_LIN : Line has more than 100 characters