chore: rename Set.nonempty_of_nonempty_subtype to `Set.Nonempty.of_…

…subtype` (#19408) This is shorter and allows anonymous dot notation. From GrowthInGroups (LeanCamCombi)
leanprover-community · Nov 23, 2024 · 2abe270 · 2abe270
1 parent d6a85bb
commit 2abe270
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 6 deletions.
diff --git a/Mathlib/Data/ENat/Lattice.lean b/Mathlib/Data/ENat/Lattice.lean
@@ -106,7 +106,7 @@ lemma finite_of_sSup_lt_top (h : sSup s < ⊤) : s.Finite := by
   exact sSup_eq_top_of_infinite h
 
 lemma sSup_mem_of_nonempty_of_lt_top [Nonempty s] (hs' : sSup s < ⊤) : sSup s ∈ s :=
-  Nonempty.csSup_mem nonempty_of_nonempty_subtype (finite_of_sSup_lt_top hs')
+  Nonempty.csSup_mem .of_subtype (finite_of_sSup_lt_top hs')
 
 lemma exists_eq_iSup_of_lt_top [Nonempty ι] (h : ⨆ i, f i < ⊤) :
     ∃ i, f i = ⨆ i, f i :=

diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
@@ -436,8 +436,9 @@ instance univ.nonempty [Nonempty α] : Nonempty (↥(Set.univ : Set α)) :=
 instance instNonemptyTop [Nonempty α] : Nonempty (⊤ : Set α) :=
   inferInstanceAs (Nonempty (univ : Set α))
 
-theorem nonempty_of_nonempty_subtype [Nonempty (↥s)] : s.Nonempty :=
-  nonempty_subtype.mp ‹_›
+theorem Nonempty.of_subtype [Nonempty (↥s)] : s.Nonempty := nonempty_subtype.mp ‹_›
+
+@[deprecated (since := "2024-11-23")] alias nonempty_of_nonempty_subtype := Nonempty.of_subtype
 
 /-! ### Lemmas about the empty set -/
 
@@ -1204,7 +1205,7 @@ theorem eq_empty_of_ssubset_singleton {s : Set α} {x : α} (hs : s ⊂ {x}) : s
 
 theorem eq_of_nonempty_of_subsingleton {α} [Subsingleton α] (s t : Set α) [Nonempty s]
     [Nonempty t] : s = t :=
-  nonempty_of_nonempty_subtype.eq_univ.trans nonempty_of_nonempty_subtype.eq_univ.symm
+  Nonempty.of_subtype.eq_univ.trans Nonempty.of_subtype.eq_univ.symm
 
 theorem eq_of_nonempty_of_subsingleton' {α} [Subsingleton α] {s : Set α} (t : Set α)
     (hs : s.Nonempty) [Nonempty t] : s = t :=

diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean
@@ -408,7 +408,7 @@ theorem Nonempty.preimage {s : Set β} (hs : s.Nonempty) {f : α → β} (hf : S
   ⟨x, mem_preimage.2 <| hx.symm ▸ hy⟩
 
 instance (f : α → β) (s : Set α) [Nonempty s] : Nonempty (f '' s) :=
-  (Set.Nonempty.image f nonempty_of_nonempty_subtype).to_subtype
+  (Set.Nonempty.image f .of_subtype).to_subtype
 
 /-- image and preimage are a Galois connection -/
 @[simp]

diff --git a/Mathlib/GroupTheory/PGroup.lean b/Mathlib/GroupTheory/PGroup.lean
@@ -189,7 +189,7 @@ theorem card_modEq_card_fixedPoints : Nat.card α ≡ Nat.card (fixedPoints G α
 theorem nonempty_fixed_point_of_prime_not_dvd_card (α) [MulAction G α] (hpα : ¬p ∣ Nat.card α) :
     (fixedPoints G α).Nonempty :=
   have : Finite α := Nat.finite_of_card_ne_zero (fun h ↦ (h ▸ hpα) (dvd_zero p))
-  @Set.nonempty_of_nonempty_subtype _ _
+  @Set.Nonempty.of_subtype _ _
     (by
       rw [← Finite.card_pos_iff, pos_iff_ne_zero]
       contrapose! hpα