diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
index a84822245f2c57..20c3043dd90078 100644
--- a/Mathlib/Analysis/Normed/Group/Basic.lean
+++ b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -608,11 +608,12 @@ end NNNorm
 section ENorm
 
 @[to_additive (attr := simp) enorm_zero]
-lemma enorm_one' {E : Type*} [TopologicalSpace E] [ESeminormedMonoid E] : ‖(1 : E)‖ₑ = 0 := by
+lemma enorm_one' {E : Type*} [TopologicalSpace E] [Monoid E] [ESeminormedMonoid E] :
+    ‖(1 : E)‖ₑ = 0 := by
   rw [ESeminormedMonoid.enorm_zero]
 
 @[to_additive exists_enorm_lt]
-lemma exists_enorm_lt' (E : Type*) [TopologicalSpace E] [ESeminormedMonoid E]
+lemma exists_enorm_lt' (E : Type*) [TopologicalSpace E] [Monoid E] [ESeminormedMonoid E]
     [hbot : NeBot (𝓝[≠] (1 : E))] {c : ℝ≥0∞} (hc : c ≠ 0) : ∃ x ≠ (1 : E), ‖x‖ₑ < c :=
   frequently_iff_neBot.mpr hbot |>.and_eventually
     (ContinuousENorm.continuous_enorm.tendsto' 1 0 (by simp) |>.eventually_lt_const hc.bot_lt)
@@ -650,7 +651,7 @@ end ENorm
 
 section ESeminormedMonoid
 
-variable {E : Type*} [TopologicalSpace E] [ESeminormedMonoid E]
+variable {E : Type*} [TopologicalSpace E] [Monoid E] [ESeminormedMonoid E]
 
 @[to_additive enorm_add_le]
 lemma enorm_mul_le' (a b : E) : ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ := ESeminormedMonoid.enorm_mul_le a b
@@ -672,7 +673,7 @@ end ESeminormedMonoid
 
 section ENormedMonoid
 
-variable {E : Type*} [TopologicalSpace E] [ENormedMonoid E]
+variable {E : Type*} [TopologicalSpace E] [Monoid E] [ENormedMonoid E]
 
 @[to_additive (attr := simp) enorm_eq_zero]
 lemma enorm_eq_zero' {a : E} : ‖a‖ₑ = 0 ↔ a = 1 := by
@@ -752,7 +753,7 @@ end Induced
 section SeminormedCommGroup
 
 variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a b : E} {r : ℝ}
-variable {ε : Type*} [TopologicalSpace ε] [ESeminormedCommMonoid ε]
+variable {ε : Type*} [TopologicalSpace ε] [CommMonoid ε] [ESeminormedMonoid ε]
 
 @[to_additive]
 theorem dist_eq_norm_div (a b : E) : dist a b = ‖a / b‖ := by
@@ -804,7 +805,7 @@ theorem norm_multiset_sum_le {E} [SeminormedAddCommGroup E] (m : Multiset E) :
     ‖m.sum‖ ≤ (m.map fun x => ‖x‖).sum :=
   m.le_sum_of_subadditive norm norm_zero.le norm_add_le
 
-variable {ε : Type*} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] in
+variable {ε : Type*} [TopologicalSpace ε] [AddCommMonoid ε] [ESeminormedAddMonoid ε] in
 theorem enorm_multisetSum_le (m : Multiset ε) :
     ‖m.sum‖ₑ ≤ (m.map fun x => ‖x‖ₑ).sum :=
   m.le_sum_of_subadditive enorm enorm_zero.le enorm_add_le
@@ -813,13 +814,13 @@ theorem enorm_multisetSum_le (m : Multiset ε) :
 theorem norm_multiset_prod_le (m : Multiset E) : ‖m.prod‖ ≤ (m.map fun x => ‖x‖).sum :=
   m.apply_prod_le_sum_map _ norm_one'.le norm_mul_le'
 
-variable {ε : Type*} [TopologicalSpace ε] [ESeminormedCommMonoid ε] in
+variable {ε : Type*} [TopologicalSpace ε] [CommMonoid ε] [ESeminormedMonoid ε] in
 @[to_additive existing]
 theorem enorm_multisetProd_le (m : Multiset ε) :
     ‖m.prod‖ₑ ≤ (m.map fun x => ‖x‖ₑ).sum :=
   m.apply_prod_le_sum_map _ enorm_one'.le enorm_mul_le'
 
-variable {ε : Type*} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] in
+variable {ε : Type*} [TopologicalSpace ε] [AddCommMonoid ε] [ESeminormedAddMonoid ε] in
 @[bound]
 theorem enorm_sum_le (s : Finset ι) (f : ι → ε) :
     ‖∑ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ :=
diff --git a/Mathlib/Analysis/Normed/Group/Continuity.lean b/Mathlib/Analysis/Normed/Group/Continuity.lean
index e0f31ba15daa9e..d75521119b06db 100644
--- a/Mathlib/Analysis/Normed/Group/Continuity.lean
+++ b/Mathlib/Analysis/Normed/Group/Continuity.lean
@@ -135,11 +135,6 @@ instance NormedGroup.toENormedMonoid {F : Type*} [NormedGroup F] : ENormedMonoid
   enorm_eq_zero := by simp [enorm_eq_nnnorm]
   enorm_mul_le := by simp [enorm_eq_nnnorm, ← coe_add, nnnorm_mul_le']
 
-@[to_additive]
-instance NormedCommGroup.toENormedCommMonoid [NormedCommGroup E] : ENormedCommMonoid E where
-  __ := NormedGroup.toENormedMonoid
-  __ := ‹NormedCommGroup E›
-
 end Instances
 
 section SeminormedGroup
diff --git a/Mathlib/Analysis/Normed/Group/Defs.lean b/Mathlib/Analysis/Normed/Group/Defs.lean
index eb920d5fc2806c..f92e762bd66ba6 100644
--- a/Mathlib/Analysis/Normed/Group/Defs.lean
+++ b/Mathlib/Analysis/Normed/Group/Defs.lean
@@ -111,36 +111,30 @@ class ContinuousENorm (E : Type*) [TopologicalSpace E] extends ENorm E where
 /-- An e-seminormed monoid is an additive monoid endowed with a continuous enorm.
 Note that we do not ask for the enorm to be positive definite:
 non-trivial elements may have enorm zero. -/
-class ESeminormedAddMonoid (E : Type*) [TopologicalSpace E]
-    extends ContinuousENorm E, AddMonoid E where
+class ESeminormedAddMonoid (E : Type*) [TopologicalSpace E] [AddMonoid E]
+    extends ContinuousENorm E where
   enorm_zero : ‖(0 : E)‖ₑ = 0
   protected enorm_add_le : ∀ x y : E, ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
 
--- see Note [lower instance priority]
-attribute [instance 200] ESeminormedAddMonoid.toAddMonoid
-
 /-- An enormed monoid is an additive monoid endowed with a continuous enorm,
 which is positive definite: in other words, this is an `ESeminormedAddMonoid` with a positive
 definiteness condition added. -/
-class ENormedAddMonoid (E : Type*) [TopologicalSpace E]
+class ENormedAddMonoid (E : Type*) [TopologicalSpace E] [AddMonoid E]
     extends ESeminormedAddMonoid E where
   enorm_eq_zero : ∀ x : E, ‖x‖ₑ = 0 ↔ x = 0
 
 /-- An e-seminormed monoid is a monoid endowed with a continuous enorm.
 Note that we only ask for the enorm to be a semi-norm: non-trivial elements may have enorm zero. -/
 @[to_additive]
-class ESeminormedMonoid (E : Type*) [TopologicalSpace E] extends ContinuousENorm E, Monoid E where
+class ESeminormedMonoid (E : Type*) [TopologicalSpace E] [Monoid E] extends ContinuousENorm E where
   enorm_zero : ‖(1 : E)‖ₑ = 0
   enorm_mul_le : ∀ x y : E, ‖x * y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
 
--- see Note [lower instance priority]
-attribute [instance 200] ESeminormedMonoid.toMonoid
-
 /-- An enormed monoid is a monoid endowed with a continuous enorm,
 which is positive definite: in other words, this is an `ESeminormedMonoid` with a positive
 definiteness condition added. -/
 @[to_additive]
-class ENormedMonoid (E : Type*) [TopologicalSpace E] extends ESeminormedMonoid E where
+class ENormedMonoid (E : Type*) [TopologicalSpace E] [Monoid E] extends ESeminormedMonoid E where
   enorm_eq_zero : ∀ x : E, ‖x‖ₑ = 0 ↔ x = 1
 
 /-- An e-seminormed commutative monoid is an additive commutative monoid endowed with a continuous
@@ -149,35 +143,41 @@ enorm.
 We don't have `ESeminormedAddCommMonoid` extend `EMetricSpace`, since the canonical instance `ℝ≥0∞`
 is not an `EMetricSpace`. This is because `ℝ≥0∞` carries the order topology, which is distinct from
 the topology coming from `edist`. -/
-class ESeminormedAddCommMonoid (E : Type*) [TopologicalSpace E]
-  extends ESeminormedAddMonoid E, AddCommMonoid E where
-
--- see Note [lower instance priority]
-attribute [instance 200] ESeminormedAddCommMonoid.toAddCommMonoid
+@[deprecated "Use `[AddCommMonoid E] [ESeminormedAddMonoid E]` instead." (since := "2026-04-14")]
+structure ESeminormedAddCommMonoid (E : Type*) [TopologicalSpace E]
+  extends AddCommMonoid E, ESeminormedAddMonoid E where
 
+set_option linter.deprecated false in
 /-- An enormed commutative monoid is an additive commutative monoid
 endowed with a continuous enorm which is positive definite.
 
 We don't have `ENormedAddCommMonoid` extend `EMetricSpace`, since the canonical instance `ℝ≥0∞`
 is not an `EMetricSpace`. This is because `ℝ≥0∞` carries the order topology, which is distinct from
 the topology coming from `edist`. -/
-class ENormedAddCommMonoid (E : Type*) [TopologicalSpace E]
+@[deprecated "Use `[AddCommMonoid E] [ENormedAddMonoid E]` instead." (since := "2026-04-14")]
+structure ENormedAddCommMonoid (E : Type*) [TopologicalSpace E]
   extends ESeminormedAddCommMonoid E, ENormedAddMonoid E where
 
-/-- An e-seminormed commutative monoid is a commutative monoid endowed with a continuous enorm. -/
-@[to_additive]
-class ESeminormedCommMonoid (E : Type*) [TopologicalSpace E]
-  extends ESeminormedMonoid E, CommMonoid E where
+attribute [nolint docBlame] ENormedAddCommMonoid.toENormedAddMonoid
 
--- see Note [lower instance priority]
-attribute [instance 200] ESeminormedCommMonoid.toCommMonoid
+set_option linter.existingAttributeWarning false in
+/-- An e-seminormed commutative monoid is a commutative monoid endowed with a continuous enorm. -/
+@[to_additive,
+  deprecated "Use `[CommMonoid E] [ESeminormedMonoid E]` instead." (since := "2026-04-14")]
+structure ESeminormedCommMonoid (E : Type*) [TopologicalSpace E]
+  extends CommMonoid E, ESeminormedMonoid E where
 
+set_option linter.deprecated false in
+set_option linter.existingAttributeWarning false in
 /-- An enormed commutative monoid is a commutative monoid endowed with a continuous enorm
 which is positive definite. -/
-@[to_additive]
-class ENormedCommMonoid (E : Type*) [TopologicalSpace E]
+@[to_additive,
+  deprecated "Use `[CommMonoid E] [ENormedMonoid E]` instead." (since := "2026-04-14")]
+structure ENormedCommMonoid (E : Type*) [TopologicalSpace E]
   extends ESeminormedCommMonoid E, ENormedMonoid E where
 
+attribute [nolint docBlame] ENormedCommMonoid.toENormedMonoid
+
 /-- A seminormed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖`
 defines a pseudometric space structure. -/
 class SeminormedAddGroup (E : Type*) extends Norm E, AddGroup E, PseudoMetricSpace E where
diff --git a/Mathlib/Analysis/Normed/Group/Indicator.lean b/Mathlib/Analysis/Normed/Group/Indicator.lean
index c307ef50f4e45e..29595dbbb43236 100644
--- a/Mathlib/Analysis/Normed/Group/Indicator.lean
+++ b/Mathlib/Analysis/Normed/Group/Indicator.lean
@@ -23,7 +23,7 @@ open Set
 
 section ESeminormedAddMonoid
 
-variable {α ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε]
+variable {α ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
   {s t : Set α} (f : α → ε) (a : α)
 
 lemma enorm_indicator_eq_indicator_enorm :
diff --git a/Mathlib/Analysis/Normed/Group/InfiniteSum.lean b/Mathlib/Analysis/Normed/Group/InfiniteSum.lean
index 8c94cc49287a62..1854281f8418d9 100644
--- a/Mathlib/Analysis/Normed/Group/InfiniteSum.lean
+++ b/Mathlib/Analysis/Normed/Group/InfiniteSum.lean
@@ -41,7 +41,7 @@ open Topology ENNReal NNReal
 open Finset Filter Metric
 
 variable {ι α E F ε : Type*} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F]
-  [TopologicalSpace ε] [ESeminormedAddCommMonoid ε]
+  [TopologicalSpace ε] [AddCommMonoid ε] [ESeminormedAddMonoid ε]
 
 theorem cauchySeq_finset_iff_vanishing_norm {f : ι → E} :
     (CauchySeq fun s : Finset ι => ∑ i ∈ s, f i) ↔
diff --git a/Mathlib/Analysis/Normed/Group/Real.lean b/Mathlib/Analysis/Normed/Group/Real.lean
index 20ae16f5c06a86..98fa35148fdee2 100644
--- a/Mathlib/Analysis/Normed/Group/Real.lean
+++ b/Mathlib/Analysis/Normed/Group/Real.lean
@@ -39,7 +39,7 @@ instance : ENorm ℝ≥0∞ where
 
 @[simp] lemma enorm_eq_self (x : ℝ≥0∞) : ‖x‖ₑ = x := rfl
 
-noncomputable instance : ENormedAddCommMonoid ℝ≥0∞ where
+noncomputable instance : ENormedAddMonoid ℝ≥0∞ where
   continuous_enorm := continuous_id
   enorm_zero := by simp
   enorm_eq_zero := by simp
@@ -120,7 +120,7 @@ end Real
 section SeminormedCommGroup
 
 variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a b : E} {r : ℝ}
-variable {ε : Type*} [TopologicalSpace ε] [ESeminormedCommMonoid ε]
+variable {ε : Type*} [TopologicalSpace ε] [CommMonoid ε] [ESeminormedMonoid ε]
 
 @[to_additive (attr := simp high) norm_norm] -- Higher priority as a shortcut lemma.
 lemma norm_norm' (x : E) : ‖‖x‖‖ = ‖x‖ := Real.norm_of_nonneg (norm_nonneg' _)
diff --git a/Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean b/Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
index 533bb84a681d8c..e2fb128fe6abe6 100644
--- a/Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
+++ b/Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
@@ -35,7 +35,7 @@ open EMetric ENNReal Filter MeasureTheory NNReal Set
 
 variable {α β ε ε' : Type*} {m : MeasurableSpace α} {μ ν : Measure α}
 variable [NormedAddCommGroup β] [TopologicalSpace ε] [ContinuousENorm ε]
-  [TopologicalSpace ε'] [ESeminormedAddMonoid ε']
+  [TopologicalSpace ε'] [AddMonoid ε'] [ESeminormedAddMonoid ε']
 
 namespace MeasureTheory
 
diff --git a/Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean b/Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
index ec8059a833779b..e0054bc05f2cb3 100644
--- a/Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
+++ b/Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
@@ -38,7 +38,7 @@ open Set Filter TopologicalSpace ENNReal EMetric MeasureTheory
 
 variable {α β γ ε ε' ε'' : Type*} {m : MeasurableSpace α} {μ ν : Measure α}
 variable [NormedAddCommGroup β] [NormedAddCommGroup γ] [ENorm ε] [ENorm ε']
-  [TopologicalSpace ε''] [ESeminormedAddMonoid ε'']
+  [TopologicalSpace ε''] [AddMonoid ε''] [ESeminormedAddMonoid ε'']
 
 namespace MeasureTheory
 
@@ -246,7 +246,8 @@ theorem hasFiniteIntegral_zero_measure {m : MeasurableSpace α} (f : α → ε)
 
 variable (α μ) in
 @[fun_prop, simp]
-theorem hasFiniteIntegral_zero {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε] :
+theorem hasFiniteIntegral_zero {ε : Type*}
+    [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε] :
     HasFiniteIntegral (fun _ : α => (0 : ε)) μ := by
   simp [hasFiniteIntegral_iff_enorm]
 
@@ -284,7 +285,8 @@ theorem HasFiniteIntegral.of_isEmpty [IsEmpty α] {f : α → β} :
 
 @[simp]
 theorem HasFiniteIntegral.of_subsingleton_codomain
-    {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [Subsingleton ε] {f : α → ε} :
+    {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
+    [Subsingleton ε] {f : α → ε} :
     HasFiniteIntegral f μ :=
   hasFiniteIntegral_zero _ _ |>.congr <| .of_forall fun _ ↦ Subsingleton.elim _ _
 
@@ -313,7 +315,7 @@ theorem isFiniteMeasure_withDensity_ofReal {f : α → ℝ} (hfi : HasFiniteInte
 section DominatedConvergence
 
 variable {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
-  {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε]
+  {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
   {F' : ℕ → α → ε} {f' : α → ε} {bound' : α → ℝ≥0∞}
 
 theorem all_ae_norm_ofReal_F_le_bound (h : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a) :
diff --git a/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean b/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
index e0e53faa54c768..1cf57dad98b6be 100644
--- a/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
+++ b/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
@@ -247,7 +247,8 @@ lemma integrable_norm_pow_of_le [IsFiniteMeasure μ] {f : α → β} (hf : AEStr
 theorem Integrable.mono_measure {f : α → ε} (h : Integrable f ν) (hμ : μ ≤ ν) : Integrable f μ :=
   ⟨h.aestronglyMeasurable.mono_measure hμ, h.hasFiniteIntegral.mono_measure hμ⟩
 
-theorem Integrable.of_measure_le_smul {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε]
+theorem Integrable.of_measure_le_smul {ε}
+    [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
     {μ' : Measure α} {c : ℝ≥0∞} (hc : c ≠ ∞) (hμ'_le : μ' ≤ c • μ)
     {f : α → ε} (hf : Integrable f μ) : Integrable f μ' := by
   rw [← memLp_one_iff_integrable] at hf ⊢
@@ -305,7 +306,7 @@ theorem integrable_finset_sum_measure [PseudoMetrizableSpace ε]
 
 section
 
-variable {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε]
+variable {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
 
 @[fun_prop]
 theorem Integrable.smul_measure {f : α → ε} (h : Integrable f μ) {c : ℝ≥0∞} (hc : c ≠ ∞) :
@@ -399,7 +400,7 @@ theorem lintegral_edist_lt_top {f g : α → β} (hf : Integrable f μ) (hg : In
 
 section ESeminormedAddMonoid
 
-variable {ε' : Type*} [TopologicalSpace ε'] [ESeminormedAddMonoid ε']
+variable {ε' : Type*} [TopologicalSpace ε'] [AddMonoid ε'] [ESeminormedAddMonoid ε']
 
 variable (α ε') in
 @[simp]
@@ -430,7 +431,8 @@ end ESeminormedAddMonoid
 
 section ESeminormedAddCommMonoid
 
-variable {ε' : Type*} [TopologicalSpace ε'] [ESeminormedAddCommMonoid ε'] [ContinuousAdd ε']
+variable {ε' : Type*} [TopologicalSpace ε'] [AddCommMonoid ε'] [ESeminormedAddMonoid ε']
+  [ContinuousAdd ε']
 
 @[fun_prop]
 theorem integrable_finset_sum' {ι} (s : Finset ι) {f : ι → α → ε'}
@@ -950,7 +952,7 @@ end PosPart
 section IsBoundedSMul
 
 variable {𝕜 : Type*}
-  {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε]
+  {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
 
 @[to_fun (attr := fun_prop)]
 theorem Integrable.smul [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] [IsBoundedSMul 𝕜 β] (c : 𝕜)
diff --git a/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean b/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
index 372bd7007439e4..292d39910ee570 100644
--- a/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
+++ b/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
@@ -33,7 +33,7 @@ open scoped Topology Interval ENNReal
 variable {X Y ε ε' ε'' E F R : Type*} [MeasurableSpace X] [TopologicalSpace X]
 variable [MeasurableSpace Y] [TopologicalSpace Y]
 variable [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace ε'] [ContinuousENorm ε']
-  [TopologicalSpace ε''] [ESeminormedAddMonoid ε'']
+  [TopologicalSpace ε''] [AddMonoid ε''] [ESeminormedAddMonoid ε'']
   [NormedAddCommGroup E] [NormedAddCommGroup F] {f g : X → ε} {μ ν : Measure X} {s : Set X}
 
 namespace MeasureTheory
@@ -397,14 +397,14 @@ protected theorem LocallyIntegrable.smul {f : X → E} {𝕜 : Type*} [NormedAdd
     [SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E] (hf : LocallyIntegrable f μ) (c : 𝕜) :
     LocallyIntegrable (c • f) μ := fun x ↦ (hf x).smul c
 
-variable {ε''' : Type*} [TopologicalSpace ε'''] [ESeminormedAddCommMonoid ε''']
+variable {ε''' : Type*} [TopologicalSpace ε'''] [AddCommMonoid ε'''] [ESeminormedAddMonoid ε''']
   [ContinuousAdd ε'''] in
 theorem locallyIntegrable_finset_sum' {ι} (s : Finset ι) {f : ι → X → ε'''}
     (hf : ∀ i ∈ s, LocallyIntegrable (f i) μ) : LocallyIntegrable (∑ i ∈ s, f i) μ :=
   Finset.sum_induction f (fun g => LocallyIntegrable g μ) (fun _ _ => LocallyIntegrable.add)
     locallyIntegrable_zero hf
 
-variable {ε''' : Type*} [TopologicalSpace ε'''] [ESeminormedAddCommMonoid ε''']
+variable {ε''' : Type*} [TopologicalSpace ε'''] [AddCommMonoid ε'''] [ESeminormedAddMonoid ε''']
   [ContinuousAdd ε'''] in
 theorem locallyIntegrable_finset_sum {ι} (s : Finset ι) {f : ι → X → ε'''}
     (hf : ∀ i ∈ s, LocallyIntegrable (f i) μ) : LocallyIntegrable (fun a ↦ ∑ i ∈ s, f i a) μ := by
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
index e0a122dd1bc6d0..56313d41873d27 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -77,7 +77,7 @@ theorem memLp_zero_iff_aestronglyMeasurable [TopologicalSpace ε] {f : α → ε
 
 section ESeminormedAddMonoid
 
-variable {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε]
+variable {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
 
 @[simp]
 theorem eLpNorm'_zero (hp0_lt : 0 < q) : eLpNorm' (0 : α → ε) q μ = 0 := by
@@ -175,7 +175,7 @@ end Neg
 section Const
 
 variable {ε' ε'' : Type*} [TopologicalSpace ε'] [ContinuousENorm ε']
-  [TopologicalSpace ε''] [ESeminormedAddMonoid ε'']
+  [TopologicalSpace ε''] [AddMonoid ε''] [ESeminormedAddMonoid ε'']
 
 theorem eLpNorm'_const (c : ε) (hq_pos : 0 < q) :
     eLpNorm' (fun _ : α => c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q) := by
@@ -388,7 +388,7 @@ theorem eLpNormEssSup_lt_top_of_ae_bound {f : α → F} {C : ℝ} (hfC : ∀ᵐ
     eLpNormEssSup f μ < ∞ :=
   (eLpNormEssSup_le_of_ae_bound hfC).trans_lt ENNReal.ofReal_lt_top
 
-theorem eLpNorm_le_of_ae_enorm_bound {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε]
+theorem eLpNorm_le_of_ae_enorm_bound {ε} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
     {f : α → ε} {C : ℝ≥0∞} (hfC : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ C) :
     eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹ := by
   rcases eq_zero_or_neZero μ with rfl | hμ
@@ -602,7 +602,7 @@ end ContinuousENorm
 
 section ENormedAddMonoid
 
-variable {ε : Type*} [TopologicalSpace ε] [ENormedAddMonoid ε]
+variable {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ENormedAddMonoid ε]
 
 /-- For a function `f` with support in `s`, the Lᵖ norms of `f` with respect to `μ` and
 `μ.restrict s` are the same. -/
@@ -759,7 +759,7 @@ end ContinuousENorm
 
 section ESeminormedAddMonoid
 
-variable {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε]
+variable {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
 
 theorem eLpNorm'_eq_zero_of_ae_zero {f : α → ε} (hq0_lt : 0 < q) (hf_zero : f =ᵐ[μ] 0) :
     eLpNorm' f q μ = 0 := by rw [eLpNorm'_congr_ae hf_zero, eLpNorm'_zero hq0_lt]
@@ -816,7 +816,7 @@ end ESeminormedAddMonoid
 
 section ENormedAddMonoid
 
-variable {ε : Type*} [TopologicalSpace ε] [ENormedAddMonoid ε]
+variable {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ENormedAddMonoid ε]
 
 theorem ae_eq_zero_of_eLpNorm'_eq_zero {f : α → ε} (hq0 : 0 ≤ q) (hf : AEStronglyMeasurable f μ)
     (h : eLpNorm' f q μ = 0) : f =ᵐ[μ] 0 := by
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
index 859b622e81eb85..3b1972f3b8bb3d 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
@@ -28,7 +28,7 @@ section SameSpace
 
 variable {α ε ε' : Type*} {m : MeasurableSpace α} {μ : Measure α} {f : α → ε}
   [TopologicalSpace ε] [ContinuousENorm ε]
-  [TopologicalSpace ε'] [ESeminormedAddMonoid ε']
+  [TopologicalSpace ε'] [AddMonoid ε'] [ESeminormedAddMonoid ε']
 
 theorem eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ {p q : ℝ} (hp0_lt : 0 < p) (hpq : p ≤ q)
     (hf : AEStronglyMeasurable f μ) :
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Indicator.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Indicator.lean
index 3cb5767adf98f4..02f59142051f68 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/Indicator.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Indicator.lean
@@ -31,7 +31,7 @@ variable {f : α → F}
 
 section Indicator
 
-variable {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε]
+variable {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
   {c : ε} {hf : AEStronglyMeasurable f μ} {s : Set α}
   {ε' : Type*} [TopologicalSpace ε'] [ContinuousENorm ε']
 
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Monotonicity.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Monotonicity.lean
index 6c7f60ab2961c6..a73f60d91a6eca 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/Monotonicity.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Monotonicity.lean
@@ -58,7 +58,7 @@ theorem eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul' {f : α → ε} {g : α 
 
 section ESeminormedAddMonoid
 
-variable {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε]
+variable {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
 
 /-- If `‖f x‖ₑ ≤ c * ‖g x‖ₑ` a.e., `eLpNorm' f p μ ≤ c * eLpNorm' g p μ` for all `p ∈ (0, ∞)`. -/
 theorem eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul {f : α → ε} {c : ℝ≥0∞} {g : α → ε'} {p : ℝ}
@@ -160,7 +160,7 @@ theorem eLpNorm_le_mul_eLpNorm_of_ae_le_mul' {f : α → ε} {g : α → ε'} {c
     eLpNorm f p μ ≤ c * eLpNorm g p μ := by
   apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul' h
 
-variable {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε] in
+variable {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε] in
 /-- If `‖f x‖ₑ ≤ c * ‖g x‖ₑ`, then `eLpNorm f p μ ≤ c * eLpNorm g p μ`.
 
 This version allows `c = ∞`, but requires `g` to be a.e. strongly measurable. -/
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/SMul.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/SMul.lean
index adecdeac2a13d2..f6687ee347950f 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/SMul.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/SMul.lean
@@ -59,8 +59,8 @@ end IsBoundedSMul
 section ENormSMulClass
 
 variable {𝕜 : Type*} [NormedRing 𝕜]
-  {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [SMul 𝕜 ε] [ENormSMulClass 𝕜 ε]
-  {c : 𝕜} {f : α → ε}
+  {ε : Type*} [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
+  [SMul 𝕜 ε] [ENormSMulClass 𝕜 ε] {c : 𝕜} {f : α → ε}
 
 theorem eLpNorm'_const_smul_le' (hq : 0 < q) : eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * eLpNorm' f q μ :=
   eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul'
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
index a6eb6500d9d6a2..070099f39d136a 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
@@ -23,7 +23,8 @@ open scoped ENNReal Topology
 namespace MeasureTheory
 
 variable {α E ε ε' : Type*} {m : MeasurableSpace α} [NormedAddCommGroup E]
-  [TopologicalSpace ε] [ESeminormedAddMonoid ε] [TopologicalSpace ε'] [ESeminormedAddCommMonoid ε']
+  [TopologicalSpace ε] [AddMonoid ε] [ESeminormedAddMonoid ε]
+  [TopologicalSpace ε'] [AddCommMonoid ε'] [ESeminormedAddMonoid ε']
   {p : ℝ≥0∞} {q : ℝ} {μ : Measure α} {f g : α → ε}
 
 theorem eLpNorm'_add_le (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ)
diff --git a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
index be11e7d4eac624..6ead1ac3353f04 100644
--- a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
+++ b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
@@ -95,7 +95,7 @@ def IntegrableOn (f : α → ε) (s : Set α) (μ : Measure α := by volume_tac)
 theorem IntegrableOn.integrable (h : IntegrableOn f s μ) : Integrable f (μ.restrict s) :=
   h
 
-variable [TopologicalSpace ε'] [ESeminormedAddMonoid ε']
+variable [TopologicalSpace ε'] [AddMonoid ε'] [ESeminormedAddMonoid ε']
 
 @[simp]
 theorem integrableOn_empty : IntegrableOn f ∅ μ := by
@@ -396,7 +396,8 @@ theorem IntegrableOn.restrict_toMeasurable {f : α → ε'}
 -- TODO: investigate generalising this section to e-seminormed monoids
 section ENormedAddMonoid
 
-variable {ε' : Type*} [TopologicalSpace ε'] [ENormedAddMonoid ε'] [PseudoMetrizableSpace ε']
+variable {ε' : Type*} [TopologicalSpace ε'] [AddMonoid ε'] [ENormedAddMonoid ε']
+  [PseudoMetrizableSpace ε']
 
 -- TODO: generalise this to e-seminormed commutative monoids,
 -- by merely assuming ‖f x‖ₑ vanishes on t \ s
@@ -595,7 +596,7 @@ theorem IntegrableAtFilter.inf_ae_iff {l : Filter α} :
 
 alias ⟨IntegrableAtFilter.of_inf_ae, _⟩ := IntegrableAtFilter.inf_ae_iff
 
-variable {ε' : Type*} [TopologicalSpace ε'] [ENormedAddMonoid ε'] in
+variable {ε' : Type*} [TopologicalSpace ε'] [AddMonoid ε'] [ENormedAddMonoid ε'] in
 @[simp]
 theorem integrableAtFilter_top [PseudoMetrizableSpace ε'] {f : α → ε'} :
     IntegrableAtFilter f ⊤ μ ↔ Integrable f μ := by
@@ -820,7 +821,7 @@ the unprimed ones use `[NoAtoms μ]`.
 section PartialOrder
 
 variable [PartialOrder α] [MeasurableSingletonClass α]
-  [TopologicalSpace ε'] [ESeminormedAddMonoid ε'] [PseudoMetrizableSpace ε']
+  [TopologicalSpace ε'] [AddMonoid ε'] [ESeminormedAddMonoid ε'] [PseudoMetrizableSpace ε']
   {f : α → ε'} {μ : Measure α} {a b : α}
 
 theorem integrableOn_Icc_iff_integrableOn_Ioc'
diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
index eff889145cf166..e80c34028c87dd 100644
--- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
+++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
@@ -58,7 +58,8 @@ open MeasureTheory Set Filter Function TopologicalSpace
 open scoped Topology Filter ENNReal Interval NNReal
 
 variable {ι 𝕜 ε ε' E F A : Type*} [NormedAddCommGroup E]
-  [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace ε'] [ENormedAddMonoid ε']
+  [TopologicalSpace ε] [AddMonoid ε] [ENormedAddMonoid ε]
+  [TopologicalSpace ε'] [AddMonoid ε'] [ENormedAddMonoid ε']
 
 /-!
 ### Integrability on an interval
@@ -319,15 +320,15 @@ theorem sub {f g : ℝ → E} (hf : IntervalIntegrable f μ a b) (hg : IntervalI
     IntervalIntegrable (fun x => f x - g x) μ a b :=
   ⟨hf.1.sub hg.1, hf.2.sub hg.2⟩
 
-theorem sum {ε} [TopologicalSpace ε] [ENormedAddCommMonoid ε] [ContinuousAdd ε]
+theorem sum {ε} [TopologicalSpace ε] [AddCommMonoid ε] [ENormedAddMonoid ε] [ContinuousAdd ε]
     (s : Finset ι) {f : ι → ℝ → ε} (h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b) :
     IntervalIntegrable (∑ i ∈ s, f i) μ a b :=
   ⟨integrable_finset_sum' s fun i hi => (h i hi).1, integrable_finset_sum' s fun i hi => (h i hi).2⟩
 
 /-- Finite sums of interval integrable functions are interval integrable. -/
 @[simp]
-protected theorem finsum
-    {ε} [TopologicalSpace ε] [ENormedAddCommMonoid ε] [ContinuousAdd ε] [PseudoMetrizableSpace ε]
+protected theorem finsum {ε} [TopologicalSpace ε] [AddCommMonoid ε] [ENormedAddMonoid ε]
+    [ContinuousAdd ε] [PseudoMetrizableSpace ε]
     {f : ι → ℝ → ε} (h : ∀ i, IntervalIntegrable (f i) μ a b) :
     IntervalIntegrable (∑ᶠ i, f i) μ a b := by
   by_cases h₁ : f.support.Finite
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index cd7b3931a80469..68e6b3efff3f4f 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -36,7 +36,7 @@ open scoped ENNReal
 namespace MeasureTheory.VectorMeasure
 
 variable {X V : Type*} {mX : MeasurableSpace X}
-  [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V]
+  [TopologicalSpace V] [AddCommMonoid V] [ENormedAddMonoid V] [T2Space V]
 
 @[simp]
 lemma variation_apply (μ : VectorMeasure X V) (s : Set X) :
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Defs.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Defs.lean
index 829311da677ffc..30010cc35a0883 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Defs.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Defs.lean
@@ -38,7 +38,7 @@ open MeasureTheory BigOperators NNReal ENNReal Function
 
 namespace MeasureTheory.VectorMeasure
 
-variable {V : Type*} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V]
+variable {V : Type*} [TopologicalSpace V] [AddCommMonoid V] [ENormedAddMonoid V] [T2Space V]
 
 /-- The norm of a vector measure is σ-subadditive on measurable sets. -/
 lemma isSigmaSubadditiveSetFun_enorm (μ : VectorMeasure X V) :