refactor(data/finite/set,data/set/finite): move most contents of one file to another (#15166)

* move most content of `data.finite.set` to `data.set.finite`;
* use `casesI nonempty_fintype _` instead of `letI := fintype.of_finite`; sometimes it lets us avoid `classical.choice`;
* merge `set.finite.of_fintype`, `set.finite_of_fintype`, and `set.finite_of_finite` into `set.to_finite`;
* rewrite `set.finite_univ_iff` and `finite.of_finite_univ` in terms of `set.finite`;
* replace some assumptions `[fintype (plift _)]` with `[finite _]`;
* generalize `set.cod_restrict` and some lemmas to allow domain in `Sort*`, use it for `finite.of_injective_finite.range`.

Author: urkud

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

@@ -301,7 +301,7 @@ end
 lemma exists_mi : ∃(i : ι), i ∈ bcubes cs c ∧ ∀(i' ∈ bcubes cs c),
   (cs i).w ≤ (cs i').w :=
 by simpa
-  using (bcubes cs c).exists_min_image (λ i, (cs i).w) (finite.of_fintype _) (nonempty_bcubes h v)
+  using (bcubes cs c).exists_min_image (λ i, (cs i).w) (set.to_finite _) (nonempty_bcubes h v)
 
 /-- We let `mi` be the (index for the) smallest cube in the valley `c` -/
 def mi : ι := classical.some $ exists_mi h v
@@ -350,7 +350,7 @@ begin
   have hs : s.nonempty,
   { rcases (two_le_iff' (⟨i, hi⟩ : bcubes cs c)).mp (two_le_mk_bcubes h v) with ⟨⟨i', hi'⟩, h2i'⟩,
     refine ⟨i', hi', _⟩, simp only [mem_singleton_iff], intro h, apply h2i', simp [h] },
-  rcases set.exists_min_image s (w ∘ cs) (finite.of_fintype _) hs with ⟨i', ⟨hi', h2i'⟩, h3i'⟩,
+  rcases set.exists_min_image s (w ∘ cs) (set.to_finite _) hs with ⟨i', ⟨hi', h2i'⟩, h3i'⟩,
   rw [mem_singleton_iff] at h2i',
   let x := c.b j.succ + c.w - (cs i').w,
   have hx : x < (cs i).b j.succ,

src/algebra/big_operators/finprod.lean

@@ -202,7 +202,7 @@ end
 
 @[to_additive] lemma monoid_hom.map_finprod_Prop {p : Prop} (f : M →* N) (g : p → M) :
   f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) :=
-f.map_finprod_plift g (finite.of_fintype _)
+f.map_finprod_plift g (set.to_finite _)
 
 @[to_additive] lemma monoid_hom.map_finprod_of_preimage_one (f : M →* N)
   (hf : ∀ x, f x = 1 → x = 1) (g : α → M) :
@@ -310,7 +310,7 @@ by { classical, rw [finprod_def, dif_pos hf] }
 
 @[to_additive] lemma finprod_eq_prod_of_fintype [fintype α] (f : α → M) :
   ∏ᶠ i : α, f i = ∏ i, f i :=
-finprod_eq_prod_of_mul_support_to_finset_subset _ (finite.of_fintype _) $ finset.subset_univ _
+finprod_eq_prod_of_mul_support_to_finset_subset _ (set.to_finite _) $ finset.subset_univ _
 
 @[to_additive] lemma finprod_cond_eq_prod_of_cond_iff (f : α → M) {p : α → Prop} {t : finset α}
   (h : ∀ {x}, f x ≠ 1 → (p x ↔ x ∈ t)) :

src/analysis/box_integral/partition/measure.lean

@@ -55,7 +55,7 @@ end
 lemma measurable_set_Icc : measurable_set I.Icc := measurable_set_Icc
 
 lemma measurable_set_Ioo : measurable_set I.Ioo :=
-(measurable_set_pi (set.finite.of_fintype _).countable).2 $ or.inl $ λ i hi, measurable_set_Ioo
+(measurable_set_pi (set.to_finite _).countable).2 $ or.inl $ λ i hi, measurable_set_Ioo
 
 lemma coe_ae_eq_Icc : (I : set (ι → ℝ)) =ᵐ[volume] I.Icc :=
 by { rw coe_eq_pi, exact measure.univ_pi_Ioc_ae_eq_Icc }

src/data/finite/basic.lean

@@ -87,16 +87,18 @@ priority than ones coming from `fintype` instances. -/
 @[priority 900]
 instance finite.of_fintype' (α : Type*) [fintype α] : finite α := finite.of_fintype ‹_›
 
-/-- 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 α :=
-nonempty.some $ let ⟨n, ⟨e⟩⟩ := finite.exists_equiv_fin α in ⟨fintype.of_equiv _ e.symm⟩
-
 lemma finite_iff_nonempty_fintype (α : Type*) :
   finite α ↔ nonempty (fintype α) :=
 ⟨λ h, let ⟨k, ⟨e⟩⟩ := @finite.exists_equiv_fin α h in ⟨fintype.of_equiv _ e.symm⟩,
   λ ⟨_⟩, by exactI infer_instance⟩
 
+lemma nonempty_fintype (α : Type*) [finite α] : nonempty (fintype α) :=
+(finite_iff_nonempty_fintype α).mp ‹_›
+
+/-- 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 α := (nonempty_fintype α).some
+
 lemma not_finite_iff_infinite {α : Type*} : ¬ finite α ↔ infinite α :=
 by rw [← is_empty_fintype, finite_iff_nonempty_fintype, not_nonempty_iff]
 

src/data/finite/set.lean

@@ -7,162 +7,24 @@ import data.finite.basic
 import data.set.finite
 
 /-!
-# Finite instances for `set`
+# Lemmas about `finite` and `set`s
 
-This module provides ways to go between `set.finite` and `finite` and also provides a number
-of `finite` instances for basic set constructions such as unions, intersections, and so on.
-
-## Main definitions
-
-* `set.finite_of_finite` creates a `set.finite` proof from a `finite` instance
-* `set.finite.finite` creates a `finite` instance from a `set.finite` proof
-* `finite.set.subset` for finiteness of subsets of a finite set
+In this file we prove two lemmas about `finite` and `set`s.
 
 ## Tags
 
 finiteness, finite sets
-
 -/
 
 open set
-open_locale classical
 
 universes u v w x
-variables {α : Type u} {β : Type v} {ι : Sort w} {γ : Type x}
-
-/-- Constructor for `set.finite` using a `finite` instance. -/
-theorem set.finite_of_finite (s : set α) [finite s] : s.finite := ⟨fintype.of_finite s⟩
-
-/-- Projection of `set.finite` to its `finite` instance.
-This is intended to be used with dot notation.
-See also `set.finite.fintype`. -/
-@[nolint dup_namespace]
-protected lemma set.finite.finite {s : set α} (h : s.finite) : finite s :=
-finite.of_fintype h.fintype
-
-lemma set.finite_iff_finite {s : set α} : s.finite ↔ finite s :=
-⟨λ h, h.finite, λ h, by exactI set.finite_of_finite s⟩
-
-/-- Construct a `finite` instance for a `set` from a `finset` with the same elements. -/
-protected lemma finite.of_finset {p : set α} (s : finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : finite p :=
-finite.of_fintype (fintype.of_finset s H)
-
-/-! ### Finite instances
-
-There is seemingly some overlap between the following instances and the `fintype` instances
-in `data.set.finite`. While every `fintype` instance gives a `finite` instance, those
-instances that depend on `fintype` or `decidable` instances need an additional `finite` instance
-to be able to generally apply.
-
-Some set instances do not appear here since they are consequences of others, for example
-`subtype.finite` for subsets of a finite type.
--/
-
-namespace finite.set
-
-example {s : set α} [finite α] : finite s := infer_instance
-example : finite (∅ : set α) := infer_instance
-example (a : α) : finite ({a} : set α) := infer_instance
-
-instance finite_union (s t : set α) [finite s] [finite t] :
-  finite (s ∪ t : set α) :=
-by { haveI := fintype.of_finite s, haveI := fintype.of_finite t, apply_instance }
-
-instance finite_sep (s : set α) (p : α → Prop) [finite s] :
-  finite ({a ∈ s | p a} : set α) :=
-by { haveI := fintype.of_finite s, apply_instance }
-
-protected lemma subset (s : set α) {t : set α} [finite s] (h : t ⊆ s) : finite t :=
-by { rw eq_sep_of_subset h, apply_instance }
-
-instance finite_inter_of_right (s t : set α) [finite t] :
-  finite (s ∩ t : set α) := finite.set.subset t (inter_subset_right s t)
-
-instance finite_inter_of_left (s t : set α) [finite s] :
-  finite (s ∩ t : set α) := finite.set.subset s (inter_subset_left s t)
-
-instance finite_diff (s t : set α) [finite s] :
-  finite (s \ t : set α) := finite.set.subset s (diff_subset s t)
-
-instance finite_Union [finite ι] (f : ι → set α) [∀ i, finite (f i)] : finite (⋃ i, f i) :=
-begin
-  convert_to finite (⋃ (i : plift ι), f i.down),
-  { congr, ext, simp },
-  haveI := fintype.of_finite (plift ι),
-  haveI := λ i, fintype.of_finite (f i),
-  apply_instance,
-end
-
-instance finite_sUnion {s : set (set α)} [finite s] [H : ∀ (t : s), finite (t : set α)] :
-  finite (⋃₀ s) :=
-by { rw sUnion_eq_Union, exact @finite.set.finite_Union _ _ _ _ H }
-
-lemma finite_bUnion {ι : Type*} (s : set ι) [finite s] (t : ι → set α) (H : ∀ i ∈ s, finite (t i)) :
-  finite (⋃(x ∈ s), t x) :=
-begin
-  convert_to finite (⋃ (x : s), t x),
-  { congr' 1, ext, simp },
-  haveI : ∀ (i : s), finite (t i) := λ i, H i i.property,
-  apply_instance,
-end
-
-instance finite_bUnion' {ι : Type*} (s : set ι) [finite s] (t : ι → set α) [∀ i, finite (t i)] :
-  finite (⋃(x ∈ s), t x) :=
-finite_bUnion s t (λ i h, infer_instance)
-
-/--
-Example: `finite (⋃ (i < n), f i)` where `f : ℕ → set α` and `[∀ i, finite (f i)]`
-(when given instances from `data.nat.interval`).
--/
-instance finite_bUnion'' {ι : Type*} (p : ι → Prop) [h : finite {x | p x}]
-  (t : ι → set α) [∀ i, finite (t i)] :
-  finite (⋃ x (h : p x), t x) :=
-@finite.set.finite_bUnion' _ _ (set_of p) h t _
-
-instance finite_Inter {ι : Sort*} [nonempty ι] (t : ι → set α) [∀ i, finite (t i)] :
-  finite (⋂ i, t i) :=
-finite.set.subset (t $ classical.arbitrary ι) (Inter_subset _ _)
-
-instance finite_insert (a : α) (s : set α) [finite s] : finite (insert a s : set α) :=
-((set.finite_of_finite s).insert a).finite
-
-instance finite_image (s : set α) (f : α → β) [finite s] : finite (f '' s) :=
-((set.finite_of_finite s).image f).finite
-
-instance finite_range (f : ι → α) [finite ι] : finite (range f) :=
-by { haveI := fintype.of_finite (plift ι), apply_instance }
-
-instance finite_replacement [finite α] (f : α → β) : finite {(f x) | (x : α)} :=
-finite.set.finite_range f
-
-instance finite_prod (s : set α) (t : set β) [finite s] [finite t] :
-  finite (s ×ˢ t : set (α × β)) :=
-by { haveI := fintype.of_finite s, haveI := fintype.of_finite t, apply_instance }
-
-instance finite_image2 (f : α → β → γ) (s : set α) (t : set β) [finite s] [finite t] :
-  finite (image2 f s t : set γ) :=
-by { rw ← image_prod, apply_instance }
-
-instance finite_seq (f : set (α → β)) (s : set α) [finite f] [finite s] : finite (f.seq s) :=
-by { rw seq_def, apply_instance }
-
-end finite.set
-
-/-! ### Non-instances -/
-
-lemma set.finite_univ_iff : finite (set.univ : set α) ↔ finite α :=
-(equiv.set.univ α).finite_iff
-
-lemma finite.of_finite_univ [finite ↥(univ : set α)] : finite α :=
-set.finite_univ_iff.mp ‹_›
+variables {α : Type u} {β : Type v} {ι : Sort w}
 
 lemma finite.set.finite_of_finite_image (s : set α)
   {f : α → β} (h : s.inj_on f) [finite (f '' s)] : finite s :=
 finite.of_equiv _ (equiv.of_bijective _ h.bij_on_image.bijective).symm
 
-lemma finite.of_injective_finite_range {f : α → β}
-  (hf : function.injective f) [finite (range f)] : finite α :=
-begin
-  refine finite.of_injective (set.range_factorization f) (λ x y h, hf _),
-  simpa only [range_factorization_coe] using congr_arg (coe : range f → β) h,
-end
+lemma finite.of_injective_finite_range {f : ι → α}
+  (hf : function.injective f) [finite (range f)] : finite ι :=
+finite.of_injective (set.range_factorization f) (hf.cod_restrict _)

src/data/polynomial/ring_division.lean

@@ -655,7 +655,7 @@ finset_coe.fintype _
 
 lemma root_set_finite (p : T[X])
   (S : Type*) [comm_ring S] [is_domain S] [algebra T S] : (p.root_set S).finite :=
-set.finite_of_fintype _
+set.to_finite _
 
 theorem mem_root_set_iff' {p : T[X]} {S : Type*} [comm_ring S] [is_domain S]
   [algebra T S] (hp : p.map (algebra_map T S) ≠ 0) (a : S) :