feat(data/equiv/basic): subtype_equiv_psigma (#9688)

- [x] depends on: #9687

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/data/equiv/basic.lean

@@ -953,6 +953,28 @@ by { ext1 x, cases x, refl }
   (sigma_congr_right (λ a, equiv.refl (β a))) = equiv.refl (Σ a, β a) :=
 by { ext1 x, cases x, refl }
 
+/-- A `psigma` with `Prop` fibers is equivalent to the subtype.  -/
+def psigma_equiv_subtype {α : Type v} (P : α → Prop) :
+  (Σ' i, P i) ≃ subtype P :=
+{ to_fun := λ x, ⟨x.1, x.2⟩,
+  inv_fun := λ x, ⟨x.1, x.2⟩,
+  left_inv := λ x, by { cases x, refl, },
+  right_inv := λ x, by { cases x, refl, }, }
+
+/-- A `sigma` with `plift` fibers is equivalent to the subtype. -/
+def sigma_plift_equiv_subtype {α : Type v} (P : α → Prop) :
+  (Σ i, plift (P i)) ≃ subtype P :=
+((psigma_equiv_sigma _).symm.trans (psigma_congr_right (λ a, equiv.plift))).trans
+  (psigma_equiv_subtype P)
+
+/--
+A `sigma` with `λ i, ulift (plift (P i))` fibers is equivalent to `{ x // P x }`.
+Variant of `sigma_plift_equiv_subtype`.
+-/
+def sigma_ulift_plift_equiv_subtype {α : Type v} (P : α → Prop) :
+  (Σ i, ulift (plift (P i))) ≃ subtype P :=
+(sigma_congr_right (λ a, equiv.ulift)).trans (sigma_plift_equiv_subtype P)
+
 namespace perm
 
 /-- A family of permutations `Π a, perm (β a)` generates a permuation `perm (Σ a, β₁ a)`. -/