(no)lint

mattrobball · mattrobball · commit be3ad6aec433 · 2023-08-11T20:28:19.000-04:00
diff --git a/Mathlib/Algebra/Category/GroupCat/Limits.lean b/Mathlib/Algebra/Category/GroupCat/Limits.lean
@@ -474,4 +474,6 @@ def kernelIsoKerOver {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.kernel_iso_ker_over AddCommGroupCat.kernelIsoKerOver
 
+attribute [nolint simpNF] AddCommGroupCat.kernelIsoKerOver_hom_left_apply_coe
+
 end AddCommGroupCat
diff --git a/Mathlib/Algebra/Lie/Subalgebra.lean b/Mathlib/Algebra/Lie/Subalgebra.lean
@@ -193,7 +193,7 @@ theorem mk_coe (S : Set L) (h₁ h₂ h₃ h₄) :
   rfl
 #align lie_subalgebra.mk_coe LieSubalgebra.mk_coe
 
-@[simp]
+@[simp, nolint simpVarHead]
 theorem coe_to_submodule_mk (p : Submodule R L) (h) :
     (({ p with lie_mem' := h } : LieSubalgebra R L) : Submodule R L) = p := by
   cases p
diff --git a/Mathlib/Algebra/Lie/Submodule.lean b/Mathlib/Algebra/Lie/Submodule.lean
@@ -123,7 +123,7 @@ theorem coe_toSet_mk (S : Set M) (h₁ h₂ h₃ h₄) :
   rfl
 #align lie_submodule.coe_to_set_mk LieSubmodule.coe_toSet_mk
 
-@[simp]
+@[simp, nolint simpVarHead]
 theorem coe_toSubmodule_mk (p : Submodule R M) (h) :
     (({ p with lie_mem := h } : LieSubmodule R L M) : Submodule R M) = p := by cases p; rfl
 #align lie_submodule.coe_to_submodule_mk LieSubmodule.coe_toSubmodule_mk
@@ -1285,3 +1285,4 @@ theorem LieIdeal.topEquiv_apply (x : (⊤ : LieIdeal R L)) : LieIdeal.topEquiv x
 #align lie_ideal.top_equiv_apply LieIdeal.topEquiv_apply
 
 end TopEquiv
+
diff --git a/Mathlib/Analysis/NormedSpace/AffineIsometry.lean b/Mathlib/Analysis/NormedSpace/AffineIsometry.lean
@@ -887,6 +887,9 @@ noncomputable def equivMapOfInjective (E : AffineSubspace 𝕜 P₁) [Nonempty E
     map_vadd' := fun p v => Subtype.ext <| φ.map_vadd p v }
 #align affine_subspace.equiv_map_of_injective AffineSubspace.equivMapOfInjective
 
+attribute [nolint simpNF] AffineSubspace.equivMapOfInjective_invFun_coe
+attribute [nolint simpNF] AffineSubspace.linear_equivMapOfInjective_symm_apply_coe
+
 /-- Restricts an affine isometry to an affine isometry equivalence between a nonempty affine
 subspace `E` and its image.
 
