feat(data/set/countable): protect lemmas (#15415)

We protect `set.countable_iff_exists_injective`, `set.countable_iff_exists_surjective`, and `set.countable.to_encodable` in order to avoid clashes with the theorems on the new `countable` typeclass.

Author: vihdzp

src/data/countable/basic.lean

@@ -10,7 +10,7 @@ import data.countable.defs
 /-!
 # Countable types
 
-In this file we provide basis instances of the `countable` typeclass defined elsewhere.
+In this file we provide basic instances of the `countable` typeclass defined elsewhere.
 -/
 
 universes u v w

src/data/set/countable.lean

@@ -27,7 +27,7 @@ constructive analogue of countability. (For the most part, theorems about
 -/
 protected def countable (s : set α) : Prop := nonempty (encodable s)
 
-lemma countable_iff_exists_injective {s : set α} :
+protected lemma countable_iff_exists_injective {s : set α} :
   s.countable ↔ ∃f:s → ℕ, injective f :=
 ⟨λ ⟨h⟩, by exactI ⟨encode, encode_injective⟩,
  λ ⟨f, h⟩, ⟨⟨f, partial_inv f, partial_inv_left h⟩⟩⟩
@@ -36,13 +36,13 @@ lemma countable_iff_exists_injective {s : set α} :
 on `s`. -/
 lemma countable_iff_exists_inj_on {s : set α} :
   s.countable ↔ ∃ f : α → ℕ, inj_on f s :=
-countable_iff_exists_injective.trans
+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⟩⟩
 
-lemma countable_iff_exists_surjective [ne : nonempty α] {s : set α} :
+protected lemma countable_iff_exists_surjective [ne : nonempty α] {s : set α} :
   s.countable ↔ ∃f:ℕ → α, s ⊆ range f :=
 ⟨λ ⟨h⟩, by inhabit α; exactI ⟨λ n, ((decode s n).map subtype.val).iget,
   λ a as, ⟨encode (⟨a, as⟩ : s), by simp [encodek]⟩⟩,
@@ -69,7 +69,7 @@ have (∃ f : ℕ → s, surjective f) → s.countable, from assume ⟨f, fsurj
 by split; assumption
 
 /-- Convert `set.countable s` to `encodable s` (noncomputable). -/
-def countable.to_encodable {s : set α} : s.countable → encodable s :=
+protected def countable.to_encodable {s : set α} : s.countable → encodable s :=
 classical.choice
 
 lemma countable_encodable' (s : set α) [H : encodable s] : s.countable :=
@@ -86,7 +86,7 @@ begin
   letI : encodable s := countable.to_encodable hc,
   letI : nonempty s := hs.to_subtype,
   have : (univ : set s).countable := countable_encodable _,
-  rcases countable_iff_exists_surjective.1 this with ⟨g, hg⟩,
+  rcases set.countable_iff_exists_surjective.1 this with ⟨g, hg⟩,
   have : range g = univ := univ_subset_iff.1 hg,
   use coe ∘ g,
   simp only [range_comp, this, image_univ, subtype.range_coe]

src/set_theory/cardinal/basic.lean

@@ -1038,7 +1038,7 @@ denumerable_iff.1 ⟨‹_›⟩
 
 @[simp] lemma mk_set_le_aleph_0 (s : set α) : #s ≤ ℵ₀ ↔ s.countable :=
 begin
-  rw [countable_iff_exists_injective], split,
+  rw [set.countable_iff_exists_injective], split,
   { rintro ⟨f'⟩, cases embedding.trans f' equiv.ulift.to_embedding with f hf, exact ⟨f, hf⟩ },
   { rintro ⟨f, hf⟩, exact ⟨embedding.trans ⟨f, hf⟩ equiv.ulift.symm.to_embedding⟩ }
 end

src/topology/bases.lean

@@ -275,7 +275,7 @@ If `α` might be empty, then `exists_countable_dense` is the main way to use sep
 lemma exists_dense_seq [separable_space α] [nonempty α] : ∃ u : ℕ → α, dense_range u :=
 begin
   obtain ⟨s : set α, hs, s_dense⟩ := exists_countable_dense α,
-  cases countable_iff_exists_surjective.mp hs with u hu,
+  cases set.countable_iff_exists_surjective.mp hs with u hu,
   exact ⟨u, s_dense.mono hu⟩,
 end
 

src/topology/metric_space/kuratowski.lean

@@ -91,7 +91,7 @@ begin
     haveI : inhabited α := ⟨basepoint⟩,
     have : ∃s:set α, s.countable ∧ dense s := exists_countable_dense α,
     rcases this with ⟨S, ⟨S_countable, S_dense⟩⟩,
-    rcases countable_iff_exists_surjective.1 S_countable with ⟨x, x_range⟩,
+    rcases set.countable_iff_exists_surjective.1 S_countable with ⟨x, x_range⟩,
     /- Use embedding_of_subset to construct the desired isometry -/
     exact ⟨embedding_of_subset x, embedding_of_subset_isometry x (S_dense.mono x_range)⟩ }
 end