From 9b11656c0355e057d739c644878cc1d62c47f1b7 Mon Sep 17 00:00:00 2001
From: leanprover-community-bot <leanprover.community@gmail.com>
Date: Mon, 5 Sep 2022 05:16:33 +0000
Subject: [PATCH] chore(scripts): update nolints.txt (#16384)

I am happy to remove some nolints for you!
---
 scripts/nolints.txt | 70 ---------------------------------------------
 1 file changed, 70 deletions(-)

diff --git a/scripts/nolints.txt b/scripts/nolints.txt
index 35424dd9601a4..39e90c94e7f75 100644
--- a/scripts/nolints.txt
+++ b/scripts/nolints.txt
@@ -423,82 +423,16 @@ apply_nolint subgroup.card_subgroup_dvd_card to_additive_doc
 -- group_theory/group_action/sub_mul_action.lean
 apply_nolint sub_mul_action.has_zero fails_quickly
 
--- linear_algebra/affine_space/affine_subspace.lean
-apply_nolint affine_span.nonempty fails_quickly
-apply_nolint affine_subspace.to_add_torsor fails_quickly
-
 -- linear_algebra/affine_space/basis.lean
 apply_nolint affine_basis.affine_independent_of_to_matrix_right_inv fintype_finite
 apply_nolint affine_basis.affine_span_eq_top_of_to_matrix_left_inv fintype_finite
 apply_nolint affine_basis.ext_elem fintype_finite
 
--- linear_algebra/affine_space/finite_dimensional.lean
-apply_nolint finite_dimensional_direction_affine_span_image_of_fintype fintype_finite
-apply_nolint finite_dimensional_direction_affine_span_of_fintype fintype_finite
-apply_nolint finite_dimensional_vector_span_image_of_fintype fintype_finite
-apply_nolint finite_dimensional_vector_span_of_fintype fintype_finite
-
--- linear_algebra/alternating.lean
-apply_nolint basis.ext_alternating fintype_finite
-
--- linear_algebra/determinant.lean
-apply_nolint alternating_map.map_basis_eq_zero_iff fintype_finite
-apply_nolint alternating_map.map_basis_ne_zero_iff fintype_finite
-apply_nolint linear_map.det_zero' fintype_finite
-
--- linear_algebra/dimension.lean
-apply_nolint dim_pi fintype_finite
-
--- linear_algebra/dual.lean
-apply_nolint basis.dual_dim_eq fintype_finite
-apply_nolint basis.eval_range fintype_finite
-apply_nolint basis.to_dual_range fintype_finite
-apply_nolint basis.total_coord fintype_finite
-
--- linear_algebra/finsupp_vector_space.lean
-apply_nolint cardinal_lt_aleph_0_of_finite_dimensional fintype_finite
-
--- linear_algebra/free_module/finite/basic.lean
-apply_nolint module.finite.matrix fintype_finite
-apply_nolint module.finite.of_basis fintype_finite
-
 -- linear_algebra/free_module/pid.lean
-apply_nolint ideal.exists_smith_normal_form fintype_finite
 apply_nolint submodule.basis_of_pid_aux fintype_finite
 apply_nolint submodule.exists_smith_normal_form_of_le fintype_finite
 apply_nolint submodule.nonempty_basis_of_pid fintype_finite
 
--- linear_algebra/free_module/rank.lean
-apply_nolint module.free.rank_matrix fintype_finite
-apply_nolint module.free.rank_matrix' fintype_finite
-apply_nolint module.free.rank_matrix'' fintype_finite
-apply_nolint module.free.rank_pi_fintype fintype_finite
-
--- linear_algebra/matrix/finite_dimensional.lean
-apply_nolint matrix.finite_dimensional fintype_finite
-
--- linear_algebra/matrix/reindex.lean
-apply_nolint matrix.mul_reindex_linear_equiv_one fintype_finite
-
--- linear_algebra/matrix/transvection.lean
-apply_nolint matrix.update_row_eq_transvection fintype_finite
-
--- linear_algebra/multilinear/basis.lean
-apply_nolint basis.ext_multilinear fintype_finite
-
--- linear_algebra/multilinear/finite_dimensional.lean
-apply_nolint module.finite.multilinear_map fintype_finite
-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/std_basis.lean
-apply_nolint linear_map.supr_range_std_basis fintype_finite
-
--- linear_algebra/trace.lean
-apply_nolint linear_map.trace_eq_contract_of_basis fintype_finite
-
 -- logic/relator.lean
 apply_nolint relator.bi_total doc_blame
 apply_nolint relator.bi_unique doc_blame
@@ -533,10 +467,6 @@ apply_nolint tactic.coinductive_predicate doc_blame
 apply_nolint tactic.interactive.coinduction doc_blame
 apply_nolint tactic.mono doc_blame
 
--- model_theory/definability.lean
-apply_nolint set.definable.image_comp fintype_finite
-apply_nolint set.definable.image_comp_embedding fintype_finite
-
 -- model_theory/direct_limit.lean
 apply_nolint first_order.language.direct_limit.exists_quotient_mk_sigma_mk_eq fintype_finite
 apply_nolint first_order.language.direct_limit.exists_unify_eq fintype_finite