chore(Data/Finsupp): rename mapDomain_notin_range to mapDomain_of_notMem_range (leanprover-community#41766)

... so that this follows the naming convention. Same for `embDomain` and for `HahnSeries`.

Author: YaelDillies

Mathlib/Algebra/Group/Finsupp.lean

@@ -137,7 +137,7 @@ def embDomain.addMonoidHom (f : ι ↪ F) : (ι →₀ M) →+ F →₀ M where
     by_cases h : b ∈ Set.range f
     · rcases h with ⟨a, rfl⟩
       simp
-    · simp only [coe_add, Pi.add_apply, embDomain_notin_range _ _ _ h, add_zero]
+    · simp only [coe_add, Pi.add_apply, embDomain_of_notMem_range _ _ _ h, add_zero]
 
 @[simp]
 lemma embDomain_add (f : ι ↪ F) (v w : ι →₀ M) :

Mathlib/Analysis/InnerProductSpace/SingularValues.lean

@@ -121,7 +121,7 @@ theorem singularValues_of_lt {n : ℕ} (hn : finrank 𝕜 E = n) {i : ℕ} (hi :
   T.singularValues_fin hn ⟨i, hi⟩
 
 theorem singularValues_of_finrank_le {i : ℕ} (hi : finrank 𝕜 E ≤ i) : T.singularValues i = 0 := by
-  apply Finsupp.embDomain_notin_range
+  apply Finsupp.embDomain_of_notMem_range
   simp [hi]
 
 theorem sq_singularValues_fin {n : ℕ} (hn : finrank 𝕜 E = n) (i : Fin n) :

Mathlib/Combinatorics/Nullstellensatz.lean

@@ -189,7 +189,7 @@ private lemma Alon.of_mem_P_support {ι : Type*} (i : ι) (S : Finset R) (m : ι
     ext j
     by_cases hj : j = i
     · rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]
-    · rw [mapDomain_notin_range, single_eq_of_ne hj]
+    · rw [mapDomain_of_notMem_range, single_eq_of_ne hj]
       simp [Set.range_const, Set.mem_singleton_iff, hj]
 
 variable [Finite σ]

Mathlib/Data/Finsupp/Basic.lean

@@ -281,12 +281,14 @@ lemma mapDomain_of_not_mem_image_support {f : α → β} {x : α →₀ M} {b :
   rw [mapDomain, sum_apply, sum, Finset.sum_eq_zero]
   exact fun a ha ↦ single_eq_of_ne fun eq => hb <| eq ▸ Set.mem_image_of_mem _ ha
 
-theorem mapDomain_notin_range {f : α → β} (x : α →₀ M) (a : β) (h : a ∉ Set.range f) :
+theorem mapDomain_of_notMem_range {f : α → β} (x : α →₀ M) (a : β) (h : a ∉ Set.range f) :
     mapDomain f x a = 0 :=
   mapDomain_of_not_mem_image_support <| by grw [Set.image_subset_range]; exact h
 
+@[deprecated (since := "2026-07-15")] alias mapDomain_notin_range := mapDomain_of_notMem_range
+
 lemma mem_range_of_mapDomain_ne_zero {f : α → β} {x : α →₀ M} {b : β} (h : mapDomain f x b ≠ 0) :
-    b ∈ Set.range f := by contrapose! h; exact mapDomain_notin_range _ _ h
+    b ∈ Set.range f := by contrapose! h; exact mapDomain_of_notMem_range _ _ h
 
 @[simp]
 theorem mapDomain_id : mapDomain id v = v :=
@@ -421,7 +423,7 @@ theorem embDomain_eq_mapDomain (f : α ↪ β) (v : α →₀ M) : embDomain f v
   by_cases h : a ∈ Set.range f
   · rcases h with ⟨a, rfl⟩
     rw [mapDomain_apply f.injective, embDomain_apply_self]
-  · rw [mapDomain_notin_range, embDomain_notin_range] <;> assumption
+  · rw [mapDomain_of_notMem_range, embDomain_of_notMem_range] <;> assumption
 
 @[to_additive]
 theorem prod_mapDomain_index_inj [CommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N}
@@ -546,7 +548,7 @@ lemma embDomain_comapDomain {f : α ↪ β} {g : β →₀ M} (hg : ↑g.support
   · obtain ⟨a, rfl⟩ := hb
     rw [embDomain_apply_self, comapDomain_apply]
   · replace hg : g b = 0 := notMem_support_iff.mp <| mt (hg ·) hb
-    rw [embDomain_notin_range _ _ _ hb, hg]
+    rw [embDomain_of_notMem_range _ _ _ hb, hg]
 
 @[simp]
 theorem comapDomain_embDomain (f : α ↪ β) (l : α →₀ M) :
@@ -625,7 +627,7 @@ theorem comapDomain_mapDomain (hf : Function.Injective f) (l : α →₀ M) :
 
 lemma mem_range_mapDomain_iff (hf : Function.Injective f) (x : β →₀ M) :
     x ∈ Set.range (Finsupp.mapDomain f) ↔ ∀ b ∉ Set.range f, x b = 0 := by
-  refine ⟨fun ⟨y, hy⟩ x hx ↦ hy ▸ Finsupp.mapDomain_notin_range y x hx, fun h ↦ ?_⟩
+  refine ⟨fun ⟨y, hy⟩ x hx ↦ hy ▸ Finsupp.mapDomain_of_notMem_range y x hx, fun h ↦ ?_⟩
   refine ⟨Finsupp.comapDomain f x hf.injOn, Finsupp.mapDomain_comapDomain f hf _ fun i hi ↦ ?_⟩
   by_contra hc
   simp only [Finset.mem_coe, Finsupp.mem_support_iff, ne_eq] at hi
@@ -1066,7 +1068,7 @@ lemma sumElim_inr (f : α →₀ γ) (g : β →₀ γ) (x : β) : sumElim f g (
 
 lemma sumElim_eq_add [AddCommMonoid M] (f : α →₀ M) (g : β →₀ M) :
     sumElim f g = mapDomain Sum.inl f + mapDomain Sum.inr g := by
-  ext (_ | _) <;> simp [mapDomain_notin_range, Sum.inl_injective, Sum.inr_injective]
+  ext (_ | _) <;> simp [mapDomain_of_notMem_range, Sum.inl_injective, Sum.inr_injective]
 
 @[simp] lemma mapDomain_swap_sumElim [AddCommMonoid M] (f : α →₀ M) (g : β →₀ M) :
     mapDomain Sum.swap (sumElim f g) = sumElim g f := by
@@ -1224,7 +1226,7 @@ theorem extendDomain_eq_embDomain_subtype (f : Subtype P →₀ M) :
   by_cases h : P a
   · refine Eq.trans ?_ (embDomain_apply_self (.subtype P) f (Subtype.mk a h)).symm
     simp [h]
-  · rw [embDomain_notin_range] <;> simp [*]
+  · rw [embDomain_of_notMem_range] <;> simp [*]
 
 theorem support_extendDomain_subset (f : Subtype P →₀ M) :
     ↑(f.extendDomain).support ⊆ {x | P x} := by

Mathlib/Data/Finsupp/Defs.lean

@@ -437,9 +437,11 @@ theorem embDomain_apply_self (f : α ↪ β) (v : α →₀ M) (a : α) : embDom
   grind
 
 @[grind =>]
-theorem embDomain_notin_range (f : α ↪ β) (v : α →₀ M) (a : β) (h : a ∉ Set.range f) :
+theorem embDomain_of_notMem_range (f : α ↪ β) (v : α →₀ M) (a : β) (h : a ∉ Set.range f) :
     embDomain f v a = 0 := by grind [embDomain]
 
+@[deprecated (since := "2026-07-15")] alias embDomain_notin_range := embDomain_of_notMem_range
+
 theorem embDomain_injective (f : α ↪ β) : Function.Injective (embDomain f : (α →₀ M) → β →₀ M) :=
   fun l₁ l₂ h => ext fun a => by simpa only [embDomain_apply_self] using DFunLike.ext_iff.1 h (f a)
 

Mathlib/Data/Finsupp/Option.lean

@@ -90,7 +90,7 @@ theorem some_single_some (a : α) (m : M) :
   ext; rw [some_apply]; exact embDomain_apply_self _ _ _
 
 @[simp] lemma embDomain_some_none (f : α →₀ M) : f.embDomain .some .none = 0 :=
-  embDomain_notin_range _ _ _ (by simp)
+  embDomain_of_notMem_range _ _ _ (by simp)
 
 @[simp]
 theorem embDomain_some_some (f : α →₀ M) (x) : f.embDomain .some (.some x) = f x := by

Mathlib/Data/Finsupp/Order.lean

@@ -291,7 +291,7 @@ lemma mapDomain_tsub {f : ι → κ} (h : f.Injective) (f1 f2 : ι →₀ α) :
     (f1 - f2).mapDomain f = f1.mapDomain f - f2.mapDomain f := by
   ext y
   by_cases! hy : y ∉ Set.range f
-  · simp [mapDomain_notin_range _ _ hy]
+  · simp [mapDomain_of_notMem_range _ _ hy]
   · obtain ⟨x, rfl⟩ := hy
     simp [mapDomain_apply h]
 

Mathlib/Data/Finsupp/Sigma.lean

@@ -53,7 +53,7 @@ theorem embSigma_apply [DecidableEq κ] {k : κ} (f : ι k →₀ M) (i : Σ k,
     simp only [embSigma, Embedding.sigmaMk]
     apply embDomain_apply_self
   · simp only [embSigma, Embedding.sigmaMk]
-    rw [embDomain_notin_range]
+    rw [embDomain_of_notMem_range]
     simp_all
 
 @[simp]
@@ -65,7 +65,7 @@ theorem embSigma_apply_self {k : κ} (f : ι k →₀ M) (i : ι k) :
 /-- Values of `embSigma f` at indices outside the `k`-th summand are zero. -/
 theorem embSigma_apply_of_ne {k k' : κ} (f : ι k →₀ M) (hk : k' ≠ k) (i : ι k') :
     embSigma f ⟨k', i⟩ = 0 := by
-  apply embDomain_notin_range
+  apply embDomain_of_notMem_range
   grind
 
 @[simp, grind =]

Mathlib/Data/List/ToFinsupp.lean

@@ -99,7 +99,7 @@ theorem toFinsupp_append {R : Type*} [AddZeroClass R] (l₁ l₂ : List R)
   simp only [toFinsupp_apply, Finsupp.add_apply]
   cases lt_or_ge n l₁.length with
   | inl h =>
-    rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
+    rw [getD_append _ _ _ _ h, Finsupp.embDomain_of_notMem_range, add_zero]
     rintro ⟨k, rfl : length l₁ + k = n⟩
     lia
   | inr h =>

Mathlib/RingTheory/Extension/Generators.lean

@@ -552,7 +552,7 @@ lemma toComp_toAlgHom_monomial (Q : Generators S T ι') (P : Generators R S ι)
     simp [rename_eq_aeval]
     rfl
   · ext f (i₁ | i₂) <;>
-      simp [Finsupp.mapDomain_notin_range, Finsupp.mapDomain_apply Sum.inr_injective]
+      simp [Finsupp.mapDomain_of_notMem_range, Finsupp.mapDomain_apply Sum.inr_injective]
 
 @[simp]
 lemma toAlgHom_ofComp_rename (Q : Generators S T ι') (P : Generators R S ι) (p : P.Ring) :