nolint

Author: YaelDillies

Mathlib/Data/Finsupp/Basic.lean

@@ -285,7 +285,9 @@ theorem mapDomain_notin_range {f : α → β} (x : α →₀ M) (a : β) (h : a
     mapDomain f x a = 0 :=
   mapDomain_of_not_mem_image_support <| by grw [Set.image_subset_range]; exact h
 
-@[simp high] lemma mapDomain_id : mapDomain id v = v := sum_single _
+-- The linter complains that `mapDomain_id` can be proved from `mapDomain_fun_id` and `id_eq`
+-- but this isn't true (at least within most of mathlib)
+@[simp, nolint simpNF] lemma mapDomain_id : mapDomain id v = v := sum_single _
 @[simp] lemma mapDomain_fun_id : mapDomain (fun x ↦ x) v = v := sum_single _
 
 lemma mapDomain_fun_comp (f : α → β) (g : β → γ) :