refactor(set_theory/cardinal/basic): migrate from fintype to finite (#15175)

* add `finite_iff_exists_equiv_fin`;
* add `cardinal.mk_eq_nat_iff` and `cardinal.lt_aleph_0_iff_finite`;
* rename the old `cardinal.lt_aleph_0_iff_finite` to `cardinal.lt_aleph_0_iff_finite_set`;
* rename `cardinal.lt_aleph_0_of_fintype` to `cardinal.lt_aleph_0_of_finite`, assume `[finite]` instead of `[fintype]`;
* add an alias `set.finite.lt_aleph_0`;
* rename `W_type.cardinal_mk_le_max_aleph_0_of_fintype` to `W_type.cardinal_mk_le_max_aleph_0_of_finite`, fix assumption.

Author: urkud

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -509,7 +509,7 @@ omit h
 /-- The infinite sequence of cubes contradicts the finiteness of the family. -/
 theorem not_correct : ¬correct cs :=
 begin
-  intro h, apply (lt_aleph_0_of_fintype ι).not_le,
+  intro h, apply (lt_aleph_0_of_finite ι).not_le,
   rw [aleph_0, lift_id], fapply mk_le_of_injective, exact λ n, (sequence_of_cubes h n).1,
   intros n m hnm, apply (strict_anti_sequence_of_cubes h).injective,
   dsimp only [decreasing_sequence], rw hnm

src/data/W/cardinal.lean

@@ -51,7 +51,7 @@ end
 
 /-- If, for any `a : α`, `β a` is finite, then the cardinality of `W_type β`
   is at most the maximum of the cardinality of `α` and `ℵ₀`  -/
-lemma cardinal_mk_le_max_aleph_0_of_fintype [Π a, fintype (β a)] : #(W_type β) ≤ max (#α) ℵ₀ :=
+lemma cardinal_mk_le_max_aleph_0_of_finite [∀ a, finite (β a)] : #(W_type β) ≤ max (#α) ℵ₀ :=
 (is_empty_or_nonempty α).elim
   (begin
     introI h,
@@ -63,7 +63,7 @@ calc cardinal.sum (λ a, m ^ #(β a))
     ≤ #α * ⨆ a, m ^ #(β a) : cardinal.sum_le_supr _
 ... ≤ m * ⨆ a, m ^ #(β a) : mul_le_mul' (le_max_left _ _) le_rfl
 ... = m : mul_eq_left.{u} (le_max_right _ _)
-  (csupr_le' $ λ i, pow_le (le_max_right _ _) (lt_aleph_0_of_fintype _)) $
+  (csupr_le' $ λ i, pow_le (le_max_right _ _) (lt_aleph_0_of_finite _)) $
   pos_iff_ne_zero.1 $ order.succ_le_iff.1
     begin
       rw succ_zero,

src/data/finite/basic.lean

@@ -71,8 +71,11 @@ in this way to allow there to be `finite` instances for propositions.
 class inductive finite (α : Sort*) : Prop
 | intro {n : ℕ} : α ≃ fin n → finite
 
+lemma finite_iff_exists_equiv_fin {α : Sort*} : finite α ↔ ∃ n, nonempty (α ≃ fin n) :=
+⟨λ ⟨e⟩, ⟨_, ⟨e⟩⟩, λ ⟨n, ⟨e⟩⟩, ⟨e⟩⟩
+
 lemma finite.exists_equiv_fin (α : Sort*) [h : finite α] : ∃ (n : ℕ), nonempty (α ≃ fin n) :=
-by { casesI h with n f, exact ⟨n, ⟨f⟩⟩ }
+finite_iff_exists_equiv_fin.mp h
 
 lemma finite.of_equiv (α : Sort*) {β : Sort*} [h : finite α] (f : α ≃ β) : finite β :=
 by { casesI h with n e, exact finite.intro (f.symm.trans e) }

src/data/mv_polynomial/cardinal.lean

@@ -85,7 +85,7 @@ calc #(mv_polynomial_fun σ R) = #R + #σ + #(ulift bool) :
 ... ≤ max (max (max (max (#R) (#σ)) ℵ₀) (#(ulift bool))) ℵ₀ :
   max_le_max (max_le_max (add_le_max _ _) le_rfl) le_rfl
 ... ≤ _ : by simp only [max_comm ℵ₀, max_assoc, max_left_comm ℵ₀, max_self,
-            max_eq_left (lt_aleph_0_of_fintype (ulift.{u} bool)).le]
+            max_eq_left (lt_aleph_0_of_finite (ulift.{u} bool)).le]
 
 namespace mv_polynomial
 
@@ -95,7 +95,7 @@ lemma cardinal_mk_le_max {σ R : Type u} [comm_semiring R] :
   #(mv_polynomial σ R) ≤ max (max (#R) (#σ)) ℵ₀ :=
 calc #(mv_polynomial σ R) ≤ #(W_type (arity σ R)) :
   cardinal.mk_le_of_surjective to_mv_polynomial_surjective
-... ≤ max (#(mv_polynomial_fun σ R)) ℵ₀ : W_type.cardinal_mk_le_max_aleph_0_of_fintype
+... ≤ max (#(mv_polynomial_fun σ R)) ℵ₀ : W_type.cardinal_mk_le_max_aleph_0_of_finite
 ... ≤ _ : max_le_max cardinal_mv_polynomial_fun_le le_rfl
 ... ≤ _ : by simp only [max_assoc, max_self]
 

src/data/polynomial/cardinal.lean

@@ -22,6 +22,6 @@ lemma cardinal_mk_le_max {R : Type u} [comm_semiring R] : #R[X] ≤ max (#R) ℵ
 calc #R[X] = #(mv_polynomial punit.{u + 1} R) :
   cardinal.eq.2 ⟨(mv_polynomial.punit_alg_equiv.{u u} R).to_equiv.symm⟩
 ... ≤ _ : mv_polynomial.cardinal_mk_le_max
-... ≤ _ : by rw [max_assoc, max_eq_right (lt_aleph_0_of_fintype punit).le]
+... ≤ _ : by rw [max_assoc, max_eq_right (lt_aleph_0_of_finite punit).le]
 
 end polynomial

src/field_theory/finiteness.lean

@@ -27,7 +27,7 @@ its dimension (as a cardinal) is strictly less than the first infinite cardinal
 lemma iff_dim_lt_aleph_0 : is_noetherian K V ↔ module.rank K V < ℵ₀ :=
 begin
   let b := basis.of_vector_space K V,
-  rw [← b.mk_eq_dim'', lt_aleph_0_iff_finite],
+  rw [← b.mk_eq_dim'', lt_aleph_0_iff_set_finite],
   split,
   { introI,
     exact finite_of_linear_independent (basis.of_vector_space_index.linear_independent K V) },
@@ -104,7 +104,7 @@ begin
     exact ⟨⟨finset_basis_index K V, by { convert (finset_basis K V).span_eq, simp }⟩⟩ },
   { rintros ⟨s, hs⟩,
     rw [is_noetherian.iff_dim_lt_aleph_0, ← dim_top, ← hs],
-    exact lt_of_le_of_lt (dim_span_le _) (lt_aleph_0_iff_finite.2 (set.finite_mem_finset s)) }
+    exact lt_of_le_of_lt (dim_span_le _) s.finite_to_set.lt_aleph_0 }
 end
 
 end is_noetherian

src/field_theory/is_alg_closed/classification.lean

@@ -66,7 +66,7 @@ calc #L ≤ #(Σ p : R[X], { x : L // x ∈ (p.map (algebra_map R L)).roots }) :
     rw [lt_aleph_0_iff_finite],
     classical,
     simp only [← @multiset.mem_to_finset _ _ _ (p.map (algebra_map R L)).roots],
-    exact set.finite_mem_finset _,
+    apply_instance
   end)
 ... = #R[X] * ℵ₀ : sum_const' _ _
 ... ≤ max (max (#R[X]) ℵ₀) ℵ₀ : mul_le_max _ _
@@ -192,9 +192,9 @@ begin
       from ring_hom.injective _) with t ht,
   have : #s = #t,
   { rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph_0_lt _ hs
-      (lt_aleph_0_of_fintype (zmod p)).le hK,
+      (lt_aleph_0_of_finite (zmod p)).le hK,
         ← cardinal_eq_cardinal_transcendence_basis_of_aleph_0_lt _ ht
-      (lt_aleph_0_of_fintype (zmod p)).le, hKL],
+      (lt_aleph_0_of_finite (zmod p)).le, hKL],
     rwa ← hKL },
   cases cardinal.eq.1 this with e,
   exact ⟨equiv_of_transcendence_basis _ _ e hs ht⟩

src/linear_algebra/dimension.lean

@@ -617,7 +617,7 @@ begin
     { exact not_le_of_lt this ⟨set.embedding_of_subset _ _ hs⟩ },
     refine lt_of_le_of_lt (le_trans cardinal.mk_Union_le_sum_mk
       (cardinal.sum_le_sum _ (λ _, ℵ₀) _)) _,
-    { exact λ j, (cardinal.lt_aleph_0_of_fintype _).le },
+    { exact λ j, (cardinal.lt_aleph_0_of_finite _).le },
     { simpa } },
 end
 

src/linear_algebra/finsupp_vector_space.lean

@@ -198,7 +198,7 @@ lemma cardinal_lt_aleph_0_of_finite_dimensional [fintype K] [finite_dimensional
 begin
   letI : is_noetherian K V := is_noetherian.iff_fg.2 infer_instance,
   rw cardinal_mk_eq_cardinal_mk_field_pow_dim K V,
-  exact cardinal.power_lt_aleph_0 (cardinal.lt_aleph_0_of_fintype K)
+  exact cardinal.power_lt_aleph_0 (cardinal.lt_aleph_0_of_finite K)
     (is_noetherian.dim_lt_aleph_0 K V),
 end
 

src/set_theory/cardinal/basic.lean

@@ -924,18 +924,22 @@ theorem aleph_0_le {c : cardinal} : ℵ₀ ≤ c ↔ ∀ n : ℕ, ↑n ≤ c :=
   exact (nat.lt_succ_self _).not_le (nat_cast_le.1 (h (n+1)))
 end⟩
 
+theorem mk_eq_nat_iff {α : Type u} {n : ℕ} : #α = n ↔ nonempty (α ≃ fin n) :=
+by rw [← lift_mk_fin, ← lift_uzero (#α), lift_mk_eq']
+
+theorem lt_aleph_0_iff_finite {α : Type u} : #α < ℵ₀ ↔ finite α :=
+by simp only [lt_aleph_0, mk_eq_nat_iff, finite_iff_exists_equiv_fin]
+
 theorem lt_aleph_0_iff_fintype {α : Type u} : #α < ℵ₀ ↔ nonempty (fintype α) :=
-lt_aleph_0.trans ⟨λ ⟨n, e⟩, begin
-  rw [← lift_mk_fin n] at e,
-  cases quotient.exact e with f,
-  exact ⟨fintype.of_equiv _ f.symm⟩
-end, λ ⟨_⟩, by exactI ⟨_, mk_fintype _⟩⟩
+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_of_fintype (α : Type u) [fintype α] : #α < ℵ₀ :=
-lt_aleph_0_iff_fintype.2 ⟨infer_instance⟩
+theorem lt_aleph_0_iff_set_finite {α} {S : set α} : #S < ℵ₀ ↔ S.finite :=
+lt_aleph_0_iff_finite.trans finite_coe_iff
 
-theorem lt_aleph_0_iff_finite {α} {S : set α} : #S < ℵ₀ ↔ S.finite :=
-lt_aleph_0_iff_fintype.trans finite_def.symm
+alias lt_aleph_0_iff_set_finite ↔ _ _root_.set.finite.lt_aleph_0
 
 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⟩⟩
@@ -1015,7 +1019,7 @@ calc #α = 1 ↔ #α ≤ 1 ∧ 1 ≤ #α : le_antisymm_iff
   le_one_iff_subsingleton.and (one_le_iff_ne_zero.trans mk_ne_zero_iff)
 
 theorem infinite_iff {α : Type u} : infinite α ↔ ℵ₀ ≤ #α :=
-by rw [←not_lt, lt_aleph_0_iff_fintype, not_nonempty_iff, is_empty_fintype]
+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 ‹_›
 
@@ -1316,14 +1320,14 @@ lemma mk_bUnion_le {ι α : Type u} (A : ι → set α) (s : set ι) :
 by { rw bUnion_eq_Union, apply mk_Union_le }
 
 lemma finset_card_lt_aleph_0 (s : finset α) : #(↑s : set α) < ℵ₀ :=
-by { rw lt_aleph_0_iff_fintype, exact ⟨finset.subtype.fintype s⟩ }
+lt_aleph_0_of_finite _
 
 theorem mk_eq_nat_iff_finset {α} {s : set α} {n : ℕ} :
   #s = n ↔ ∃ t : finset α, (t : set α) = s ∧ t.card = n :=
 begin
   split,
   { intro h,
-    lift s to finset α using lt_aleph_0_iff_finite.1 (h.symm ▸ nat_lt_aleph_0 n),
+    lift s to finset α using lt_aleph_0_iff_set_finite.1 (h.symm ▸ nat_lt_aleph_0 n),
     simpa using h },
   { rintro ⟨t, rfl, rfl⟩,
     exact mk_coe_finset }