refactor(data/set/finite): protect set.finite (#14344)

This change will make it so that it does not conflict with a top-level `finite` that will be added to complement `infinite`.

roadmap/topology/shrinking_lemma.lean

@@ -34,7 +34,7 @@ cover so that the closure of each new open set is contained in the corresponding
 set. -/
 lemma roadmap.shrinking_lemma {X : Type u} [topological_space X] [normal_space X]
   {s : set X} (hs : is_closed s) {α : Type v} (u : α → set X) (uo : ∀ a, is_open (u a))
-  (uf : ∀ x, finite {a | x ∈ u a}) (su : s ⊆ Union u) :
+  (uf : ∀ x, {a | x ∈ u a}.finite) (su : s ⊆ Union u) :
   ∃ v : α → set X, s ⊆ Union v ∧ ∀ a, is_open (v a) ∧ closure (v a) ⊆ u a :=
 todo
 /-

src/algebra/big_operators/finprod.lean

@@ -87,13 +87,13 @@ open_locale classical
 /-- Sum of `f x` as `x` ranges over the elements of the support of `f`, if it's finite. Zero
 otherwise. -/
 @[irreducible] noncomputable def finsum {M α} [add_comm_monoid M] (f : α → M) : M :=
-if h : finite (support (f ∘ plift.down)) then ∑ i in h.to_finset, f i.down else 0
+if h : (support (f ∘ plift.down)).finite then ∑ i in h.to_finset, f i.down else 0
 
 /-- Product of `f x` as `x` ranges over the elements of the multiplicative support of `f`, if it's
 finite. One otherwise. -/
 @[irreducible, to_additive]
 noncomputable def finprod (f : α → M) : M :=
-if h : finite (mul_support (f ∘ plift.down)) then ∏ i in h.to_finset, f i.down else 1
+if h : (mul_support (f ∘ plift.down)).finite then ∏ i in h.to_finset, f i.down else 1
 
 end
 
@@ -102,7 +102,7 @@ localized "notation `∑ᶠ` binders `, ` r:(scoped:67 f, finsum f) := r" in big
 localized "notation `∏ᶠ` binders `, ` r:(scoped:67 f, finprod f) := r" in big_operators
 
 @[to_additive] lemma finprod_eq_prod_plift_of_mul_support_to_finset_subset
-  {f : α → M} (hf : finite (mul_support (f ∘ plift.down))) {s : finset (plift α)}
+  {f : α → M} (hf : (mul_support (f ∘ plift.down)).finite) {s : finset (plift α)}
   (hs : hf.to_finset ⊆ s) :
   ∏ᶠ i, f i = ∏ i in s, f i.down :=
 begin
@@ -191,7 +191,7 @@ lemma one_le_finprod' {M : Type*} [ordered_comm_monoid M] {f : α → M} (hf : 
 finprod_induction _ le_rfl (λ _ _, one_le_mul) hf
 
 @[to_additive] lemma monoid_hom.map_finprod_plift (f : M →* N) (g : α → M)
-  (h : finite (mul_support $ g ∘ plift.down)) :
+  (h : (mul_support $ g ∘ plift.down).finite) :
   f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) :=
 begin
   rw [finprod_eq_prod_plift_of_mul_support_subset h.coe_to_finset.ge,
@@ -277,7 +277,7 @@ begin
 end
 
 @[to_additive] lemma finprod_eq_prod_of_mul_support_to_finset_subset (f : α → M)
-  (hf : finite (mul_support f)) {s : finset α} (h : hf.to_finset ⊆ s) :
+  (hf : (mul_support f).finite) {s : finset α} (h : hf.to_finset ⊆ s) :
   ∏ᶠ i, f i = ∏ i in s, f i :=
 finprod_eq_prod_of_mul_support_subset _ $ λ x hx, h $ hf.mem_to_finset.2 hx
 
@@ -326,7 +326,7 @@ begin
 end
 
 @[to_additive] lemma finprod_cond_ne (f : α → M) (a : α) [decidable_eq α]
-  (hf : finite (mul_support f)) : (∏ᶠ i ≠ a, f i) = ∏ i in hf.to_finset.erase a, f i :=
+  (hf : (mul_support f).finite) : (∏ᶠ i ≠ a, f i) = ∏ i in hf.to_finset.erase a, f i :=
 begin
   apply finprod_cond_eq_prod_of_cond_iff,
   intros x hx,
@@ -670,7 +670,7 @@ lemma finprod_mem_image' {s : set β} {g : β → α} (hg : (s ∩ mul_support (
   ∏ᶠ i ∈ g '' s, f i = ∏ᶠ j ∈ s, f (g j) :=
 begin
   classical,
-  by_cases hs : finite (s ∩ mul_support (f ∘ g)),
+  by_cases hs : (s ∩ mul_support (f ∘ g)).finite,
   { have hg : ∀ (x ∈ hs.to_finset) (y ∈ hs.to_finset), g x = g y → x = y,
       by simpa only [hs.mem_to_finset],
     rw [finprod_mem_eq_prod _ hs, ← finset.prod_image hg],
@@ -814,7 +814,7 @@ lemma finprod_mem_sUnion {t : set (set α)} (h : t.pairwise_disjoint id) (ht₀
   ∏ᶠ a ∈ ⋃₀ t, f a = ∏ᶠ s ∈ t, ∏ᶠ a ∈ s, f a :=
 by { rw set.sUnion_eq_bUnion, exact finprod_mem_bUnion h ht₀ ht₁ }
 
-@[to_additive] lemma mul_finprod_cond_ne (a : α) (hf : finite (mul_support f)) :
+@[to_additive] lemma mul_finprod_cond_ne (a : α) (hf : (mul_support f).finite) :
   f a * (∏ᶠ i ≠ a, f i) = ∏ᶠ i, f i :=
 begin
   classical,
@@ -858,7 +858,7 @@ finprod_nonneg $ λ x, finprod_nonneg $ hf x
 
 @[to_additive]
 lemma single_le_finprod {M : Type*} [ordered_comm_monoid M] (i : α) {f : α → M}
-  (hf : finite (mul_support f)) (h : ∀ j, 1 ≤ f j) :
+  (hf : (mul_support f).finite) (h : ∀ j, 1 ≤ f j) :
   f i ≤ ∏ᶠ j, f j :=
 by classical;
 calc f i ≤ ∏ j in insert i hf.to_finset, f j :
@@ -867,7 +867,7 @@ calc f i ≤ ∏ j in insert i hf.to_finset, f j :
   (finprod_eq_prod_of_mul_support_to_finset_subset _ hf (finset.subset_insert _ _)).symm
 
 lemma finprod_eq_zero {M₀ : Type*} [comm_monoid_with_zero M₀] (f : α → M₀) (x : α)
-  (hx : f x = 0) (hf : finite (mul_support f)) :
+  (hx : f x = 0) (hf : (mul_support f).finite) :
   ∏ᶠ x, f x = 0 :=
 begin
   nontriviality,

src/algebra/star/pointwise.lean

@@ -91,7 +91,7 @@ equiv.star.surjective.preimage_subset_preimage_iff
 lemma star_subset [has_involutive_star α] {s t : set α} : s⋆ ⊆ t ↔ s ⊆ t⋆ :=
 by { rw [← star_subset_star, star_star] }
 
-lemma finite.star [has_involutive_star α] {s : set α} (hs : finite s) : finite s⋆ :=
+lemma finite.star [has_involutive_star α] {s : set α} (hs : s.finite) : s⋆.finite :=
 hs.preimage $ star_injective.inj_on _
 
 lemma star_singleton {β : Type*} [has_involutive_star β] (x : β) : ({x} : set β)⋆ = {x⋆} :=

src/analysis/convex/combination.lean

@@ -302,7 +302,7 @@ begin
       (hw₁.symm ▸ zero_lt_one) (λ x hx, hx) }
 end
 
-lemma set.finite.convex_hull_eq {s : set E} (hs : finite s) :
+lemma set.finite.convex_hull_eq {s : set E} (hs : s.finite) :
   convex_hull R s = {x : E | ∃ (w : E → R) (hw₀ : ∀ y ∈ s, 0 ≤ w y)
     (hw₁ : ∑ y in hs.to_finset, w y = 1), hs.to_finset.center_mass w id = x} :=
 by simpa only [set.finite.coe_to_finset, set.finite.mem_to_finset, exists_prop]
@@ -402,7 +402,7 @@ under the linear map sending each function `w` to `∑ x in s, w x • x`.
 Since we have no sums over finite sets, we use sum over `@finset.univ _ hs.fintype`.
 The map is defined in terms of operations on `(s → ℝ) →ₗ[ℝ] ℝ` so that later we will not need
 to prove that this map is linear. -/
-lemma set.finite.convex_hull_eq_image {s : set E} (hs : finite s) :
+lemma set.finite.convex_hull_eq_image {s : set E} (hs : s.finite) :
   convex_hull R s = by haveI := hs.fintype; exact
     (⇑(∑ x : s, (@linear_map.proj R s _ (λ i, R) _ _ x).smul_right x.1)) '' (std_simplex R s) :=
 begin

src/analysis/convex/topology.lean

@@ -213,7 +213,7 @@ variables [add_comm_group E] [module ℝ E] [topological_space E]
   [topological_add_group E] [has_continuous_smul ℝ E]
 
 /-- Convex hull of a finite set is compact. -/
-lemma set.finite.compact_convex_hull {s : set E} (hs : finite s) :
+lemma set.finite.compact_convex_hull {s : set E} (hs : s.finite) :
   is_compact (convex_hull ℝ s) :=
 begin
   rw [hs.convex_hull_eq_image],
@@ -223,7 +223,7 @@ begin
 end
 
 /-- Convex hull of a finite set is closed. -/
-lemma set.finite.is_closed_convex_hull [t2_space E] {s : set E} (hs : finite s) :
+lemma set.finite.is_closed_convex_hull [t2_space E] {s : set E} (hs : s.finite) :
   is_closed (convex_hull ℝ s) :=
 hs.compact_convex_hull.is_closed
 

src/data/polynomial/ring_division.lean

@@ -622,7 +622,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 :=
-⟨polynomial.root_set_fintype p S⟩
+set.finite_of_fintype _
 
 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) :

src/data/set/countable.lean

@@ -184,7 +184,7 @@ by simp only [insert_eq, countable_union, countable_singleton, true_and]
 lemma countable.insert {s : set α} (a : α) (h : countable s) : countable (insert a s) :=
 countable_insert.2 h
 
-lemma finite.countable {s : set α} : finite s → countable s
+lemma finite.countable {s : set α} : s.finite → countable s
 | ⟨h⟩ := trunc.nonempty (by exactI fintype.trunc_encodable s)
 
 lemma subsingleton.countable {s : set α} (hs : s.subsingleton) : countable s :=
@@ -198,7 +198,7 @@ lemma countable_is_bot (α : Type*) [partial_order α] : countable {x : α | is_
 
 /-- The set of finite subsets of a countable set is countable. -/
 lemma countable_set_of_finite_subset {s : set α} : countable s →
-  countable {t | finite t ∧ t ⊆ s} | ⟨h⟩ :=
+  countable {t | set.finite t ∧ t ⊆ s} | ⟨h⟩ :=
 begin
   resetI,
   refine countable.mono _ (countable_range