refactor(data/{finite,fintype}): redefine infinite in terms of finite, move to data.finite.defs (#16390)

Author: urkud

src/data/finite/basic.lean

@@ -18,7 +18,6 @@ defined.
   former lemma takes `fintype α` as an explicit argument while the latter takes it as an instance
   argument.
 * `fintype.of_finite` noncomputably creates a `fintype` instance from a `finite` instance.
-* `finite_or_infinite` is that every type is either `finite` or `infinite`.
 
 ## Implementation notes
 
@@ -42,13 +41,6 @@ open_locale classical
 
 variables {α β γ : Type*}
 
-lemma finite_or_infinite (α : Type*) :
-  finite α ∨ infinite α :=
-begin
-  rw ← not_finite_iff_infinite,
-  apply em
-end
-
 namespace finite
 
 @[priority 100] -- see Note [lower instance priority]

src/data/finite/defs.lean

@@ -9,7 +9,8 @@ import logic.equiv.basic
 # Definition of the `finite` typeclass
 
 This file defines a typeclass `finite` saying that `α : Sort*` is finite. A type is `finite` if it
-is equivalent to `fin n` for some `n`.
+is equivalent to `fin n` for some `n`. We also define `infinite α` as a typeclass equivalent to
+`¬finite α`.
 
 The `finite` predicate has no computational relevance and, being `Prop`-valued, gets to enjoy proof
 irrelevance -- it represents the mere fact that the type is finite.  While the `fintype` class also
@@ -26,6 +27,7 @@ instead.
 ## Main definitions
 
 * `finite α` denotes that `α` is a finite type.
+* `infinite α` denotes that `α` is an infinite type.
 
 ## Implementation notes
 
@@ -66,11 +68,27 @@ lemma equiv.finite_iff (f : α ≃ β) : finite α ↔ finite β :=
 lemma function.bijective.finite_iff {f : α → β} (h : bijective f) : finite α ↔ finite β :=
 (equiv.of_bijective f h).finite_iff
 
-namespace finite
+lemma finite.of_bijective [finite α] {f : α → β} (h : bijective f) : finite β := h.finite_iff.mp ‹_›
 
-lemma of_bijective [finite α] {f : α → β} (h : bijective f) : finite β := h.finite_iff.mp ‹_›
+instance [finite α] : finite (plift α) := finite.of_equiv α equiv.plift.symm
+instance {α : Type v} [finite α] : finite (ulift.{u} α) := finite.of_equiv α equiv.ulift.symm
 
-instance [finite α] : finite (plift α) := of_equiv α equiv.plift.symm
-instance {α : Type v} [finite α] : finite (ulift.{u} α) := of_equiv α equiv.ulift.symm
+/-- A type is said to be infinite if it is not finite. Note that `infinite α` is equivalent to
+`is_empty (fintype α)` or `is_empty (finite α)`. -/
+class infinite (α : Sort*) : Prop :=
+(not_finite : ¬finite α)
 
-end finite
+@[simp] lemma not_finite_iff_infinite : ¬finite α ↔ infinite α := ⟨infinite.mk, λ h, h.1⟩
+
+@[simp] lemma not_infinite_iff_finite : ¬infinite α ↔ finite α :=
+not_finite_iff_infinite.not_right.symm
+
+lemma finite_or_infinite (α : Sort*) : finite α ∨ infinite α :=
+or_iff_not_imp_left.2 $ not_finite_iff_infinite.1
+
+lemma not_finite (α : Sort*) [infinite α] [finite α] : false := @infinite.not_finite α ‹_› ‹_›
+
+protected lemma finite.false [infinite α] (h : finite α) : false := not_finite α
+protected lemma infinite.false [finite α] (h : infinite α) : false := not_finite α
+
+alias not_infinite_iff_finite ↔ finite.of_not_infinite finite.not_infinite

src/data/fintype/basic.lean

@@ -1918,34 +1918,15 @@ well_founded_of_trans_of_irrefl _
 
 end finite
 
-/-- A type is said to be infinite if it has no fintype instance.
-  Note that `infinite α` is equivalent to `is_empty (fintype α)`. -/
-class infinite (α : Type*) : Prop :=
-(not_fintype : fintype α → false)
-
-lemma not_finite (α : Type*) [infinite α] [finite α] : false :=
-by { casesI nonempty_fintype α, exact infinite.not_fintype ‹_› }
-
-protected lemma finite.false [infinite α] (h : finite α) : false := not_finite α
-
 @[nolint fintype_finite]
 protected lemma fintype.false [infinite α] (h : fintype α) : false := not_finite α
-protected lemma infinite.false [finite α] (h : infinite α) : false := not_finite α
 
 @[simp] lemma is_empty_fintype {α : Type*} : is_empty (fintype α) ↔ infinite α :=
-⟨λ ⟨x⟩, ⟨x⟩, λ ⟨x⟩, ⟨x⟩⟩
-
-lemma not_finite_iff_infinite : ¬ finite α ↔ infinite α :=
-by rw [← is_empty_fintype, finite_iff_nonempty_fintype, not_nonempty_iff]
-
-lemma not_infinite_iff_finite : ¬ infinite α ↔ finite α := not_finite_iff_infinite.not_right.symm
-
-alias not_finite_iff_infinite ↔ infinite.of_not_finite infinite.not_finite
-alias not_infinite_iff_finite ↔ finite.of_not_infinite finite.not_infinite
+⟨λ ⟨h⟩, ⟨λ h', (@nonempty_fintype α h').elim h⟩, λ ⟨h⟩, ⟨λ h', h h'.finite⟩⟩
 
 /-- A non-infinite type is a fintype. -/
 noncomputable def fintype_of_not_infinite {α : Type*} (h : ¬ infinite α) : fintype α :=
-nonempty.some $ by rwa [← not_is_empty_iff, is_empty_fintype]
+@fintype.of_finite _ (not_infinite_iff_finite.mp h)
 
 section
 open_locale classical
@@ -1975,6 +1956,8 @@ lemma finset.exists_maximal {α : Type*} [preorder α] (s : finset α) (h : s.no
 
 namespace infinite
 
+lemma of_not_fintype (h : fintype α → false) : infinite α := is_empty_fintype.mp ⟨h⟩
+
 lemma exists_not_mem_finset [infinite α] (s : finset α) : ∃ x, x ∉ s :=
 not_forall.1 $ λ h, fintype.false ⟨s, h⟩
 
@@ -1988,15 +1971,15 @@ protected lemma nonempty (α : Type*) [infinite α] : nonempty α :=
 by apply_instance
 
 lemma of_injective [infinite β] (f : β → α) (hf : injective f) : infinite α :=
-⟨λ I, by exactI (fintype.of_injective f hf).false⟩
+⟨λ I, by exactI (finite.of_injective f hf).false⟩
 
 lemma of_surjective [infinite β] (f : α → β) (hf : surjective f) : infinite α :=
-⟨λ I, by { classical, exactI (fintype.of_surjective f hf).false }⟩
+⟨λ I, by exactI (finite.of_surjective f hf).false⟩
 
 end infinite
 
 instance : infinite ℕ :=
-⟨λ ⟨s, hs⟩, finset.not_mem_range_self $ s.subset_range_sup_succ (hs _)⟩
+infinite.of_not_fintype $ λ ⟨s, hs⟩, finset.not_mem_range_self $ s.subset_range_sup_succ (hs _)
 
 instance : infinite ℤ :=
 infinite.of_injective int.of_nat (λ _ _, int.of_nat.inj)

src/data/fintype/card_embedding.lean

@@ -43,8 +43,9 @@ end
 
 /- The cardinality of embeddings from an infinite type to a finite type is zero.
 This is a re-statement of the pigeonhole principle. -/
-@[simp] lemma card_embedding_eq_of_infinite {α β} [infinite α] [fintype β] [fintype (α ↪ β)] :
+@[simp] lemma card_embedding_eq_of_infinite {α β : Type*} [infinite α] [fintype β]
+  [fintype (α ↪ β)] :
   ‖α ↪ β‖ = 0 :=
-card_eq_zero_iff.mpr function.embedding.is_empty
+card_eq_zero
 
 end fintype

src/data/set/finite.lean

@@ -853,10 +853,9 @@ theorem infinite_univ [h : infinite α] : (@univ α).infinite :=
 infinite_univ_iff.2 h
 
 theorem infinite_coe_iff {s : set α} : infinite s ↔ s.infinite :=
-⟨λ ⟨h₁⟩ h₂, h₁ h₂.fintype, λ h₁, ⟨λ h₂, h₁ ⟨h₂⟩⟩⟩
+not_finite_iff_infinite.symm.trans finite_coe_iff.not
 
-theorem infinite.to_subtype {s : set α} (h : s.infinite) : infinite s :=
-infinite_coe_iff.2 h
+alias infinite_coe_iff ↔ _ infinite.to_subtype
 
 /-- Embedding of `ℕ` into an infinite set. -/
 noncomputable def infinite.nat_embedding (s : set α) (h : s.infinite) : ℕ ↪ s :=

src/field_theory/is_alg_closed/basic.lean

@@ -348,7 +348,7 @@ perfect_ring.of_surjective k p $ λ x, is_alg_closed.exists_pow_nat_eq _ $ ne_ze
 @[priority 500]
 instance {K : Type*} [field K] [is_alg_closed K] : infinite K :=
 begin
-  apply infinite.mk,
+  apply infinite.of_not_fintype,
   introsI hfin,
   set n := fintype.card K with hn,
   set f := (X : K[X]) ^ (n + 1) - 1 with hf,