diff --git a/Mathlib/Algebra/Group/Subgroup/Defs.lean b/Mathlib/Algebra/Group/Subgroup/Defs.lean
index b18ac2fbe16885..c593d7b0570bca 100644
--- a/Mathlib/Algebra/Group/Subgroup/Defs.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Defs.lean
@@ -396,7 +396,7 @@ theorem toSubmonoid_mono : Monotone (toSubmonoid : Subgroup G → Submonoid G) :
 theorem toSubmonoid_le {p q : Subgroup G} : p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q :=
   Iff.rfl
 
-@[to_additive (attr := simp)]
+@[to_additive (attr := deprecated OneMemClass.coe_nonempty (since := "2026-04-20"))]
 lemma coe_nonempty (s : Subgroup G) : (s : Set G).Nonempty := ⟨1, one_mem _⟩
 
 end Subgroup
diff --git a/Mathlib/Algebra/Group/Submonoid/Defs.lean b/Mathlib/Algebra/Group/Submonoid/Defs.lean
index 34387c4b9749c1..420acdf550b202 100644
--- a/Mathlib/Algebra/Group/Submonoid/Defs.lean
+++ b/Mathlib/Algebra/Group/Submonoid/Defs.lean
@@ -76,6 +76,13 @@ attribute [to_additive] OneMemClass
 
 attribute [simp, aesop safe (rule_sets := [SetLike])] one_mem zero_mem
 
+/-- The underlying set of a term of a `OneMemClass` is nonempty. -/
+@[to_additive (attr := simp)
+/-- The underlying set of a term of a `ZeroMemClass` is nonempty. -/]
+theorem OneMemClass.coe_nonempty {S M : Type*} [One M] [SetLike S M] [OneMemClass S M] (s : S) :
+    (s : Set M).Nonempty :=
+  ⟨1, one_mem s⟩
+
 section
 
 /-- A submonoid of a monoid `M` is a subset containing 1 and closed under multiplication. -/
diff --git a/Mathlib/Data/ZMod/QuotientGroup.lean b/Mathlib/Data/ZMod/QuotientGroup.lean
index c8465c0e480649..008f9fc2161340 100644
--- a/Mathlib/Data/ZMod/QuotientGroup.lean
+++ b/Mathlib/Data/ZMod/QuotientGroup.lean
@@ -167,7 +167,7 @@ variable {a}
 @[to_additive (attr := simp)]
 lemma finite_zpowers : (zpowers a : Set α).Finite ↔ IsOfFinOrder a := by
   simp only [← orderOf_pos_iff, ← Nat.card_zpowers, Nat.card_pos_iff, ← SetLike.coe_sort_coe,
-    nonempty_coe_sort, Nat.card_pos_iff, Set.finite_coe_iff, Subgroup.coe_nonempty, true_and]
+    nonempty_coe_sort, Nat.card_pos_iff, Set.finite_coe_iff, OneMemClass.coe_nonempty, true_and]
 
 @[to_additive (attr := simp)]
 lemma infinite_zpowers : (zpowers a : Set α).Infinite ↔ ¬IsOfFinOrder a := finite_zpowers.not
diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean
index 2e2969241e516c..d1934f48229ff5 100644
--- a/Mathlib/GroupTheory/OrderOfElement.lean
+++ b/Mathlib/GroupTheory/OrderOfElement.lean
@@ -1163,7 +1163,7 @@ nonrec lemma Subgroup.orderOf_dvd_natCard {G : Type*} [Group G] (s : Subgroup G)
 @[to_additive]
 lemma Subgroup.orderOf_le_card {G : Type*} [Group G] (s : Subgroup G) (hs : (s : Set G).Finite)
     {x} (hx : x ∈ s) : orderOf x ≤ Nat.card s :=
-  le_of_dvd (Nat.card_pos_iff.2 <| ⟨s.coe_nonempty.to_subtype, hs.to_subtype⟩) <|
+  le_of_dvd (Nat.card_pos_iff.2 <| ⟨(OneMemClass.coe_nonempty s).to_subtype, hs.to_subtype⟩) <|
     s.orderOf_dvd_natCard hx
 
 @[to_additive]