diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean
index 5b0af20456dff..f1437e7138084 100644
--- a/Mathlib/Data/Finset/Image.lean
+++ b/Mathlib/Data/Finset/Image.lean
@@ -767,4 +767,38 @@ theorem finsetCongr_toEmbedding (e : α ≃ β) :
     e.finsetCongr.toEmbedding = (Finset.mapEmbedding e.toEmbedding).toEmbedding :=
   rfl
 
+/-- Given a predicate `p : α → Prop`, produces an equivalence between
+  `Finset {a : α // p a}` and `{s : Finset α // ∀ a ∈ s, p a}`.
+
+  Theorems generated by simps:
+  @[simp]
+  protected lemma finsetSubtypeCongr_apply_coe (p : α → Prop) (s : Finset {a // p a}) :
+    (Equiv.finsetSubtypeCongr p) s = s.map ⟨Subtype.val, Subtype.val_injective⟩
+
+  @[simp]
+  protected lemma finsetSubtypeCongr_symm_apply (p : α → Prop) (s : { s // ∀ a ∈ s, p a }) :
+    (Equiv.finsetSubtypeCongr p).symm s =
+      s.val.attach.map (Subtype.impEmbedding (Membership.mem s.val) p fun _ ↦ s.property _)
+  -/
+
+@[simps]
+protected def finsetSubtypeCongr (p : α → Prop) :
+    Finset {a : α // p a} ≃ {s : Finset α // ∀ a ∈ s, p a} where
+  toFun s := ⟨s.map ⟨fun a ↦ a.val, Subtype.val_injective⟩, fun _ h ↦
+    have ⟨v, _, h⟩ := Embedding.coeFn_mk _ _ ▸ mem_map.mp h; h ▸ v.property⟩
+  invFun s := s.val.attach.map (Subtype.impEmbedding _ _ s.property)
+  left_inv s := by
+    ext a; constructor <;> intro h <;>
+    simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
+      exists_and_right, exists_eq_right, Subtype.impEmbedding, Subtype.mk.injEq] at *
+    · rcases h with ⟨_, ⟨_, h₁⟩, h₂⟩; exact h₂ ▸ h₁
+    · use a, ⟨a.property, h⟩
+  right_inv s := by
+    ext a; constructor <;> intro h <;>
+    simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
+      exists_and_right, exists_eq_right, Subtype.impEmbedding, Subtype.mk.injEq] at *
+    · rcases h with ⟨_, _, h₁, h₂⟩; exact h₂ ▸ h₁
+    · use s.property _ h, a
+
 end Equiv
+
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
index 8d28bac27f0b0..a7158d7cf6b77 100644
--- a/Mathlib/Data/Set/Basic.lean
+++ b/Mathlib/Data/Set/Basic.lean
@@ -2168,4 +2168,30 @@ end Disjoint
 @[simp] theorem Prop.compl_singleton (p : Prop) : ({p}ᶜ : Set Prop) = {¬p} :=
   ext fun q ↦ by simpa [@Iff.comm q] using not_iff
 
+namespace Equiv
+
+/-- Given a predicate `p : α → Prop`, produces an equivalence between
+  `Set {a : α // p a}` and `{s : Set α // ∀ a ∈ s, p a}`.
+
+  Theorems generated by simps:
+
+  @[simp]
+  protected lemma setSubtypeCongr_apply_coe (p : α → Prop) (s : Set {a // p a}) (a : α) :
+    (Equiv.setSubtypeCongr p) s a = ∃ (h : p a), s ⟨a, h⟩
+
+  @[simp]
+  protected lemma setSubtypeCongr_symm_apply
+      (p : α → Prop) (s : {s // ∀ a ∈ s, p a}) (a : {a // p a}) :
+    (Equiv.setSubtypeCongr p).symm s a = s.val a.val
+  -/
+@[simps]
+protected def setSubtypeCongr {α : Type*} (p : α → Prop) :
+    Set {a : α // p a} ≃ {s : Set α // ∀ a ∈ s, p a} where
+  toFun s := ⟨fun a ↦ ∃ h : p a, s ⟨a, h⟩, fun _ h ↦ h.1⟩
+  invFun s a := s.val a
+  left_inv s := by ext a; exact ⟨fun h ↦ h.2, fun h ↦ ⟨a.property, h⟩⟩
+  right_inv s := by ext; exact ⟨fun h ↦ h.2, fun h ↦ ⟨s.property _ h, h⟩⟩
+
+end Equiv
+
 set_option linter.style.longFile 2300