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

I am happy to remove some nolints for you!

scripts/style-exceptions.txt

@@ -32,12 +32,8 @@ src/computability/partrec_code.lean : line 10 : ERR_MOD : Module docstring missi
 src/control/applicative.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/control/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/control/bifunctor.lean : line 12 : ERR_MOD : Module docstring missing, or too late
-src/control/functor/multivariate.lean : line 172 : ERR_LIN : Line has more than 100 characters
-src/control/functor/multivariate.lean : line 177 : ERR_LIN : Line has more than 100 characters
-src/control/functor/multivariate.lean : line 178 : ERR_LIN : Line has more than 100 characters
 src/control/monad/cont.lean : line 12 : ERR_MOD : Module docstring missing, or too late
 src/control/monad/writer.lean : line 11 : ERR_MOD : Module docstring missing, or too late
-src/control/monad/writer.lean : line 153 : ERR_LIN : Line has more than 100 characters
 src/control/traversable/derive.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/control/traversable/equiv.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/control/traversable/instances.lean : line 12 : ERR_MOD : Module docstring missing, or too late
@@ -84,21 +80,11 @@ src/data/list/zip.lean : line 8 : ERR_MOD : Module docstring missing, or too lat
 src/data/matrix/pequiv.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/data/mllist.lean : line 14 : ERR_MOD : Module docstring missing, or too late
 src/data/multiset/range.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/data/mv_polynomial/variables.lean : line 628 : ERR_LIN : Line has more than 100 characters
-src/data/nat/basic.lean : line 908 : ERR_LIN : Line has more than 100 characters
 src/data/nat/cast.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/data/nat/dist.lean : line 10 : ERR_MOD : Module docstring missing, or too late
-src/data/nat/gcd.lean : line 200 : ERR_LIN : Line has more than 100 characters
-src/data/nat/gcd.lean : line 54 : ERR_LIN : Line has more than 100 characters
-src/data/nat/modeq.lean : line 214 : ERR_LIN : Line has more than 100 characters
 src/data/nat/modeq.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/data/nat/multiplicity.lean : line 143 : ERR_LIN : Line has more than 100 characters
-src/data/nat/multiplicity.lean : line 144 : ERR_LIN : Line has more than 100 characters
-src/data/nat/multiplicity.lean : line 165 : 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/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
 src/data/option/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/data/option/defs.lean : line 9 : ERR_MOD : Module docstring missing, or too late
@@ -143,46 +129,17 @@ src/deprecated/subgroup.lean : line 10 : ERR_MOD : Module docstring missing, or
 src/deprecated/subring.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/geometry/euclidean/basic.lean : line 13 : ERR_MOD : Module docstring missing, or too late
 src/geometry/euclidean/circumcenter.lean : line 10 : ERR_MOD : Module docstring missing, or too late
-src/geometry/euclidean/circumcenter.lean : line 544 : ERR_LIN : Line has more than 100 characters
-src/geometry/euclidean/circumcenter.lean : line 840 : ERR_LIN : Line has more than 100 characters
-src/geometry/euclidean/circumcenter.lean : line 845 : ERR_LIN : Line has more than 100 characters
-src/geometry/euclidean/circumcenter.lean : line 849 : ERR_LIN : Line has more than 100 characters
 src/geometry/euclidean/monge_point.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/geometry/euclidean/triangle.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/geometry/manifold/charted_space.lean : line 574 : ERR_LIN : Line has more than 100 characters
-src/geometry/manifold/charted_space.lean : line 846 : ERR_LIN : Line has more than 100 characters
-src/geometry/manifold/charted_space.lean : line 891 : ERR_LIN : Line has more than 100 characters
-src/geometry/manifold/local_invariant_properties.lean : line 211 : ERR_LIN : Line has more than 100 characters
-src/geometry/manifold/local_invariant_properties.lean : line 216 : ERR_LIN : Line has more than 100 characters
-src/geometry/manifold/local_invariant_properties.lean : line 388 : ERR_LIN : Line has more than 100 characters
-src/geometry/manifold/local_invariant_properties.lean : line 433 : ERR_LIN : Line has more than 100 characters
 src/logic/relation.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/measure_theory/decomposition.lean : line 14 : ERR_MOD : Module docstring missing, or too late
-src/meta/coinductive_predicates.lean : line 115 : ERR_LIN : Line has more than 100 characters
-src/meta/coinductive_predicates.lean : line 12 : ERR_LIN : Line has more than 100 characters
-src/meta/coinductive_predicates.lean : line 281 : ERR_LIN : Line has more than 100 characters
-src/meta/coinductive_predicates.lean : line 296 : ERR_LIN : Line has more than 100 characters
-src/meta/coinductive_predicates.lean : line 303 : ERR_LIN : Line has more than 100 characters
-src/meta/coinductive_predicates.lean : line 438 : ERR_LIN : Line has more than 100 characters
-src/meta/coinductive_predicates.lean : line 448 : ERR_LIN : Line has more than 100 characters
-src/meta/coinductive_predicates.lean : line 488 : ERR_LIN : Line has more than 100 characters
-src/meta/coinductive_predicates.lean : line 76 : ERR_LIN : Line has more than 100 characters
-src/meta/coinductive_predicates.lean : line 77 : ERR_LIN : Line has more than 100 characters
 src/meta/coinductive_predicates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/meta/expr.lean : line 1007 : ERR_LIN : Line has more than 100 characters
-src/meta/expr.lean : line 496 : ERR_LIN : Line has more than 100 characters
-src/meta/expr.lean : line 751 : ERR_LIN : Line has more than 100 characters
-src/meta/expr.lean : line 786 : ERR_LIN : Line has more than 100 characters
 src/meta/expr_lens.lean : line 130 : ERR_LIN : Line has more than 100 characters
 src/meta/rb_map.lean : line 14 : ERR_LIN : Line has more than 100 characters
 src/order/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/order/boolean_algebra.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/order/bounded_lattice.lean : line 15 : ERR_MOD : Module docstring missing, or too late
-src/order/bounded_lattice.lean : line 227 : ERR_LIN : Line has more than 100 characters
-src/order/bounded_lattice.lean : line 231 : ERR_LIN : Line has more than 100 characters
-src/order/bounded_lattice.lean : line 235 : ERR_LIN : Line has more than 100 characters
-src/order/bounded_lattice.lean : line 239 : ERR_LIN : Line has more than 100 characters
 src/order/complete_boolean_algebra.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/order/complete_lattice.lean : line 134 : ERR_LIN : Line has more than 100 characters
 src/order/complete_lattice.lean : line 94 : ERR_LIN : Line has more than 100 characters
@@ -191,12 +148,6 @@ src/order/conditionally_complete_lattice.lean : line 748 : ERR_LIN : Line has mo
 src/order/conditionally_complete_lattice.lean : line 760 : ERR_LIN : Line has more than 100 characters
 src/order/conditionally_complete_lattice.lean : line 891 : ERR_LIN : Line has more than 100 characters
 src/order/directed.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/order/filter/extr.lean : line 309 : ERR_LIN : Line has more than 100 characters
-src/order/filter/extr.lean : line 66 : ERR_LIN : Line has more than 100 characters
-src/order/filter/lift.lean : line 153 : ERR_LIN : Line has more than 100 characters
-src/order/filter/lift.lean : line 261 : ERR_LIN : Line has more than 100 characters
-src/order/filter/lift.lean : line 276 : ERR_LIN : Line has more than 100 characters
-src/order/filter/lift.lean : line 342 : ERR_LIN : Line has more than 100 characters
 src/order/filter/partial.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/order/fixed_points.lean : line 203 : ERR_LIN : Line has more than 100 characters
 src/order/fixed_points.lean : line 207 : ERR_LIN : Line has more than 100 characters
@@ -213,11 +164,6 @@ src/order/preorder_hom.lean : line 124 : ERR_LIN : Line has more than 100 charac
 src/order/preorder_hom.lean : line 131 : ERR_LIN : Line has more than 100 characters
 src/order/rel_iso.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/order/zorn.lean : line 11 : ERR_MOD : Module docstring missing, or too late
-src/set_theory/cardinal.lean : line 1156 : ERR_LIN : Line has more than 100 characters
-src/set_theory/cardinal.lean : line 1160 : ERR_LIN : Line has more than 100 characters
-src/set_theory/cardinal.lean : line 136 : ERR_LIN : Line has more than 100 characters
-src/set_theory/cardinal.lean : line 498 : ERR_LIN : Line has more than 100 characters
-src/set_theory/cardinal.lean : line 986 : ERR_LIN : Line has more than 100 characters
 src/set_theory/game/impartial.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/set_theory/game/nim.lean : line 83 : ERR_LIN : Line has more than 100 characters
 src/set_theory/game/nim.lean : line 86 : ERR_LIN : Line has more than 100 characters
@@ -242,9 +188,7 @@ src/tactic/cache.lean : line 87 : ERR_LIN : Line has more than 100 characters
 src/tactic/chain.lean : line 13 : ERR_LIN : Line has more than 100 characters
 src/tactic/chain.lean : line 32 : ERR_LIN : Line has more than 100 characters
 src/tactic/chain.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/tactic/chain.lean : line 87 : ERR_LIN : Line has more than 100 characters
 src/tactic/converter/binders.lean : line 10 : ERR_MOD : Module docstring missing, or too late
-src/tactic/converter/binders.lean : line 31 : ERR_LIN : Line has more than 100 characters
 src/tactic/converter/interactive.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/tactic/converter/interactive.lean : line 53 : ERR_LIN : Line has more than 100 characters
 src/tactic/converter/old_conv.lean : line 272 : ERR_LIN : Line has more than 100 characters
@@ -256,20 +200,12 @@ src/tactic/delta_instance.lean : line 67 : ERR_LIN : Line has more than 100 char
 src/tactic/delta_instance.lean : line 75 : ERR_LIN : Line has more than 100 characters
 src/tactic/delta_instance.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/elide.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/tactic/equiv_rw.lean : line 174 : ERR_LIN : Line has more than 100 characters
-src/tactic/equiv_rw.lean : line 223 : ERR_LIN : Line has more than 100 characters
-src/tactic/equiv_rw.lean : line 260 : ERR_LIN : Line has more than 100 characters
-src/tactic/equiv_rw.lean : line 42 : ERR_LIN : Line has more than 100 characters
-src/tactic/equiv_rw.lean : line 97 : ERR_LIN : Line has more than 100 characters
+src/tactic/equiv_rw.lean : line 225 : ERR_LIN : Line has more than 100 characters
 src/tactic/ext.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/tactic/fin_cases.lean : line 120 : ERR_LIN : Line has more than 100 characters
 src/tactic/fin_cases.lean : line 13 : ERR_MOD : Module docstring missing, or too late
 src/tactic/find.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/tactic/find_unused.lean : line 44 : ERR_LIN : Line has more than 100 characters
-src/tactic/finish.lean : line 315 : ERR_LIN : Line has more than 100 characters
-src/tactic/finish.lean : line 402 : ERR_LIN : Line has more than 100 characters
 src/tactic/generalizes.lean : line 118 : ERR_LIN : Line has more than 100 characters
-src/tactic/group.lean : line 36 : ERR_LIN : Line has more than 100 characters
 src/tactic/hint.lean : line 57 : ERR_LIN : Line has more than 100 characters
 src/tactic/hint.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/induction.lean : line 1252 : ERR_RNT : Reserved notation outside tactic.reserved_notation
@@ -296,20 +232,6 @@ src/tactic/lean_core_docs.lean : line 733 : ERR_LIN : Line has more than 100 cha
 src/tactic/lean_core_docs.lean : line 766 : ERR_LIN : Line has more than 100 characters
 src/tactic/lift.lean : line 95 : ERR_LIN : Line has more than 100 characters
 src/tactic/linarith/elimination.lean : line 121 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/frontend.lean : line 156 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/frontend.lean : line 251 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/frontend.lean : line 257 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/frontend.lean : line 259 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/frontend.lean : line 260 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/lemmas.lean : line 22 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/lemmas.lean : line 23 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/lemmas.lean : line 26 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/lemmas.lean : line 27 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/lemmas.lean : line 31 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/lemmas.lean : line 34 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/lemmas.lean : line 37 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/lemmas.lean : line 74 : ERR_LIN : Line has more than 100 characters
-src/tactic/linarith/lemmas.lean : line 79 : ERR_LIN : Line has more than 100 characters
 src/tactic/linarith/parsing.lean : line 19 : ERR_LIN : Line has more than 100 characters
 src/tactic/linarith/preprocessing.lean : line 223 : ERR_LIN : Line has more than 100 characters
 src/tactic/linarith/preprocessing.lean : line 254 : ERR_LIN : Line has more than 100 characters
@@ -340,16 +262,11 @@ src/tactic/monotonicity/interactive.lean : line 468 : ERR_LIN : Line has more th
 src/tactic/monotonicity/interactive.lean : line 489 : ERR_LIN : Line has more than 100 characters
 src/tactic/monotonicity/lemmas.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/tactic/noncomm_ring.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/tactic/norm_cast.lean : line 561 : ERR_LIN : Line has more than 100 characters
-src/tactic/norm_cast.lean : line 757 : ERR_LIN : Line has more than 100 characters
 src/tactic/nth_rewrite/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/nth_rewrite/congr.lean : line 10 : ERR_MOD : Module docstring missing, or too late
-src/tactic/nth_rewrite/default.lean : line 110 : ERR_LIN : Line has more than 100 characters
-src/tactic/nth_rewrite/default.lean : line 113 : ERR_LIN : Line has more than 100 characters
 src/tactic/omega/clause.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/omega/coeffs.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/omega/eq_elim.lean : line 7 : ERR_MOD : Module docstring missing, or too late
-src/tactic/omega/find_ees.lean : line 152 : ERR_LIN : Line has more than 100 characters
 src/tactic/omega/find_ees.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/omega/find_scalars.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/omega/int/dnf.lean : line 7 : ERR_MOD : Module docstring missing, or too late
@@ -360,30 +277,20 @@ src/tactic/omega/lin_comb.lean : line 7 : ERR_MOD : Module docstring missing, or
 src/tactic/omega/main.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/omega/misc.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/omega/nat/dnf.lean : line 7 : ERR_MOD : Module docstring missing, or too late
-src/tactic/omega/nat/dnf.lean : line 76 : ERR_LIN : Line has more than 100 characters
 src/tactic/omega/nat/form.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/omega/nat/main.lean : line 7 : ERR_MOD : Module docstring missing, or too late
-src/tactic/omega/nat/main.lean : line 97 : ERR_LIN : Line has more than 100 characters
 src/tactic/omega/nat/neg_elim.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/omega/nat/preterm.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/omega/nat/sub_elim.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/omega/prove_unsats.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/omega/term.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/tactic/push_neg.lean : line 12 : ERR_MOD : Module docstring missing, or too late
-src/tactic/push_neg.lean : line 183 : ERR_LIN : Line has more than 100 characters
-src/tactic/push_neg.lean : line 184 : ERR_LIN : Line has more than 100 characters
-src/tactic/push_neg.lean : line 186 : ERR_LIN : Line has more than 100 characters
-src/tactic/push_neg.lean : line 187 : ERR_LIN : Line has more than 100 characters
+src/tactic/push_neg.lean : line 188 : ERR_LIN : Line has more than 100 characters
+src/tactic/push_neg.lean : line 189 : ERR_LIN : Line has more than 100 characters
 src/tactic/restate_axiom.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/rewrite.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/rewrite_all/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/tactic/ring.lean : line 521 : ERR_LIN : Line has more than 100 characters
-src/tactic/ring.lean : line 621 : ERR_LIN : Line has more than 100 characters
-src/tactic/ring2.lean : line 482 : ERR_LIN : Line has more than 100 characters
-src/tactic/ring_exp.lean : line 1549 : ERR_LIN : Line has more than 100 characters
 src/tactic/show_term.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/tactic/simp_result.lean : line 94 : ERR_LIN : Line has more than 100 characters
-src/tactic/simp_rw.lean : line 44 : ERR_LIN : Line has more than 100 characters
 src/tactic/simpa.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/simps.lean : line 430 : ERR_LIN : Line has more than 100 characters
 src/tactic/simps.lean : line 464 : ERR_LIN : Line has more than 100 characters
@@ -463,12 +370,10 @@ src/topology/metric_space/gromov_hausdorff.lean : line 62 : ERR_LIN : Line has m
 src/topology/omega_complete_partial_order.lean : line 85 : ERR_LIN : Line has more than 100 characters
 src/topology/separation.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/topology/sheaves/forget.lean : line 147 : ERR_LIN : Line has more than 100 characters
-src/topology/sheaves/presheaf_of_functions.lean : line 80 : ERR_LIN : Line has more than 100 characters
 src/topology/sheaves/sheaf.lean : line 89 : ERR_LIN : Line has more than 100 characters
 src/topology/sheaves/sheaf.lean : line 91 : ERR_LIN : Line has more than 100 characters
 src/topology/sheaves/sheaf_condition/equalizer_products.lean : line 230 : ERR_LIN : Line has more than 100 characters
 src/topology/sheaves/sheaf_condition/equalizer_products.lean : line 231 : ERR_LIN : Line has more than 100 characters
-src/topology/sheaves/sheaf_of_functions.lean : line 168 : ERR_LIN : Line has more than 100 characters
 src/topology/sheaves/stalks.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/topology/sheaves/stalks.lean : line 127 : ERR_LIN : Line has more than 100 characters
 src/topology/sheaves/stalks.lean : line 132 : ERR_LIN : Line has more than 100 characters