refactor(data/set/countable): golf using _root_.countable, review A…

…PI (#15624)

* add `set.countable_coe_iff`, `set.countable.to_subtype`, `set.to_countable`, `set.countable_univ`, `countable.to_set`, `set.countable.exists_surjective`;
* generalize some lemmas from `[encodable]` to `[countable]`;
* move `section enumerate` up to use it in `countable_iff_exists_subset_range`;
* golf some proofs using facts about `_root_.countable`;
* drop `countable_encodable` and `countable_encodable'`, use `set.to_countable` instead.

src/data/set/countable.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import data.set.finite
+import data.countable.basic
 import logic.equiv.list
 
 /-!
@@ -15,8 +16,8 @@ open function set encodable
 
 open classical (hiding some)
 open_locale classical
-universes u v w
-variables {α : Type u} {β : Type v} {γ : Type w}
+universes u v w x
+variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}
 
 namespace set
 
@@ -27,10 +28,17 @@ constructive analogue of countability. (For the most part, theorems about
 -/
 protected def countable (s : set α) : Prop := nonempty (encodable s)
 
+@[simp] lemma countable_coe_iff {s : set α} : countable s ↔ s.countable := nonempty_encodable.symm
+
+/-- Prove `set.countable` from a `countable` instance on the subtype. -/
+lemma to_countable (s : set α) [countable s] : s.countable := countable_coe_iff.mp ‹_›
+
+/-- Restate `set.countable` as a `countable` instance. -/
+alias countable_coe_iff ↔ _root_.countable.to_set countable.to_subtype
+
 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⟩⟩⟩
+  s.countable ↔ ∃ f : s → ℕ, injective f :=
+countable_coe_iff.symm.trans (countable_iff_exists_injective s)
 
 /-- A set `s : set α` is countable if and only if there exists a function `α → ℕ` injective
 on `s`. -/
@@ -42,71 +50,69 @@ set.countable_iff_exists_injective.trans
      hf $ by simpa [as, bs] using h⟩,
  λ ⟨f, hf⟩, ⟨_, inj_on_iff_injective.1 hf⟩⟩
 
-lemma countable_iff_exists_subset_range [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]⟩⟩,
- λ ⟨f, hf⟩, ⟨⟨
-  λ x, inv_fun f x.1,
-  λ n, if h : f n ∈ s then some ⟨f n, h⟩ else none,
-  λ ⟨x, hx⟩, begin
-    have := inv_fun_eq (hf hx), dsimp at this ⊢,
-    simp [this, hx]
-  end⟩⟩⟩
+/-- Convert `set.countable s` to `encodable s` (noncomputable). -/
+protected def countable.to_encodable {s : set α} : s.countable → encodable s :=
+classical.choice
+
+section enumerate
+
+/-- Noncomputably enumerate elements in a set. The `default` value is used to extend the domain to
+all of `ℕ`. -/
+
+def enumerate_countable {s : set α} (h : s.countable) (default : α) : ℕ → α :=
+assume n, match @encodable.decode s h.to_encodable n with
+        | (some y) := y
+        | (none)   := default
+        end
+
+lemma subset_range_enumerate {s : set α} (h : s.countable) (default : α) :
+   s ⊆ range (enumerate_countable h default) :=
+assume x hx,
+⟨@encodable.encode s h.to_encodable ⟨x, hx⟩,
+by simp [enumerate_countable, encodable.encodek]⟩
+
+end enumerate
+
+lemma countable.mono {s₁ s₂ : set α} (h : s₁ ⊆ s₂) : s₂.countable → s₁.countable
+| ⟨H⟩ := ⟨@of_inj _ _ H _ (embedding_of_subset _ _ h).2⟩
+
+lemma countable_range [countable ι] (f : ι → β) : (range f).countable :=
+surjective_onto_range.countable.to_set
+
+lemma countable_iff_exists_subset_range [nonempty α] {s : set α} :
+  s.countable ↔ ∃ f : ℕ → α, s ⊆ range f :=
+⟨λ h, by { inhabit α, exact ⟨enumerate_countable h default, subset_range_enumerate _ _⟩ },
+  λ ⟨f, hsf⟩, (countable_range f).mono hsf⟩
 
 /--
 A non-empty set is countable iff there exists a surjection from the
 natural numbers onto the subtype induced by the set.
 -/
 protected lemma countable_iff_exists_surjective {s : set α} (hs : s.nonempty) :
   s.countable ↔ ∃ f : ℕ → s, surjective f :=
-have inhabited s, from ⟨classical.choice hs.to_subtype⟩,
-have s.countable → ∃ f : ℕ → s, surjective f, from assume ⟨h⟩,
-  by exactI ⟨λ n, (decode s n).iget, λ a, ⟨encode a, by simp [encodek]⟩⟩,
-have (∃ f : ℕ → s, surjective f) → s.countable, from assume ⟨f, fsurj⟩,
-  ⟨⟨inv_fun f, option.some ∘ f,
-    by intro h; simp [(inv_fun_eq (fsurj h) : f (inv_fun f h) = h)]⟩⟩,
-by split; assumption
+countable_coe_iff.symm.trans $ @countable_iff_exists_surjective s hs.to_subtype
 
-/-- Convert `set.countable s` to `encodable s` (noncomputable). -/
-protected def countable.to_encodable {s : set α} : s.countable → encodable s :=
-classical.choice
-
-lemma countable_encodable' (s : set α) [H : encodable s] : s.countable :=
-⟨H⟩
+alias set.countable_iff_exists_surjective ↔ countable.exists_surjective _
 
-lemma countable_encodable [encodable α] (s : set α) : s.countable :=
-⟨by apply_instance⟩
+lemma countable_univ [countable α] : (univ : set α).countable := to_countable univ
 
 /-- If `s : set α` is a nonempty countable set, then there exists a map
 `f : ℕ → α` such that `s = range f`. -/
 lemma countable.exists_eq_range {s : set α} (hc : s.countable) (hs : s.nonempty) :
   ∃ f : ℕ → α, s = range f :=
 begin
-  letI : encodable s := countable.to_encodable hc,
-  letI : nonempty s := hs.to_subtype,
-  have : (univ : set s).countable := countable_encodable _,
-  rcases set.countable_iff_exists_subset_range.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]
+  rcases hc.exists_surjective hs with ⟨f, hf⟩,
+  refine ⟨coe ∘ f, _⟩,
+  rw [hf.range_comp, subtype.range_coe]
 end
 
-@[simp] lemma countable_empty : (∅ : set α).countable :=
-⟨⟨λ x, x.2.elim, λ n, none, λ x, x.2.elim⟩⟩
+@[simp] lemma countable_empty : (∅ : set α).countable := to_countable _
 
 @[simp] lemma countable_singleton (a : α) : ({a} : set α).countable :=
 ⟨of_equiv _ (equiv.set.singleton a)⟩
 
-lemma countable.mono {s₁ s₂ : set α} (h : s₁ ⊆ s₂) : s₂.countable → s₁.countable
-| ⟨H⟩ := ⟨@of_inj _ _ H _ (embedding_of_subset _ _ h).2⟩
-
 lemma countable.image {s : set α} (hs : s.countable) (f : α → β) : (f '' s).countable :=
-have surjective ((maps_to_image f s).restrict _ _ _), from surjective_maps_to_image_restrict f s,
-⟨@encodable.of_inj _ _ hs.to_encodable (surj_inv this) (injective_surj_inv this)⟩
-
-lemma countable_range [encodable α] (f : α → β) : (range f).countable :=
-by rw ← image_univ; exact (countable_encodable _).image _
+by { rw [image_eq_range], haveI := hs.to_subtype, apply countable_range }
 
 lemma maps_to.countable_of_inj_on {s : set α} {t : set β} {f : α → β}
   (hf : maps_to f s t) (hf' : inj_on f s) (ht : t.countable) :
@@ -148,17 +154,16 @@ lemma countable_of_injective_of_countable_image {s : set α} {f : α → β}
 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 β} [encodable α] (ht : ∀a, (t a).countable) :
+lemma countable_Union {t : ι → set α} [countable ι] (ht : ∀ i, (t i).countable) :
   (⋃a, t a).countable :=
-by haveI := (λ a, (ht a).to_encodable);
-   rw Union_eq_range_sigma; apply countable_range
+by { haveI := λ a, (ht a).to_subtype, rw Union_eq_range_psigma, apply countable_range }
 
 lemma countable.bUnion
   {s : set α} {t : Π x ∈ s, set β} (hs : s.countable) (ht : ∀a∈s, (t a ‹_›).countable) :
   (⋃a∈s, t a ‹_›).countable :=
 begin
   rw bUnion_eq_Union,
-  haveI := hs.to_encodable,
+  haveI := hs.to_subtype,
   exact countable_Union (by simpa using ht)
 end
 
@@ -212,45 +217,29 @@ begin
   simpa using @ts a
 end
 
-lemma countable_pi {π : α → Type*} [fintype α] {s : Πa, set (π a)} (hs : ∀a, (s a).countable) :
+lemma countable_univ_pi {π : α → Type*} [finite α] {s : Π a, set (π a)}
+  (hs : ∀ a, (s a).countable) : (pi univ s).countable :=
+begin
+  haveI := λ a, (hs a).to_subtype,
+  exact (countable.of_equiv _ (equiv.set.univ_pi s).symm).to_set
+end
+
+lemma countable_pi {π : α → Type*} [finite α] {s : Πa, set (π a)} (hs : ∀a, (s a).countable) :
   {f : Πa, π a | ∀a, f a ∈ s a}.countable :=
-countable.mono
-  (show {f : Πa, π a | ∀a, f a ∈ s a} ⊆ range (λf : Πa, s a, λa, (f a).1), from
-    assume f hf, ⟨λa, ⟨f a, hf a⟩, funext $ assume a, rfl⟩) $
-have trunc (encodable (Π (a : α), s a)), from
-  @encodable.fintype_pi α _ _ _ (assume a, (hs a).to_encodable),
-trunc.induction_on this $ assume h,
-@countable_range _ _ h _
+by simpa only [← mem_univ_pi] using countable_univ_pi hs
 
 protected lemma countable.prod {s : set α} {t : set β} (hs : s.countable) (ht : t.countable) :
   set.countable (s ×ˢ t) :=
 begin
-  haveI : encodable s := hs.to_encodable,
-  haveI : encodable t := ht.to_encodable,
-  exact ⟨of_equiv (s × t) (equiv.set.prod _ _)⟩
+  haveI : countable s := hs.to_subtype,
+  haveI : countable t := ht.to_subtype,
+  exact (countable.of_equiv _ $ (equiv.set.prod _ _).symm).to_set
 end
 
 lemma countable.image2 {s : set α} {t : set β} (hs : s.countable) (ht : t.countable)
   (f : α → β → γ) : (image2 f s t).countable :=
 by { rw ← image_prod, exact (hs.prod ht).image _ }
 
-section enumerate
-
-/-- Enumerate elements in a countable set.-/
-def enumerate_countable {s : set α} (h : s.countable) (default : α) : ℕ → α :=
-assume n, match @encodable.decode s h.to_encodable n with
-        | (some y) := y
-        | (none)   := default
-        end
-
-lemma subset_range_enumerate {s : set α} (h : s.countable) (default : α) :
-   s ⊆ range (enumerate_countable h default) :=
-assume x hx,
-⟨@encodable.encode s h.to_encodable ⟨x, hx⟩,
-by simp [enumerate_countable, encodable.encodek]⟩
-
-end enumerate
-
 end set
 
 lemma finset.countable_to_set (s : finset α) : set.countable (↑s : set α) :=

src/dynamics/ergodic/conservative.lean

@@ -82,10 +82,10 @@ begin
   rcases ihN with ⟨n, hn, hμn⟩,
   set T := s ∩ ⋃ n ≥ N + 1, (f^[n]) ⁻¹' s,
   have hT : measurable_set T,
-    from hs.inter (measurable_set.bUnion (countable_encodable _)
+    from hs.inter (measurable_set.bUnion (to_countable _)
       (λ _ _, hf.measurable.iterate _ hs)),
   have hμT : μ T = 0,
-  { convert (measure_bUnion_null_iff $ countable_encodable _).2 hN,
+  { convert (measure_bUnion_null_iff $ to_countable _).2 hN,
     rw ←inter_Union₂, refl },
   have : μ ((s ∩ (f^[n]) ⁻¹' s) \ T) ≠ 0, by rwa [measure_diff_null hμT],
   rcases hf.exists_mem_image_mem ((hs.inter (hf.measurable.iterate n hs)).diff hT) this
@@ -114,7 +114,7 @@ begin
   by_contradiction H,
   have : measurable_set (s ∩ {x | ∀ m ≥ n, f^[m] x ∉ s}),
   { simp only [set_of_forall, ← compl_set_of],
-    exact hs.inter (measurable_set.bInter (countable_encodable _)
+    exact hs.inter (measurable_set.bInter (to_countable _)
       (λ m _, hf.measurable.iterate m hs.compl)) },
   rcases (hf.exists_gt_measure_inter_ne_zero this H) n with ⟨m, hmn, hm⟩,
   rcases nonempty_of_measure_ne_zero hm with ⟨x, ⟨hxs, hxn⟩, hxm, -⟩,

src/measure_theory/constructions/borel_space.lean

@@ -64,7 +64,7 @@ lemma borel_eq_top_of_encodable [topological_space α] [t1_space α] [encodable
   borel α = ⊤ :=
 begin
   refine (top_le_iff.1 $ λ s hs, bUnion_of_singleton s ▸ _),
-  apply measurable_set.bUnion s.countable_encodable,
+  apply measurable_set.bUnion s.to_countable,
   intros x hx,
   apply measurable_set.of_compl,
   apply generate_measurable.basic,
@@ -1281,14 +1281,14 @@ end
 @[measurability]
 lemma measurable_liminf {f : ℕ → δ → α} (hf : ∀ i, measurable (f i)) :
   measurable (λ x, liminf at_top (λ i, f i x)) :=
-measurable_liminf' hf at_top_countable_basis (λ i, countable_encodable _)
+measurable_liminf' hf at_top_countable_basis (λ i, to_countable _)
 
 /-- `limsup` over `ℕ` is measurable. See `measurable_limsup'` for a version with a general filter.
 -/
 @[measurability]
 lemma measurable_limsup {f : ℕ → δ → α} (hf : ∀ i, measurable (f i)) :
   measurable (λ x, limsup at_top (λ i, f i x)) :=
-measurable_limsup' hf at_top_countable_basis (λ i, countable_encodable _)
+measurable_limsup' hf at_top_countable_basis (λ i, to_countable _)
 
 end complete_linear_order
 
@@ -1600,7 +1600,7 @@ begin
     { have hg : ∀ q : ℚ, measurable_set[g] (Iio q) :=
         λ q, generate_measurable.basic (Iio q) (by simp),
       refine @measurable_set.inter _ g _ _ _ (hg _),
-      refine @measurable_set.bUnion _ _ g _ _ (countable_encodable _) (λ c h, _),
+      refine @measurable_set.bUnion _ _ g _ _ (to_countable _) (λ c h, _),
       exact @measurable_set.compl _ _ g (hg _) },
     { suffices : x < ↑b → (↑a < x ↔ ∃ (i : ℚ), a < i ∧ ↑i ≤ x), by simpa,
       refine λ _, ⟨λ h, _, λ ⟨i, hai, hix⟩, (rat.cast_lt.2 hai).trans_le hix⟩,

src/measure_theory/decomposition/unsigned_hahn.lean

@@ -106,7 +106,7 @@ begin
   have hf : ∀n m, measurable_set (f n m),
   { assume n m,
     simp only [f, finset.inf_eq_infi],
-    exact measurable_set.bInter (countable_encodable _) (assume i _, he₁ _) },
+    exact measurable_set.bInter (to_countable _) (assume i _, he₁ _) },
 
   have f_subset_f : ∀{a b c d}, a ≤ b → c ≤ d → f a d ⊆ f b c,
   { assume a b c d hab hcd,

src/measure_theory/integral/integral_eq_improper.lean

@@ -312,7 +312,7 @@ lemma ae_cover.bUnion_Iic_ae_cover [preorder ι] {φ : ι → set α} (hφ : ae_
   ae_cover μ at_top (λ (n : ι), ⋃ k (h : k ∈ Iic n), φ k) :=
 { ae_eventually_mem := hφ.ae_eventually_mem.mono
     (λ x h, h.mono (λ i hi, mem_bUnion right_mem_Iic hi)),
-  measurable := λ i, measurable_set.bUnion (countable_encodable _) (λ n _, hφ.measurable n) }
+  measurable := λ i, measurable_set.bUnion (to_countable _) (λ n _, hφ.measurable n) }
 
 lemma ae_cover.bInter_Ici_ae_cover [semilattice_sup ι] [nonempty ι] {φ : ι → set α}
   (hφ : ae_cover μ at_top φ) : ae_cover μ at_top (λ (n : ι), ⋂ k (h : k ∈ Ici n), φ k) :=
@@ -325,7 +325,7 @@ lemma ae_cover.bInter_Ici_ae_cover [semilattice_sup ι] [nonempty ι] {φ : ι 
       intros j hj,
       exact mem_bInter (λ k hk, hi k (le_trans hj hk)),
     end,
-  measurable := λ i, measurable_set.bInter (countable_encodable _) (λ n _, hφ.measurable n) }
+  measurable := λ i, measurable_set.bInter (to_countable _) (λ n _, hφ.measurable n) }
 
 end ae_cover_Union_Inter_encodable
 

src/measure_theory/integral/lebesgue.lean

@@ -1824,7 +1824,7 @@ calc
      by simp only [liminf_eq_supr_infi_of_nat]
   ... = ⨆n:ℕ, ∫⁻ a, ⨅i≥n, f i a ∂μ :
     lintegral_supr'
-      (assume n, ae_measurable_binfi _ (countable_encodable _) h_meas)
+      (assume n, ae_measurable_binfi _ (to_countable _) h_meas)
       (ae_of_all μ (assume a n m hnm, infi_le_infi_of_subset $ λ i hi, le_trans hnm hi))
   ... ≤ ⨆n:ℕ, ⨅i≥n, ∫⁻ a, f i a ∂μ :
     supr_mono $ λ n, le_infi₂_lintegral _
@@ -1846,7 +1846,7 @@ calc
   ... = ∫⁻ a, ⨅n:ℕ, ⨆i≥n, f i a ∂μ :
     begin
       refine (lintegral_infi _ _ _).symm,
-      { assume n, exact measurable_bsupr _ (countable_encodable _) hf_meas },
+      { assume n, exact measurable_bsupr _ (to_countable _) hf_meas },
       { assume n m hnm a, exact (supr_le_supr_of_subset $ λ i hi, le_trans hnm hi) },
       { refine ne_top_of_le_ne_top h_fin (lintegral_mono_ae _),
         refine (ae_all_iff.2 h_bound).mono (λ n hn, _),

src/measure_theory/measurable_space.lean

@@ -679,7 +679,7 @@ by { rw [pi_def], exact measurable_set.bInter hs (λ i hi, measurable_pi_apply _
 
 lemma measurable_set.univ_pi [encodable δ] {t : Π i : δ, set (π i)}
   (ht : ∀ i, measurable_set (t i)) : measurable_set (pi univ t) :=
-measurable_set.pi (countable_encodable _) (λ i _, ht i)
+measurable_set.pi (to_countable _) (λ i _, ht i)
 
 lemma measurable_set_pi_of_nonempty
   {s : set δ} {t : Π i, set (π i)} (hs : s.countable)
@@ -735,7 +735,7 @@ local attribute [instance] fintype.to_encodable
 
 lemma measurable_set.pi_fintype [fintype δ] {s : set δ} {t : Π i, set (π i)}
   (ht : ∀ i ∈ s, measurable_set (t i)) : measurable_set (pi s t) :=
-measurable_set.pi (countable_encodable _) ht
+measurable_set.pi (to_countable _) ht
 
 lemma measurable_set.univ_pi_fintype [fintype δ] {t : Π i, set (π i)}
   (ht : ∀ i, measurable_set (t i)) : measurable_set (pi univ t) :=

src/measure_theory/measure/ae_disjoint.lean

@@ -33,8 +33,8 @@ lemma exists_null_pairwise_disjoint_diff [encodable ι] {s : ι → set α}
 begin
   refine ⟨λ i, to_measurable μ (s i ∩ ⋃ j ∈ ({i}ᶜ : set ι), s j),
     λ i, measurable_set_to_measurable _ _, λ i, _, _⟩,
-  { simp only [measure_to_measurable, inter_Union, measure_bUnion_null_iff (countable_encodable _)],
-    exact λ j hj, hd _ _ (ne.symm hj) },
+  { simp only [measure_to_measurable, inter_Union],
+    exact (measure_bUnion_null_iff $ to_countable _).2 (λ j hj, hd _ _ (ne.symm hj)) },
   { simp only [pairwise, disjoint_left, on_fun, mem_diff, not_and, and_imp, not_not],
     intros i j hne x hi hU hj,
     replace hU : x ∉ s i ∩ ⋃ j ≠ i, s j := λ h, hU (subset_to_measurable _ _ h),

src/measure_theory/measure/measure_space.lean

@@ -1630,7 +1630,7 @@ lemma map_eq_sum [encodable β] [measurable_singleton_class β]
 begin
   ext1 s hs,
   have : ∀ y ∈ s, measurable_set (f ⁻¹' {y}), from λ y _, hf (measurable_set_singleton _),
-  simp [← tsum_measure_preimage_singleton (countable_encodable s) this, *,
+  simp [← tsum_measure_preimage_singleton (to_countable s) this, *,
     tsum_subtype s (λ b, μ (f ⁻¹' {b})), ← indicator_mul_right s (λ b, μ (f ⁻¹' {b}))]
 end
 

src/model_theory/fraisse.lean

@@ -238,7 +238,7 @@ begin
   { rintros ⟨Kn, eqinv, cq, hfg, hp, jep⟩,
     obtain ⟨M, hM, rfl⟩ := exists_cg_is_age_of Kn eqinv cq hfg hp jep,
     haveI := ((Structure.cg_iff_countable).1 hM).some,
-    refine ⟨M, countable_encodable _, rfl⟩, }
+    refine ⟨M, to_countable _, rfl⟩, }
 end
 
 variables {K} (L) (M)

src/number_theory/liouville/measure.lean

@@ -75,7 +75,7 @@ begin
   simp only [← set_of_exists],
   refine measure_mono_null set_of_liouville_with_subset_aux _,
   rw measure_Union_null_iff, intro m, rw measure_preimage_add_right, clear m,
-  refine (measure_bUnion_null_iff $ countable_encodable _).2 (λ n (hn : 1 ≤ n), _),
+  refine (measure_bUnion_null_iff $ to_countable _).2 (λ n (hn : 1 ≤ n), _),
   generalize hr : (2 + 1 / n : ℝ) = r,
   replace hr : 2 < r, by simp [← hr, zero_lt_one.trans_le hn], clear hn n,
   refine measure_set_of_frequently_eq_zero _,