chore: add @[simp] uniformly to _top_of_surjective lemmas (#5064)

Some such lemmas are already labelled `@[simp]`, and this PR adds `@[simp]` to the remaining ones. It's useful for some automation I'm writing to have these all in `simp`. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
leanprover-community · Jun 19, 2023 · 51accc7 · 51accc7
1 parent 129e53b
commit 51accc7
Show file tree

Hide file tree

Showing 7 changed files with 10 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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