feat(Algebra/Group/Submonoid/Defs): add OneMemClass.coe_nonempty (leanprover-community#38288)

The main value of this is to make `simp` stronger

Author: b-mehta

Mathlib/Algebra/Group/Subgroup/Defs.lean

@@ -396,9 +396,12 @@ 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]
 lemma coe_nonempty (s : Subgroup G) : (s : Set G).Nonempty := ⟨1, one_mem _⟩
 
+attribute [deprecated OneMemClass.coe_nonempty (since := "2026-04-20")] Subgroup.coe_nonempty
+attribute [deprecated ZeroMemClass.coe_nonempty (since := "2026-04-20")] AddSubgroup.coe_nonempty
+
 end Subgroup
 
 namespace Subgroup

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. -/

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

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]

Mathlib/NumberTheory/LocalField/Basic.lean

@@ -177,7 +177,7 @@ instance : IsAdicComplete 𝓂[K] 𝒪[K] where
       simpa [S] using (hf n.le_succ).symm
     have h n : IsClosed (S n) := (IsNoetherianRing.isClosed_ideal (𝓂[K] ^ n)).vadd (f n)
     obtain ⟨L, hL⟩ := (h 0).isCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed S hS
-      (by simp [S, Submodule.nonempty]) h
+      (by simp [S]) h
     refine ⟨L, fun n ↦ ?_⟩
     obtain ⟨y, hy, rfl⟩ := Set.mem_iInter.mp hL n
     simpa [SModEq.sub_mem] using hy