chore(data/equiv/basic): redefine set.bij_on.equiv (#5128)

Now `set.bij_on.equiv` works for any `h : set.bij_on f s t`. The old
behaviour can be achieved using `(equiv.set_univ _).symm.trans _`.

src/data/equiv/basic.lean

@@ -1772,20 +1772,11 @@ protected def congr_right {r r' : setoid α}
 quot.congr_right eq
 end quotient
 
-/-- If a function is a bijection between `univ` and a set `s` in the target type, it induces an
-equivalence between the original type and the type `↑s`. -/
-noncomputable def set.bij_on.equiv {α : Type*} {β : Type*} {s : set β} (f : α → β)
-  (h : set.bij_on f set.univ s) : α ≃ s :=
-begin
-  have : function.bijective (λ (x : α), (⟨f x, begin exact h.maps_to (set.mem_univ x) end⟩ : s)),
-  { split,
-    { assume x y hxy,
-      apply h.inj_on (set.mem_univ x) (set.mem_univ y) (subtype.mk.inj hxy) },
-    { assume x,
-      rcases h.surj_on x.2 with ⟨y, hy⟩,
-      exact ⟨y, subtype.eq hy.2⟩ } },
-  exact equiv.of_bijective _ this
-end
+/-- If a function is a bijection between two sets `s` and `t`, then it induces an
+equivalence between the the types `↥s` and ``↥t`. -/
+noncomputable def set.bij_on.equiv {α : Type*} {β : Type*} {s : set α} {t : set β} (f : α → β)
+  (h : set.bij_on f s t) : s ≃ t :=
+equiv.of_bijective _ h.bijective
 
 /-- The composition of an updated function with an equiv on a subset can be expressed as an
 updated function. -/

src/data/finset/sort.lean

@@ -240,7 +240,7 @@ the cardinality of `s` is `k`. We use this instead of a map `fin s.card → α`
 casting issues in further uses of this function. -/
 noncomputable def mono_equiv_of_fin (s : finset α) {k : ℕ} (h : s.card = k) :
   fin k ≃ {x // x ∈ s} :=
-(s.mono_of_fin_bij_on h).equiv _
+(equiv.set.univ _).symm.trans $ (s.mono_of_fin_bij_on h).equiv _
 
 end sort_linear_order
 

src/data/set/function.lean

@@ -371,6 +371,11 @@ theorem bij_on.comp (hg : bij_on g t p) (hf : bij_on f s t) : bij_on (g ∘ f) s
 bij_on.mk (hg.maps_to.comp hf.maps_to) (hg.inj_on.comp hf.inj_on hf.maps_to)
   (hg.surj_on.comp hf.surj_on)
 
+theorem bij_on.bijective (h : bij_on f s t) :
+  bijective (t.cod_restrict (s.restrict f) $ λ x, h.maps_to x.val_prop) :=
+⟨λ x y h', subtype.ext $ h.inj_on x.2 y.2 $ subtype.ext_iff.1 h',
+  λ ⟨y, hy⟩, let ⟨x, hx, hxy⟩ := h.surj_on hy in ⟨⟨x, hx⟩, subtype.eq hxy⟩⟩
+
 lemma bijective_iff_bij_on_univ : bijective f ↔ bij_on f univ univ :=
 iff.intro
 (λ h, let ⟨inj, surj⟩ := h in