feat(Subtype): SurjOn versions of coind_surjective and coind_bijective (#31349)

Conditions of theorems `Subtype.coind_surjective` and `Subtype.coind_bijective` imply that the subtype coincides with the whole type, which makes these theorems not very useful. This PR deprecates them and proves `Set.SurjOn` versions.

Author: vasnesterov

Mathlib/Data/Set/Function.lean

@@ -576,6 +576,17 @@ theorem SurjOn.forall {p : β → Prop} (hf : s.SurjOn f t) (hf' : s.MapsTo f t)
     (∀ y ∈ t, p y) ↔ (∀ x ∈ s, p (f x)) :=
   ⟨fun H x hx ↦ H (f x) (hf' hx), fun H _y hy ↦ let ⟨x, hx, hxy⟩ := hf hy; hxy ▸ H x hx⟩
 
+theorem _root_.Subtype.coind_surjective {α β} {f : α → β} {p : Set β} (h : ∀ a, f a ∈ p)
+    (hf : Set.SurjOn f Set.univ p) :
+    (Subtype.coind f h).Surjective := fun ⟨_, hb⟩ ↦
+  let ⟨a, _, ha⟩ := hf hb
+  ⟨a, Subtype.coe_injective ha⟩
+
+theorem _root_.Subtype.coind_bijective {α β} {f : α → β} {p : Set β} (h : ∀ a, f a ∈ p)
+    (hf_inj : f.Injective) (hf_surj : Set.SurjOn f Set.univ p) :
+    (Subtype.coind f h).Bijective :=
+  ⟨Subtype.coind_injective h hf_inj, Subtype.coind_surjective h hf_surj⟩
+
 end surjOn
 
 /-! ### Bijectivity -/

Mathlib/Data/Subtype.lean

@@ -142,15 +142,6 @@ def coind {α β} (f : α → β) {p : β → Prop} (h : ∀ a, p (f a)) : α 
 theorem coind_injective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Injective f) :
     Injective (coind f h) := fun x y hxy ↦ hf <| by apply congr_arg Subtype.val hxy
 
-theorem coind_surjective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Surjective f) :
-    Surjective (coind f h) := fun x ↦
-  let ⟨a, ha⟩ := hf x
-  ⟨a, coe_injective ha⟩
-
-theorem coind_bijective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Bijective f) :
-    Bijective (coind f h) :=
-  ⟨coind_injective h hf.1, coind_surjective h hf.2⟩
-
 /-- Restriction of a function to a function on subtypes. -/
 @[simps]
 def map {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ a, p a → q (f a)) :