refactor(set_theory/basic): match x < ℵ₀ lemmas with x ≤ ℵ₀ lemmas (#15662)

vihdzp · urkud · vihdzp · commit 1c4e18434eeb · 2022-09-12T11:04:51.000Z
* Mark `cardinal.lt_aleph_0_iff_set_finite` as `@[simp]` lemma.
* Add `cardinal.lt_aleph_0_iff_subtype_finite` and `cardinal.mk_le_aleph_0_iff`; drop `cardinal.encodable_iff`.
* Rename `cardinal.mk_set_le_aleph_0` to `cardinal.le_aleph_0_iff_set_countable`.
* Rename `cardinal.mk_subtype_le_aleph_0` to `cardinal.le_aleph_0_iff_subtype_countable`.
* Make `first_order.language.countable` protected.
* Use `[countable _]` instead of `[encodable _]` or `[nonempty (encodable _)]` here and there.



Co-authored-by: Yury G. Kudryashov &lt;urkud@urkud.name&gt;
diff --git a/src/algebra/algebraic_card.lean b/src/algebra/algebraic_card.lean
@@ -73,7 +73,7 @@ variable [encodable R]
 
 @[simp] theorem countable_of_encodable : set.countable {x : A | is_algebraic R x} :=
 begin
-  rw [←mk_set_le_aleph_0, ←lift_le],
+  rw [←le_aleph_0_iff_set_countable, ←lift_le],
   apply (cardinal_mk_lift_le_max R A).trans,
   simp
 end
diff --git a/src/analysis/complex/cauchy_integral.lean b/src/analysis/complex/cauchy_integral.lean
@@ -477,7 +477,8 @@ begin
   { refine nonempty_diff.2 (λ hsub, _),
     have : (Ioo l u).countable,
       from (hs.preimage ((add_right_injective w).comp of_real_injective)).mono hsub,
-    rw [← cardinal.mk_set_le_aleph_0, cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this,
+    rw [← cardinal.le_aleph_0_iff_set_countable,
+      cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this,
     exact this.not_lt cardinal.aleph_0_lt_continuum },
   exact ⟨g x, (hlu_sub hx.1).1, (hlu_sub hx.1).2, hx.2⟩
 end
diff --git a/src/data/complex/cardinality.lean b/src/data/complex/cardinality.lean
@@ -27,4 +27,4 @@ by rw [mk_univ, mk_complex]
 
 /-- The complex numbers are not countable. -/
 lemma not_countable_complex : ¬ (set.univ : set ℂ).countable :=
-by { rw [← mk_set_le_aleph_0, not_le, mk_univ_complex], apply cantor }
+by { rw [← le_aleph_0_iff_set_countable, not_le, mk_univ_complex], apply cantor }
diff --git a/src/data/real/cardinality.lean b/src/data/real/cardinality.lean
@@ -164,7 +164,7 @@ by rw [mk_univ, mk_real]
 
 /-- **Non-Denumerability of the Continuum**: The reals are not countable. -/
 lemma not_countable_real : ¬ (set.univ : set ℝ).countable :=
-by { rw [← mk_set_le_aleph_0, not_le, mk_univ_real], apply cantor }
+by { rw [← le_aleph_0_iff_set_countable, not_le, mk_univ_real], apply cantor }
 
 /-- The cardinality of the interval (a, ∞). -/
 lemma mk_Ioi_real (a : ℝ) : #(Ioi a) = 𝔠 :=
diff --git a/src/model_theory/basic.lean b/src/model_theory/basic.lean
@@ -35,6 +35,10 @@ structures.
   to the `L`-structure `N` that commutes with the interpretations of functions, and which preserves
   the interpretations of relations in both directions.
 
+## TODO
+
+Use `[countable L.symbols]` instead of `[L.countable]`.
+
 ## References
 For the Flypitch project:
 - [J. Han, F. van Doorn, *A formal proof of the independence of the continuum hypothesis*]
@@ -125,7 +129,7 @@ rfl
 def card : cardinal := # L.symbols
 
 /-- A language is countable when it has countably many symbols. -/
-class countable : Prop := (card_le_aleph_0' : L.card ≤ ℵ₀)
+@[protected] class countable : Prop := (card_le_aleph_0' : L.card ≤ ℵ₀)
 
 lemma card_le_aleph_0 [L.countable] : L.card ≤ ℵ₀ := countable.card_le_aleph_0'
 
@@ -194,8 +198,8 @@ instance subsingleton_mk₂_relations {c f₁ f₂ : Type u} {r₁ r₂ : Type v
 nat.cases_on n ⟨λ x, pempty.elim x⟩
   (λ n, nat.cases_on n h1 (λ n, nat.cases_on n h2 (λ n, ⟨λ x, pempty.elim x⟩)))
 
-lemma encodable.countable [h : encodable L.symbols] : L.countable :=
-⟨cardinal.encodable_iff.1 ⟨h⟩⟩
+lemma encodable.countable [_root_.countable L.symbols] : L.countable :=
+⟨cardinal.mk_le_aleph_0⟩
 
 @[simp] lemma empty_card : language.empty.card = 0 :=
 by simp [card_eq_card_functions_add_card_relations]
@@ -211,7 +215,7 @@ instance countable_empty : language.empty.countable :=
 end⟩
 
 lemma encodable.countable_functions [h : encodable (Σl, L.functions l)] : L.countable_functions :=
-⟨cardinal.encodable_iff.1 ⟨h⟩⟩
+⟨cardinal.mk_le_aleph_0⟩
 
 @[priority 100] instance is_relational.countable_functions [L.is_relational] :
   L.countable_functions :=
diff --git a/src/model_theory/encoding.lean b/src/model_theory/encoding.lean
@@ -117,13 +117,10 @@ begin
     rw [mk_nat, lift_aleph_0, mul_eq_max_of_aleph_0_le_left le_rfl, max_le_iff,
       csupr_le_iff' (bdd_above_range _)],
     { refine ⟨le_max_left _ _, λ i, card_le.trans _⟩,
-      rw max_le_iff,
-      refine ⟨le_max_left _ _, _⟩,
+      refine max_le (le_max_left _ _) _,
       rw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (cardinal.lift (#α)), lift_add,
-        add_assoc, lift_lift, lift_lift],
-      refine add_le_add_right _ _,
-      rw [lift_le_aleph_0, ← encodable_iff],
-      exact ⟨infer_instance⟩ },
+        add_assoc, lift_lift, lift_lift, mk_fin, lift_nat_cast],
+      exact add_le_add_right (nat_lt_aleph_0 _).le _ },
     { rw [← one_le_iff_ne_zero],
       refine trans _ (le_csupr (bdd_above_range _) 1),
       rw [one_le_iff_ne_zero, mk_ne_zero_iff],
@@ -154,13 +151,13 @@ encodable.of_left_injection list_encode (λ l, (list_decode l).head'.join)
     simp only [option.join, head', list.map, option.some_bind, id.def],
   end)
 
-lemma card_le_aleph_0 [h1 : nonempty (encodable α)] [h2 : L.countable_functions] :
+lemma card_le_aleph_0 [h1 : countable α] [h2 : L.countable_functions] :
   # (L.term α) ≤ ℵ₀ :=
 begin
   refine (card_le.trans _),
   rw [max_le_iff],
   simp only [le_refl, mk_sum, add_le_aleph_0, lift_le_aleph_0, true_and],
-  exact ⟨encodable_iff.1 h1, L.card_functions_le_aleph_0⟩,
+  exact ⟨mk_le_aleph_0, L.card_functions_le_aleph_0⟩,
 end
 
 instance small [small.{u} α] :
diff --git a/src/model_theory/finitely_generated.lean b/src/model_theory/finitely_generated.lean
@@ -157,9 +157,9 @@ begin
 end
 
 theorem cg_iff_countable [L.countable_functions] {s : L.substructure M} :
-  s.cg ↔ nonempty (encodable s) :=
+  s.cg ↔ countable s :=
 begin
-  refine ⟨_, λ h, ⟨s, h, s.closure_eq⟩⟩,
+  refine ⟨_, λ h, ⟨s, h.to_set, s.closure_eq⟩⟩,
   rintro ⟨s, h, rfl⟩,
   exact h.substructure_closure L
 end
@@ -224,10 +224,8 @@ begin
   exact h.range f,
 end
 
-lemma cg_iff_countable [L.countable_functions] :
-  cg L M ↔ nonempty (encodable M) :=
-by rw [cg_def, cg_iff_countable, cardinal.encodable_iff, cardinal.encodable_iff,
-  top_equiv.to_equiv.cardinal_eq]
+lemma cg_iff_countable [L.countable_functions] : cg L M ↔ countable M :=
+by rw [cg_def, cg_iff_countable, top_equiv.to_equiv.countable_iff]
 
 lemma fg.cg (h : fg L M) : cg L M :=
 cg_def.2 (fg_def.1 h).cg
diff --git a/src/model_theory/fraisse.lean b/src/model_theory/fraisse.lean
@@ -237,8 +237,8 @@ begin
       age.hereditary M, age.joint_embedding M⟩, },
   { 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, to_countable _, rfl⟩, }
+    haveI : countable M := Structure.cg_iff_countable.1 hM,
+    exact ⟨M, to_countable _, rfl⟩, }
 end
 
 variables {K} (L) (M)
diff --git a/src/model_theory/substructures.lean b/src/model_theory/substructures.lean
@@ -274,10 +274,10 @@ variable (L)
 
 lemma _root_.set.countable.substructure_closure
   [L.countable_functions] (h : s.countable) :
-  nonempty (encodable (closure L s)) :=
+  countable (closure L s) :=
 begin
-  haveI : nonempty (encodable s) := h,
-  rw [encodable_iff, ← lift_le_aleph_0],
+  haveI : countable s := h.to_subtype,
+  rw [← mk_le_aleph_0_iff, ← lift_le_aleph_0],
   exact lift_card_closure_le_card_term.trans term.card_le_aleph_0,
 end
 
diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean
@@ -979,11 +979,29 @@ lt_aleph_0_iff_finite.trans (finite_iff_nonempty_fintype _)
 theorem lt_aleph_0_of_finite (α : Type u) [finite α] : #α < ℵ₀ :=
 lt_aleph_0_iff_finite.2 ‹_›
 
-theorem lt_aleph_0_iff_set_finite {α} {S : set α} : #S < ℵ₀ ↔ S.finite :=
+@[simp] theorem lt_aleph_0_iff_set_finite {S : set α} : #S < ℵ₀ ↔ S.finite :=
 lt_aleph_0_iff_finite.trans finite_coe_iff
 
 alias lt_aleph_0_iff_set_finite ↔ _ _root_.set.finite.lt_aleph_0
 
+@[simp] theorem lt_aleph_0_iff_subtype_finite {p : α → Prop} :
+  #{x // p x} < ℵ₀ ↔ {x | p x}.finite :=
+lt_aleph_0_iff_set_finite
+
+lemma mk_le_aleph_0_iff : #α ≤ ℵ₀ ↔ countable α :=
+by rw [countable_iff_nonempty_embedding, aleph_0, ← lift_uzero (#α), lift_mk_le']
+
+@[simp] lemma mk_le_aleph_0 [countable α] : #α ≤ ℵ₀ := mk_le_aleph_0_iff.mpr ‹_›
+
+@[simp] lemma le_aleph_0_iff_set_countable {s : set α} : #s ≤ ℵ₀ ↔ s.countable :=
+by rw [mk_le_aleph_0_iff, countable_coe_iff]
+
+alias le_aleph_0_iff_set_countable ↔ _ _root_.set.countable.le_aleph_0
+
+@[simp] lemma le_aleph_0_iff_subtype_countable {p : α → Prop} :
+  #{x // p x} ≤ ℵ₀ ↔ {x | p x}.countable :=
+le_aleph_0_iff_set_countable
+
 instance can_lift_cardinal_nat : can_lift cardinal ℕ :=
 ⟨ coe, λ x, x < ℵ₀, λ x hx, let ⟨n, hn⟩ := lt_aleph_0.mp hx in ⟨n, hn.symm⟩⟩
 
@@ -1066,30 +1084,13 @@ by rw [← not_lt, lt_aleph_0_iff_finite, not_finite_iff_infinite]
 
 @[simp] lemma aleph_0_le_mk (α : Type u) [infinite α] : ℵ₀ ≤ #α := infinite_iff.1 ‹_›
 
-lemma encodable_iff {α : Type u} : nonempty (encodable α) ↔ #α ≤ ℵ₀ :=
-⟨λ ⟨h⟩, ⟨(@encodable.encode' α h).trans equiv.ulift.symm.to_embedding⟩,
-  λ ⟨h⟩, ⟨encodable.of_inj _ (h.trans equiv.ulift.to_embedding).injective⟩⟩
-
-@[simp] lemma mk_le_aleph_0 [countable α] : #α ≤ ℵ₀ :=
-encodable_iff.1 $ encodable.nonempty_encodable.2 ‹_›
-
 lemma denumerable_iff {α : Type u} : nonempty (denumerable α) ↔ #α = ℵ₀ :=
 ⟨λ ⟨h⟩, mk_congr ((@denumerable.eqv α h).trans equiv.ulift.symm),
  λ h, by { cases quotient.exact h with f, exact ⟨denumerable.mk' $ f.trans equiv.ulift⟩ }⟩
 
 @[simp] lemma mk_denumerable (α : Type u) [denumerable α] : #α = ℵ₀ :=
 denumerable_iff.1 ⟨‹_›⟩
 
-@[simp] lemma mk_set_le_aleph_0 (s : set α) : #s ≤ ℵ₀ ↔ s.countable :=
-begin
-  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
-
-@[simp] lemma mk_subtype_le_aleph_0 (p : α → Prop) : #{x // p x} ≤ ℵ₀ ↔ {x | p x}.countable :=
-mk_set_le_aleph_0 _
-
 @[simp] lemma aleph_0_add_aleph_0 : ℵ₀ + ℵ₀ = ℵ₀ := mk_denumerable _
 
 lemma aleph_0_mul_aleph_0 : ℵ₀ * ℵ₀ = ℵ₀ := mk_denumerable _
diff --git a/src/set_theory/cardinal/ordinal.lean b/src/set_theory/cardinal/ordinal.lean
@@ -284,7 +284,7 @@ lemma aleph_0_lt_aleph_one : ℵ₀ < aleph 1 :=
 by { rw ←succ_aleph_0, apply lt_succ }
 
 lemma countable_iff_lt_aleph_one {α : Type*} (s : set α) : s.countable ↔ #s < aleph 1 :=
-by rw [←succ_aleph_0, lt_succ_iff, mk_set_le_aleph_0]
+by rw [←succ_aleph_0, lt_succ_iff, le_aleph_0_iff_set_countable]
 
 /-- Ordinals that are cardinals are unbounded. -/
 theorem ord_card_unbounded : unbounded (<) {b : ordinal | b.card.ord = b} :=
