diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean
index 02490720fc402..5a8fb03b442aa 100644
--- a/Mathlib/GroupTheory/Subgroup/Basic.lean
+++ b/Mathlib/GroupTheory/Subgroup/Basic.lean
@@ -2660,7 +2660,8 @@ theorem range_top_iff_surjective {N} [Group N] {f : G →* N} :
 #align add_monoid_hom.range_top_iff_surjective AddMonoidHom.range_top_iff_surjective
 
 /-- The range of a surjective monoid homomorphism is the whole of the codomain. -/
-@[to_additive "The range of a surjective `AddMonoid` homomorphism is the whole of the codomain."]
+@[to_additive (attr := simp)
+  "The range of a surjective `AddMonoid` homomorphism is the whole of the codomain."]
 theorem range_top_of_surjective {N} [Group N] (f : G →* N) (hf : Function.Surjective f) :
     f.range = (⊤ : Subgroup N) :=
   range_top_iff_surjective.2 hf
diff --git a/Mathlib/GroupTheory/Submonoid/Operations.lean b/Mathlib/GroupTheory/Submonoid/Operations.lean
index be0f330594217..38749c47ea379 100644
--- a/Mathlib/GroupTheory/Submonoid/Operations.lean
+++ b/Mathlib/GroupTheory/Submonoid/Operations.lean
@@ -1072,7 +1072,8 @@ theorem mrange_top_iff_surjective {f : F} : mrange f = (⊤ : Submonoid N) ↔ F
 #align add_monoid_hom.mrange_top_iff_surjective AddMonoidHom.mrange_top_iff_surjective
 
 /-- The range of a surjective monoid hom is the whole of the codomain. -/
-@[to_additive "The range of a surjective `AddMonoid` hom is the whole of the codomain."]
+@[to_additive (attr := simp)
+  "The range of a surjective `AddMonoid` hom is the whole of the codomain."]
 theorem mrange_top_of_surjective (f : F) (hf : Function.Surjective f) :
     mrange f = (⊤ : Submonoid N) :=
   mrange_top_iff_surjective.2 hf
diff --git a/Mathlib/GroupTheory/Subsemigroup/Operations.lean b/Mathlib/GroupTheory/Subsemigroup/Operations.lean
index af7b59d322fb8..a98aeaf779bfe 100644
--- a/Mathlib/GroupTheory/Subsemigroup/Operations.lean
+++ b/Mathlib/GroupTheory/Subsemigroup/Operations.lean
@@ -787,7 +787,8 @@ theorem srange_top_iff_surjective {N} [Mul N] {f : M →ₙ* N} :
 #align add_hom.srange_top_iff_surjective AddHom.srange_top_iff_surjective
 
 /-- The range of a surjective semigroup hom is the whole of the codomain. -/
-@[to_additive "The range of a surjective `add_semigroup` hom is the whole of the codomain."]
+@[to_additive (attr := simp)
+  "The range of a surjective `add_semigroup` hom is the whole of the codomain."]
 theorem srange_top_of_surjective {N} [Mul N] (f : M →ₙ* N) (hf : Function.Surjective f) :
     f.srange = (⊤ : Subsemigroup N) :=
   srange_top_iff_surjective.2 hf
diff --git a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
index c63a12f44bf14..ef356f635c77f 100644
--- a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
+++ b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
@@ -642,6 +642,7 @@ theorem map_top (f : α → β) : map f ⊤ = restrict (range f) ⊤ :=
       Set.image_eq_empty]
 #align measure_theory.outer_measure.map_top MeasureTheory.OuterMeasure.map_top
 
+@[simp]
 theorem map_top_of_surjective (f : α → β) (hf : Surjective f) : map f ⊤ = ⊤ := by
   rw [map_top, hf.range_eq, restrict_univ]
 #align measure_theory.outer_measure.map_top_of_surjective MeasureTheory.OuterMeasure.map_top_of_surjective
diff --git a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean b/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
index 277c5391ecfdf..44ce2a4279573 100644
--- a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
+++ b/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
@@ -891,6 +891,7 @@ theorem srange_top_iff_surjective {f : F} :
 #align non_unital_ring_hom.srange_top_iff_surjective NonUnitalRingHom.srange_top_iff_surjective
 
 /-- The range of a surjective non-unital ring homomorphism is the whole of the codomain. -/
+@[simp]
 theorem srange_top_of_surjective (f : F) (hf : Function.Surjective (f : R → S)) :
     srange f = (⊤ : NonUnitalSubsemiring S) :=
   srange_top_iff_surjective.2 hf
diff --git a/Mathlib/RingTheory/Subring/Basic.lean b/Mathlib/RingTheory/Subring/Basic.lean
index b9fd4770857f6..4660fc95f0430 100644
--- a/Mathlib/RingTheory/Subring/Basic.lean
+++ b/Mathlib/RingTheory/Subring/Basic.lean
@@ -1215,6 +1215,7 @@ theorem range_top_iff_surjective {f : R →+* S} :
 #align ring_hom.range_top_iff_surjective RingHom.range_top_iff_surjective
 
 /-- The range of a surjective ring homomorphism is the whole of the codomain. -/
+@[simp]
 theorem range_top_of_surjective (f : R →+* S) (hf : Function.Surjective f) :
     f.range = (⊤ : Subring S) :=
   range_top_iff_surjective.2 hf
diff --git a/Mathlib/RingTheory/Subsemiring/Basic.lean b/Mathlib/RingTheory/Subsemiring/Basic.lean
index ca7a63c587d38..da1c176f9f8f4 100644
--- a/Mathlib/RingTheory/Subsemiring/Basic.lean
+++ b/Mathlib/RingTheory/Subsemiring/Basic.lean
@@ -1183,6 +1183,7 @@ theorem rangeS_top_iff_surjective {f : R →+* S} :
 #align ring_hom.srange_top_iff_surjective RingHom.rangeS_top_iff_surjective
 
 /-- The range of a surjective ring homomorphism is the whole of the codomain. -/
+@[simp]
 theorem rangeS_top_of_surjective (f : R →+* S) (hf : Function.Surjective f) :
     f.rangeS = (⊤ : Subsemiring S) :=
   rangeS_top_iff_surjective.2 hf