diff --git a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
index 72eecf74a0002c..04fc6ed3e31ef9 100644
--- a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
+++ b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@@ -14,6 +14,8 @@ public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
 public import Mathlib.Data.Multiset.Powerset
 public import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
 
+import Mathlib.Algebra.Order.Monoid.OrderDual
+
 /-!
 # Big operators on a finset in ordered groups
 
@@ -226,7 +228,7 @@ alias prod_le_prod_of_injOn' := prod_le_prod_of_injOn
 
 @[to_additive]
 theorem prod_eq_one_iff_of_one_le {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
-    {f : ι → N} {s : Finset ι} [MulLeftMono N] :
+    {f : ι → N} {s : Finset ι} [IsOrderedMonoid N] :
     (∀ i ∈ s, 1 ≤ f i) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) := by
   classical
     refine Finset.induction_on s
@@ -240,7 +242,7 @@ theorem prod_eq_one_iff_of_one_le {ι : Type u_1} {N : Type u_5} [CommMonoid N]
 
 @[to_additive sum_pos_iff_of_nonneg]
 lemma one_lt_prod_iff_of_one_le {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
-    {f : ι → N} {s : Finset ι} [MulLeftMono N] (hf : ∀ x ∈ s, 1 ≤ f x) :
+    {f : ι → N} {s : Finset ι} [IsOrderedMonoid N] (hf : ∀ x ∈ s, 1 ≤ f x) :
     1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x := by
   have hsum : 1 ≤ ∏ x ∈ s, f x := one_le_prod hf
   rw [hsum.lt_iff_ne', Ne, prod_eq_one_iff_of_one_le hf, not_forall]
@@ -248,7 +250,7 @@ lemma one_lt_prod_iff_of_one_le {ι : Type u_1} {N : Type u_5} [CommMonoid N] [P
 
 @[to_additive]
 theorem prod_eq_one_iff_of_le_one {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
-    {f : ι → N} {s : Finset ι} [MulLeftMono N] :
+    {f : ι → N} {s : Finset ι} [IsOrderedMonoid N] :
     (∀ i ∈ s, f i ≤ 1) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) :=
   prod_eq_one_iff_of_one_le (N := Nᵒᵈ)
 
@@ -256,7 +258,7 @@ theorem prod_eq_one_iff_of_le_one {ι : Type u_1} {N : Type u_5} [CommMonoid N]
 
 @[to_additive]
 lemma prod_lt_one_iff_of_le_one {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
-    {f : ι → N} {s : Finset ι} [MulLeftMono N] (hf : ∀ x ∈ s, f x ≤ 1) :
+    {f : ι → N} {s : Finset ι} [IsOrderedMonoid N] (hf : ∀ x ∈ s, f x ≤ 1) :
     ∏ x ∈ s, f x < 1 ↔ ∃ x ∈ s, f x < 1 :=
   one_lt_prod_iff_of_one_le (N := Nᵒᵈ) hf
 
@@ -668,7 +670,7 @@ section LinearOrderedCancelCommMonoid
 variable [CommMonoid M] [LinearOrder M] {f g : ι → M} {s : Finset ι}
 
 @[to_additive]
-theorem exists_lt_of_prod_lt [MulLeftMono M] (Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i) :
+theorem exists_lt_of_prod_lt [IsOrderedMonoid M] (Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i) :
     ∃ i ∈ s, f i < g i := by
   contrapose! Hlt with Hle
   exact prod_le_prod Hle
@@ -676,14 +678,14 @@ theorem exists_lt_of_prod_lt [MulLeftMono M] (Hlt : ∏ i ∈ s, f i < ∏ i ∈
 @[deprecated (since := "2026-09-01")] alias exists_lt_of_prod_lt' := exists_lt_of_prod_lt
 
 @[to_additive exists_pos_of_sum_zero_of_exists_nonzero]
-theorem exists_one_lt_of_prod_one_of_exists_ne_one [MulLeftMono M] (f : ι → M)
+theorem exists_one_lt_of_prod_one_of_exists_ne_one [IsOrderedMonoid M] (f : ι → M)
     (h₁ : ∏ i ∈ s, f i = 1) (h₂ : ∃ i ∈ s, f i ≠ 1) : ∃ i ∈ s, 1 < f i := by
   by_contra! h
   have : ¬ ∃ x ∈ s, f x < 1 := by simp [← prod_lt_one_iff_of_le_one h, h₁]
   grind
 
 @[to_additive exists_neg_of_sum_zero_of_exists_nonzero]
-theorem exists_lt_one_of_prod_one_of_exists_ne_one [MulLeftMono M] (f : ι → M)
+theorem exists_lt_one_of_prod_one_of_exists_ne_one [IsOrderedMonoid M] (f : ι → M)
     (h₁ : ∏ i ∈ s, f i = 1) (h₂ : ∃ i ∈ s, f i ≠ 1) : ∃ i ∈ s, f i < 1 :=
   exists_one_lt_of_prod_one_of_exists_ne_one (M := Mᵒᵈ) f h₁ h₂
 
@@ -748,12 +750,12 @@ lemma one_le_prod (hf : 1 ≤ f) : 1 ≤ ∏ i, f i := Finset.one_le_prod fun _
 
 @[to_additive]
 lemma prod_eq_one_iff_of_one_le {ι M : Type*} [Fintype ι] [CommMonoid M] [PartialOrder M]
-    [MulLeftMono M] {f : ι → M} (hf : 1 ≤ f) : ∏ i, f i = 1 ↔ f = 1 :=
+    [IsOrderedMonoid M] {f : ι → M} (hf : 1 ≤ f) : ∏ i, f i = 1 ↔ f = 1 :=
   (Finset.prod_eq_one_iff_of_one_le fun i _ ↦ hf i).trans <| by simp [funext_iff]
 
 @[to_additive]
 lemma prod_eq_one_iff_of_le_one {ι M : Type*} [Fintype ι] [CommMonoid M] [PartialOrder M]
-    [MulLeftMono M] {f : ι → M} (hf : f ≤ 1) : ∏ i, f i = 1 ↔ f = 1 :=
+    [IsOrderedMonoid M] {f : ι → M} (hf : f ≤ 1) : ∏ i, f i = 1 ↔ f = 1 :=
   (Finset.prod_eq_one_iff_of_le_one fun i _ ↦ hf i).trans <| by simp [funext_iff]
 
 end OrderedCommMonoid
diff --git a/Mathlib/Combinatorics/Nullstellensatz.lean b/Mathlib/Combinatorics/Nullstellensatz.lean
index 7b6aed3748fcd1..d32b00a5033741 100644
--- a/Mathlib/Combinatorics/Nullstellensatz.lean
+++ b/Mathlib/Combinatorics/Nullstellensatz.lean
@@ -187,7 +187,7 @@ private lemma Alon.of_mem_P_support {ι : Type*} (i : ι) (S : Finset R) (m : ι
   · rw [← hm]
     ext j
     by_cases hj : j = i
-    · rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]
+    · rw [hj, mapDomain_apply_of_injective (Function.injective_of_subsingleton _), single_eq_same]
     · rw [mapDomain_of_notMem_range, single_eq_of_ne hj]
       simp [Set.range_const, Set.mem_singleton_iff, hj]
 
diff --git a/Mathlib/Data/Finsupp/Basic.lean b/Mathlib/Data/Finsupp/Basic.lean
index cf448d98b45112..f08e2dca632d9f 100644
--- a/Mathlib/Data/Finsupp/Basic.lean
+++ b/Mathlib/Data/Finsupp/Basic.lean
@@ -263,13 +263,14 @@ section MapDomain
 
 variable [AddCommMonoid M] {v v₁ v₂ : α →₀ M}
 
-/-- Given `f : α → β` and `v : α →₀ M`, `mapDomain f v : β →₀ M`
-  is the finitely supported function whose value at `a : β` is the sum
-  of `v x` over all `x` such that `f x = a`. -/
-def mapDomain (f : α → β) (v : α →₀ M) : β →₀ M :=
-  v.sum fun a => single (f a)
+/-- Given `f : α → β` and `x : α →₀ M`, `mapDomain f x : β →₀ M` is the finitely supported function
+whose value at `b : β` is the sum of `v a` over all `a : α` such that `f a = b`. -/
+def mapDomain (f : α → β) (x : α →₀ M) : β →₀ M := x.sum fun a ↦ single (f a)
 
-@[simp] theorem mapDomain_apply {f : α → β} (hf : Function.Injective f) (x : α →₀ M) (a : α) :
+lemma mapDomain_apply (f : α → β) (x : α →₀ M) (b : β) :
+    mapDomain f x b = x.sum fun a m ↦ single (f a) m b := by simp [mapDomain]
+
+@[simp] theorem mapDomain_apply_of_injective {f : α → β} (hf : f.Injective) (x : α →₀ M) (a : α) :
     mapDomain f x (f a) = x a := by
   rw [mapDomain, sum_apply, sum_eq_single a, single_eq_same]
   · intro b _ hba
@@ -327,7 +328,7 @@ lemma mapDomain_sub {α β M : Type*} [AddCommGroup M] {v₁ v₂ : α →₀ M}
 theorem mapDomain_equiv_apply {f : α ≃ β} (x : α →₀ M) (a : β) :
     mapDomain f x a = x (f.symm a) := by
   conv_lhs => rw [← f.apply_symm_apply a]
-  exact mapDomain_apply f.injective _ _
+  exact mapDomain_apply_of_injective f.injective _ _
 
 @[simp] lemma support_mapDomain_embedding (f : α ↪ β) (x : α →₀ M) :
     (mapDomain f x).support = x.support.map f := by
@@ -422,7 +423,7 @@ theorem embDomain_eq_mapDomain (f : α ↪ β) (v : α →₀ M) : embDomain f v
   ext a
   by_cases h : a ∈ Set.range f
   · rcases h with ⟨a, rfl⟩
-    rw [mapDomain_apply f.injective, embDomain_apply_self]
+    rw [mapDomain_apply_of_injective f.injective, embDomain_apply_self]
   · rw [mapDomain_of_notMem_range, embDomain_of_notMem_range] <;> assumption
 
 @[to_additive]
@@ -435,7 +436,7 @@ theorem mapDomain_injective {f : α → β} (hf : Function.Injective f) :
   intro v₁ v₂ eq
   ext a
   have : mapDomain f v₁ (f a) = mapDomain f v₂ (f a) := by rw [eq]
-  rwa [mapDomain_apply hf, mapDomain_apply hf] at this
+  rwa [mapDomain_apply_of_injective hf, mapDomain_apply_of_injective hf] at this
 
 theorem mapDomain_surjective {f : α → β} (hf : f.Surjective) :
     (mapDomain (M := M) f).Surjective := by
@@ -517,10 +518,11 @@ theorem comapDomain_apply [Zero M] (f : α → β) (l : β →₀ M) (hf : Set.I
     (a : α) : comapDomain f l hf a = l (f a) :=
   rfl
 
-theorem sum_comapDomain [Zero M] [AddCommMonoid N] (f : α → β) (l : β →₀ M) (g : β → M → N)
+@[to_additive]
+theorem prod_comapDomain [Zero M] [CommMonoid N] (f : α → β) (l : β →₀ M) (g : β → M → N)
     (hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support) :
-    (comapDomain f l hf.injOn).sum (g ∘ f) = l.sum g :=
-  Finset.sum_preimage_of_bij f _ hf fun x => g x (l x)
+    (comapDomain f l hf.injOn).prod (g ∘ f) = l.prod g :=
+  Finset.prod_preimage_of_bij f _ hf fun x => g x (l x)
 
 theorem eq_zero_of_comapDomain_eq_zero [Zero M] (f : α → β) (l : β →₀ M)
     (hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support) : comapDomain f l hf.injOn = 0 → l = 0 := by
@@ -627,7 +629,7 @@ theorem mapDomain_comapDomain_nat_add_one (l : ℕ →₀ M) :
 
 theorem comapDomain_mapDomain (hf : Function.Injective f) (l : α →₀ M) :
     comapDomain f (mapDomain f l) hf.injOn = l := by
-  ext; rw [comapDomain_apply, mapDomain_apply hf]
+  ext; rw [comapDomain_apply, mapDomain_apply_of_injective hf]
 
 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
diff --git a/Mathlib/Data/Finsupp/Order.lean b/Mathlib/Data/Finsupp/Order.lean
index 06e72c9e815bc6..d6a2d9f5c50305 100644
--- a/Mathlib/Data/Finsupp/Order.lean
+++ b/Mathlib/Data/Finsupp/Order.lean
@@ -24,16 +24,21 @@ This file lifts order structures on `α` to `ι →₀ α`.
   functions.
 -/
 
-public section
-
-noncomputable section
-
 open Finset
 
-variable {ι κ α β : Type*}
+public noncomputable section
+
+variable {ι κ α β M : Type*}
 
 namespace Finsupp
 
+@[simp] lemma support_mapDomain_of_nonneg [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M]
+    [DecidableEq β] {x : α →₀ M} (hx : 0 ≤ x) (f : α → β) :
+    (mapDomain f x).support = x.support.image f := by
+  ext b
+  simp [mapDomain_apply, Finsupp.sum, single_apply]
+  grind [Finset.sum_eq_zero_iff_of_nonneg, Finsupp.le_def]
+
 /-! ### Order structures -/
 
 
@@ -293,7 +298,7 @@ lemma mapDomain_tsub {f : ι → κ} (h : f.Injective) (f1 f2 : ι →₀ α) :
   by_cases! hy : y ∉ Set.range f
   · simp [mapDomain_of_notMem_range _ _ hy]
   · obtain ⟨x, rfl⟩ := hy
-    simp [mapDomain_apply h]
+    simp [h]
 
 lemma embDomain_tsub (f : ι ↪ κ) (f1 f2 : ι →₀ α) :
     (f1 - f2).embDomain f = f1.embDomain f - f2.embDomain f := by
diff --git a/Mathlib/Data/Finsupp/SMul.lean b/Mathlib/Data/Finsupp/SMul.lean
index 064242391b0d2d..69a184bbaceadb 100644
--- a/Mathlib/Data/Finsupp/SMul.lean
+++ b/Mathlib/Data/Finsupp/SMul.lean
@@ -97,7 +97,7 @@ attribute [local instance] comapSMul comapMulAction comapDistribMulAction
 @[simp]
 theorem comapSMul_apply (g : G) (f : α →₀ M) (a : α) : (g • f) a = f (g⁻¹ • a) := by
   conv_lhs => rw [← smul_inv_smul g a]
-  exact mapDomain_apply (MulAction.injective g) _ (g⁻¹ • a)
+  exact mapDomain_apply_of_injective (MulAction.injective g) _ (g⁻¹ • a)
 
 end
 
diff --git a/Mathlib/RepresentationTheory/Basic.lean b/Mathlib/RepresentationTheory/Basic.lean
index ace88b2889c74b..6e15c6ef79c816 100644
--- a/Mathlib/RepresentationTheory/Basic.lean
+++ b/Mathlib/RepresentationTheory/Basic.lean
@@ -475,7 +475,7 @@ theorem coeff_ofMulAction {H : Type*} [MulAction G H] (g : G) (f : k[H]) (h : H)
   have hg : Function.Injective (g • · : H → H) := by
     intro h₁ h₂
     simp
-  simp [ofMulAction_def, Finsupp.mapDomain_apply, hg]
+  simp [ofMulAction_def, hg]
 
 @[deprecated (since := "2026-06-18")] alias ofMulAction_apply := coeff_ofMulAction
 
diff --git a/Mathlib/RingTheory/Extension/Generators.lean b/Mathlib/RingTheory/Extension/Generators.lean
index 5a15362f9248e3..cc4b34f3a3fbf7 100644
--- a/Mathlib/RingTheory/Extension/Generators.lean
+++ b/Mathlib/RingTheory/Extension/Generators.lean
@@ -554,8 +554,7 @@ lemma toComp_toAlgHom_monomial (Q : Generators S T ι') (P : Generators R S ι)
   · ext f (i₁ | i₂)
     simp [rename_eq_aeval]
     rfl
-  · ext f (i₁ | i₂) <;>
-      simp [Finsupp.mapDomain_of_notMem_range, Finsupp.mapDomain_apply Sum.inr_injective]
+  · ext f (i₁ | i₂) <;> simp [Finsupp.mapDomain_of_notMem_range, Sum.inr_injective]
 
 @[simp]
 lemma toAlgHom_ofComp_rename (Q : Generators S T ι') (P : Generators R S ι) (p : P.Ring) :
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 3af2093df89dcf..1a48e2502d24d9 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -436,7 +436,7 @@ def basis : Basis (Fin (natDegree f)) R S where
     ext i
     simp only [h.modByMonicHom_map, Finsupp.comapDomain_apply, Polynomial.toFinsupp_apply]
     rw [(Polynomial.modByMonic_eq_self_iff h.monic).mpr, Polynomial.coeff]
-    · rw [Finsupp.mapDomain_apply Fin.val_injective]
+    · rw [Finsupp.mapDomain_apply_of_injective Fin.val_injective]
     rw [degree_eq_natDegree h.monic.ne_zero, degree_lt_iff_coeff_zero]
     intro m hm
     rw [Polynomial.coeff]
diff --git a/Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean b/Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
index cdc22b64ba5e8c..377bb94c58397d 100644
--- a/Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
+++ b/Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
@@ -257,7 +257,7 @@ lemma IsSymmetric.antitone_supDegree [LinearOrder σ] {p : MvPolynomial σ R} (h
   refine ⟨i, fun k hk ↦ ?_, ?_⟩
   all_goals dsimp only [Pi.toLex_apply, ofLex_toLex]
   · conv_rhs => rw [← Equiv.swap_apply_of_ne_of_ne hk.ne (hk.trans_le hle).ne]
-    rw [Finsupp.mapDomain_apply (Equiv.injective _), supDegree]; rfl
+    rw [Finsupp.mapDomain_apply_of_injective (Equiv.injective _), supDegree]; rfl
   · apply hlt.trans_eq
     simp_rw [Finsupp.mapDomain_equiv_apply, Equiv.symm_swap, Equiv.swap_apply_left]