chore(data/set/{function,countable}): extract a lemma from a proof (#…

…15668)

src/data/set/countable.lean

@@ -44,11 +44,7 @@ countable_coe_iff.symm.trans (countable_iff_exists_injective s)
 on `s`. -/
 lemma countable_iff_exists_inj_on {s : set α} :
   s.countable ↔ ∃ f : α → ℕ, inj_on f s :=
-set.countable_iff_exists_injective.trans
-⟨λ ⟨f, hf⟩, ⟨λ a, if h : a ∈ s then f ⟨a, h⟩ else 0,
-   λ a as b bs h, congr_arg subtype.val $
-     hf $ by simpa [as, bs] using h⟩,
- λ ⟨f, hf⟩, ⟨_, inj_on_iff_injective.1 hf⟩⟩
+set.countable_iff_exists_injective.trans exists_inj_on_iff_injective.symm
 
 /-- Convert `set.countable s` to `encodable s` (noncomputable). -/
 protected def countable.to_encodable {s : set α} : s.countable → encodable s :=
@@ -155,7 +151,7 @@ let ⟨g, hg⟩ := countable_iff_exists_inj_on.1 hs in
 countable_iff_exists_inj_on.2 ⟨g ∘ f, hg.comp hf (maps_to_image _ _)⟩
 
 lemma countable_Union {t : ι → set α} [countable ι] (ht : ∀ i, (t i).countable) :
-  (⋃a, t a).countable :=
+  (⋃ i, t i).countable :=
 by { haveI := λ a, (ht a).to_subtype, rw Union_eq_range_psigma, apply countable_range }
 
 @[simp] lemma countable_Union_iff [countable ι] {t : ι → set α} :

src/data/set/function.lean

@@ -431,6 +431,11 @@ lemma inj_on_iff_injective : inj_on f s ↔ injective (s.restrict f) :=
 
 alias inj_on_iff_injective ↔ inj_on.injective _
 
+lemma exists_inj_on_iff_injective [nonempty β] :
+  (∃ f : α → β, inj_on f s) ↔ ∃ f : s → β, injective f :=
+⟨λ ⟨f, hf⟩, ⟨_, hf.injective⟩,
+  λ ⟨f, hf⟩, by { lift f to α → β using trivial, exact ⟨f, inj_on_iff_injective.2 hf⟩ }⟩
+
 lemma inj_on_preimage {B : set (set β)} (hB : B ⊆ 𝒫 (range f)) :
   inj_on (preimage f) B :=
 λ s hs t ht hst, (preimage_eq_preimage' (hB hs) (hB ht)).1 hst