refactor(data/finite/card): split from basic (#14885)

Author: urkud

src/data/finite/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
-import set_theory.cardinal.finite
+import data.fintype.basic
 
 /-!
 # Finite types
@@ -28,14 +28,6 @@ vice versa. Every `fintype` instance should be computable since they are meant
 for computation. If it's not possible to write a computable `fintype` instance,
 one should prefer writing a `finite` instance instead.
 
-The cardinality of a finite type `α` is given by `nat.card α`. This function has
-the "junk value" of `0` for infinite types, but to ensure the function has valid
-output, one just needs to know that it's possible to produce a `finite` instance
-for the type. (Note: we could have defined a `finite.card` that required you to
-supply a `finite` instance, but (a) the function would be `noncomputable` anyway
-so there is no need to supply the instance and (b) the function would have a more
-complicated dependent type that easily leads to "motive not type correct" errors.)
-
 ## Main definitions
 
 * `finite α` denotes that `α` is a finite type.
@@ -59,10 +51,6 @@ that cannot be inferred using `finite.of_fintype'`. (However, when using
 on `decidable` instances will give `finite` instances.) In the future we might
 consider writing automation to create these "lowered" instances.
 
-Theorems about `nat.card` are sometimes incidentally true for both finite and infinite
-types. If removing a finiteness constraint results in no loss in legibility, we remove
-it. We generally put such theorems into the `set_theory.cardinal.finite` module.
-
 ## Tags
 
 finiteness, finite types
@@ -99,21 +87,10 @@ priority than ones coming from `fintype` instances. -/
 @[priority 900]
 instance finite.of_fintype' (α : Type*) [fintype α] : finite α := finite.of_fintype ‹_›
 
-/-- There is (noncomputably) an equivalence between a finite type `α` and `fin (nat.card α)`. -/
-def finite.equiv_fin (α : Type*) [finite α] : α ≃ fin (nat.card α) :=
-begin
-  have := (finite.exists_equiv_fin α).some_spec.some,
-  rwa nat.card_eq_of_equiv_fin this,
-end
-
-/-- Similar to `finite.equiv_fin` but with control over the term used for the cardinality. -/
-def finite.equiv_fin_of_card_eq [finite α] {n : ℕ} (h : nat.card α = n) : α ≃ fin n :=
-by { subst h, apply finite.equiv_fin }
-
 /-- Noncomputably get a `fintype` instance from a `finite` instance. This is not an
 instance because we want `fintype` instances to be useful for computations. -/
 def fintype.of_finite (α : Type*) [finite α] : fintype α :=
-fintype.of_equiv _ (finite.equiv_fin α).symm
+nonempty.some $ let ⟨n, ⟨e⟩⟩ := finite.exists_equiv_fin α in ⟨fintype.of_equiv _ e.symm⟩
 
 lemma finite_iff_nonempty_fintype (α : Type*) :
   finite α ↔ nonempty (fintype α) :=
@@ -142,23 +119,6 @@ lemma not_infinite_iff_finite {α : Type*} : ¬ infinite α ↔ finite α :=
 lemma not_finite_iff_infinite {α : Type*} : ¬ finite α ↔ infinite α :=
 not_infinite_iff_finite.not_right.symm
 
-lemma nat.card_eq (α : Type*) :
-  nat.card α = if h : finite α then by exactI @fintype.card α (fintype.of_finite α) else 0 :=
-begin
-  casesI finite_or_infinite α,
-  { letI := fintype.of_finite α,
-    simp only [*, nat.card_eq_fintype_card, dif_pos] },
-  { simp [*, not_finite_iff_infinite.mpr h] },
-end
-
-lemma finite.card_pos_iff [finite α] :
-  0 < nat.card α ↔ nonempty α :=
-begin
-  haveI := fintype.of_finite α,
-  simp only [nat.card_eq_fintype_card],
-  exact fintype.card_pos_iff,
-end
-
 lemma of_subsingleton {α : Sort*} [subsingleton α] : finite α := finite.of_equiv _ equiv.plift
 
 @[nolint instance_priority]
@@ -190,24 +150,9 @@ end
 lemma of_surjective {α β : Sort*} [finite α] (f : α → β) (H : function.surjective f) : finite β :=
 of_injective _ $ function.injective_surj_inv H
 
-lemma card_eq [finite α] [finite β] : nat.card α = nat.card β ↔ nonempty (α ≃ β) :=
-by { haveI := fintype.of_finite α, haveI := fintype.of_finite β, simp [fintype.card_eq] }
-
 @[priority 100] -- see Note [lower instance priority]
 instance of_is_empty {α : Sort*} [is_empty α] : finite α := finite.of_equiv _ equiv.plift
 
-lemma card_le_one_iff_subsingleton [finite α] : nat.card α ≤ 1 ↔ subsingleton α :=
-by { haveI := fintype.of_finite α, simp [fintype.card_le_one_iff_subsingleton] }
-
-lemma one_lt_card_iff_nontrivial [finite α] : 1 < nat.card α ↔ nontrivial α :=
-by { haveI := fintype.of_finite α, simp [fintype.one_lt_card_iff_nontrivial] }
-
-lemma one_lt_card [finite α] [h : nontrivial α] : 1 < nat.card α :=
-one_lt_card_iff_nontrivial.mpr h
-
-@[simp] lemma card_option [finite α] : nat.card (option α) = nat.card α + 1 :=
-by { haveI := fintype.of_finite α, simp }
-
 lemma prod_left (β) [finite (α × β)] [nonempty β] : finite α :=
 of_surjective (prod.fst : α × β → α) prod.fst_surjective
 
@@ -226,39 +171,12 @@ of_injective (sum.inl : α → α ⊕ β) sum.inl_injective
 lemma sum_right (α) [finite (α ⊕ β)] : finite β :=
 of_injective (sum.inr : β → α ⊕ β) sum.inr_injective
 
-lemma card_sum [finite α] [finite β] : nat.card (α ⊕ β) = nat.card α + nat.card β :=
-by { haveI := fintype.of_finite α, haveI := fintype.of_finite β, simp }
-
-lemma card_le_of_injective [finite β] (f : α → β) (hf : function.injective f) :
-  nat.card α ≤ nat.card β :=
-by { haveI := fintype.of_finite β, haveI := fintype.of_injective f hf,
-     simpa using fintype.card_le_of_injective f hf }
-
-lemma card_le_of_embedding [finite β] (f : α ↪ β) : nat.card α ≤ nat.card β :=
-card_le_of_injective _ f.injective
-
-lemma card_le_of_surjective [finite α] (f : α → β) (hf : function.surjective f) :
-  nat.card β ≤ nat.card α :=
-by { haveI := fintype.of_finite α, haveI := fintype.of_surjective f hf,
-     simpa using fintype.card_le_of_surjective f hf }
-
-lemma card_eq_zero_iff [finite α] : nat.card α = 0 ↔ is_empty α :=
-by { haveI := fintype.of_finite α, simp [fintype.card_eq_zero_iff] }
-
 end finite
 
 /-- This instance also provides `[finite s]` for `s : set α`. -/
 instance subtype.finite {α : Sort*} [finite α] {p : α → Prop} : finite {x // p x} :=
 finite.of_injective coe subtype.coe_injective
 
-theorem finite.card_subtype_le [finite α] (p : α → Prop) :
-  nat.card {x // p x} ≤ nat.card α :=
-by { haveI := fintype.of_finite α, simpa using fintype.card_subtype_le p }
-
-theorem finite.card_subtype_lt [finite α] {p : α → Prop} {x : α} (hx : ¬ p x) :
-  nat.card {x // p x} < nat.card α :=
-by { haveI := fintype.of_finite α, simpa using fintype.card_subtype_lt hx }
-
 instance pi.finite {α : Sort*} {β : α → Sort*} [finite α] [∀ a, finite (β a)] : finite (Π a, β a) :=
 begin
   haveI := fintype.of_finite (plift α),

src/data/finite/card.lean

@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2022 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import data.finite.basic
+import set_theory.cardinal.finite
+
+/-!
+
+# Cardinality of finite types
+
+The cardinality of a finite type `α` is given by `nat.card α`. This function has
+the "junk value" of `0` for infinite types, but to ensure the function has valid
+output, one just needs to know that it's possible to produce a `finite` instance
+for the type. (Note: we could have defined a `finite.card` that required you to
+supply a `finite` instance, but (a) the function would be `noncomputable` anyway
+so there is no need to supply the instance and (b) the function would have a more
+complicated dependent type that easily leads to "motive not type correct" errors.)
+
+## Implementation notes
+
+Theorems about `nat.card` are sometimes incidentally true for both finite and infinite
+types. If removing a finiteness constraint results in no loss in legibility, we remove
+it. We generally put such theorems into the `set_theory.cardinal.finite` module.
+
+-/
+
+noncomputable theory
+open_locale classical
+
+variables {α β γ : Type*}
+
+/-- There is (noncomputably) an equivalence between a finite type `α` and `fin (nat.card α)`. -/
+def finite.equiv_fin (α : Type*) [finite α] : α ≃ fin (nat.card α) :=
+begin
+  have := (finite.exists_equiv_fin α).some_spec.some,
+  rwa nat.card_eq_of_equiv_fin this,
+end
+
+/-- Similar to `finite.equiv_fin` but with control over the term used for the cardinality. -/
+def finite.equiv_fin_of_card_eq [finite α] {n : ℕ} (h : nat.card α = n) : α ≃ fin n :=
+by { subst h, apply finite.equiv_fin }
+
+lemma nat.card_eq (α : Type*) :
+  nat.card α = if h : finite α then by exactI @fintype.card α (fintype.of_finite α) else 0 :=
+begin
+  casesI finite_or_infinite α,
+  { letI := fintype.of_finite α,
+    simp only [*, nat.card_eq_fintype_card, dif_pos] },
+  { simp [*, not_finite_iff_infinite.mpr h] },
+end
+
+lemma finite.card_pos_iff [finite α] :
+  0 < nat.card α ↔ nonempty α :=
+begin
+  haveI := fintype.of_finite α,
+  simp only [nat.card_eq_fintype_card],
+  exact fintype.card_pos_iff,
+end
+
+namespace finite
+
+lemma card_eq [finite α] [finite β] : nat.card α = nat.card β ↔ nonempty (α ≃ β) :=
+by { haveI := fintype.of_finite α, haveI := fintype.of_finite β, simp [fintype.card_eq] }
+
+lemma card_le_one_iff_subsingleton [finite α] : nat.card α ≤ 1 ↔ subsingleton α :=
+by { haveI := fintype.of_finite α, simp [fintype.card_le_one_iff_subsingleton] }
+
+lemma one_lt_card_iff_nontrivial [finite α] : 1 < nat.card α ↔ nontrivial α :=
+by { haveI := fintype.of_finite α, simp [fintype.one_lt_card_iff_nontrivial] }
+
+lemma one_lt_card [finite α] [h : nontrivial α] : 1 < nat.card α :=
+one_lt_card_iff_nontrivial.mpr h
+
+@[simp] lemma card_option [finite α] : nat.card (option α) = nat.card α + 1 :=
+by { haveI := fintype.of_finite α, simp }
+
+lemma card_le_of_injective [finite β] (f : α → β) (hf : function.injective f) :
+  nat.card α ≤ nat.card β :=
+by { haveI := fintype.of_finite β, haveI := fintype.of_injective f hf,
+     simpa using fintype.card_le_of_injective f hf }
+
+lemma card_le_of_embedding [finite β] (f : α ↪ β) : nat.card α ≤ nat.card β :=
+card_le_of_injective _ f.injective
+
+lemma card_le_of_surjective [finite α] (f : α → β) (hf : function.surjective f) :
+  nat.card β ≤ nat.card α :=
+by { haveI := fintype.of_finite α, haveI := fintype.of_surjective f hf,
+     simpa using fintype.card_le_of_surjective f hf }
+
+lemma card_eq_zero_iff [finite α] : nat.card α = 0 ↔ is_empty α :=
+by { haveI := fintype.of_finite α, simp [fintype.card_eq_zero_iff] }
+
+lemma card_sum [finite α] [finite β] : nat.card (α ⊕ β) = nat.card α + nat.card β :=
+by { haveI := fintype.of_finite α, haveI := fintype.of_finite β, simp }
+
+end finite
+
+theorem finite.card_subtype_le [finite α] (p : α → Prop) :
+  nat.card {x // p x} ≤ nat.card α :=
+by { haveI := fintype.of_finite α, simpa using fintype.card_subtype_le p }
+
+theorem finite.card_subtype_lt [finite α] {p : α → Prop} {x : α} (hx : ¬ p x) :
+  nat.card {x // p x} < nat.card α :=
+by { haveI := fintype.of_finite α, simpa using fintype.card_subtype_lt hx }