lint(*/finsupp/*): use finite instead of fintype (#17553)

Also golf some proofs.

src/data/finsupp/defs.lean

@@ -174,24 +174,24 @@ lemma support_subset_iff {s : set α} {f : α →₀ M} :
 by simp only [set.subset_def, mem_coe, mem_support_iff];
    exact forall_congr (assume a, not_imp_comm)
 
-/-- Given `fintype α`, `equiv_fun_on_fintype` is the `equiv` between `α →₀ β` and `α → β`.
+/-- Given `finite α`, `equiv_fun_on_finite` is the `equiv` between `α →₀ β` and `α → β`.
   (All functions on a finite type are finitely supported.) -/
-@[simps] def equiv_fun_on_fintype [fintype α] : (α →₀ M) ≃ (α → M) :=
-⟨λf a, f a, λf, mk (finset.univ.filter $ λa, f a ≠ 0) f (by simp only [true_and, finset.mem_univ,
-  iff_self, finset.mem_filter, finset.filter_congr_decidable, forall_true_iff]),
-  begin intro f, ext a, refl end,
-  begin intro f, ext a, refl end⟩
+@[simps] def equiv_fun_on_finite [finite α] : (α →₀ M) ≃ (α → M) :=
+{ to_fun := coe_fn,
+  inv_fun := λ f, mk (function.support f).to_finite.to_finset f (λ a, set.finite.mem_to_finset _),
+  left_inv := λ f, ext $ λ x, rfl,
+  right_inv := λ f, rfl }
 
-@[simp] lemma equiv_fun_on_fintype_symm_coe {α} [fintype α] (f : α →₀ M) :
-  equiv_fun_on_fintype.symm f = f :=
-by { ext, simp [equiv_fun_on_fintype], }
+@[simp] lemma equiv_fun_on_finite_symm_coe {α} [finite α] (f : α →₀ M) :
+  equiv_fun_on_finite.symm f = f :=
+equiv_fun_on_finite.symm_apply_apply f
 
 /--
 If `α` has a unique term, the type of finitely supported functions `α →₀ β` is equivalent to `β`.
 -/
 @[simps] noncomputable
 def _root_.equiv.finsupp_unique {ι : Type*} [unique ι] : (ι →₀ M) ≃ M :=
-finsupp.equiv_fun_on_fintype.trans (equiv.fun_unique ι M)
+finsupp.equiv_fun_on_finite.trans (equiv.fun_unique ι M)
 
 end basic
 
@@ -380,13 +380,13 @@ lemma card_support_le_one' [nonempty α] {f : α →₀ M} :
   card f.support ≤ 1 ↔ ∃ a b, f = single a b :=
 by simp only [card_le_one_iff_subset_singleton, support_subset_singleton']
 
-@[simp] lemma equiv_fun_on_fintype_single [decidable_eq α] [fintype α] (x : α) (m : M) :
-  (@finsupp.equiv_fun_on_fintype α M _ _) (finsupp.single x m) = pi.single x m :=
-by { ext, simp [finsupp.single_eq_pi_single, finsupp.equiv_fun_on_fintype], }
+@[simp] lemma equiv_fun_on_finite_single [decidable_eq α] [finite α] (x : α) (m : M) :
+  finsupp.equiv_fun_on_finite (finsupp.single x m) = pi.single x m :=
+by { ext, simp [finsupp.single_eq_pi_single], }
 
-@[simp] lemma equiv_fun_on_fintype_symm_single [decidable_eq α] [fintype α] (x : α) (m : M) :
-  (@finsupp.equiv_fun_on_fintype α M _ _).symm (pi.single x m) = finsupp.single x m :=
-by { ext, simp [finsupp.single_eq_pi_single, finsupp.equiv_fun_on_fintype], }
+@[simp] lemma equiv_fun_on_finite_symm_single [decidable_eq α] [finite α] (x : α) (m : M) :
+  finsupp.equiv_fun_on_finite.symm (pi.single x m) = finsupp.single x m :=
+by rw [← equiv_fun_on_finite_single, equiv.symm_apply_apply]
 
 end single
 

src/data/finsupp/fin.lean

@@ -26,11 +26,11 @@ variables {n : ℕ} (i : fin n) {M : Type*} [has_zero M] (y : M)
 
 /-- `tail` for maps `fin (n + 1) →₀ M`. See `fin.tail` for more details. -/
 def tail (s : fin (n + 1) →₀ M) : fin n →₀ M :=
-finsupp.equiv_fun_on_fintype.symm (fin.tail s)
+finsupp.equiv_fun_on_finite.symm (fin.tail s)
 
 /-- `cons` for maps `fin n →₀ M`. See `fin.cons` for more details. -/
 def cons (y : M) (s : fin n →₀ M) : fin (n + 1) →₀ M :=
-finsupp.equiv_fun_on_fintype.symm (fin.cons y s : fin (n + 1) → M)
+finsupp.equiv_fun_on_finite.symm (fin.cons y s : fin (n + 1) → M)
 
 lemma tail_apply : tail t i = t i.succ := rfl
 

src/data/finsupp/fintype.lean

@@ -17,7 +17,7 @@ Some lemmas on the combination of `finsupp`, `fintype` and `infinite`.
 noncomputable instance finsupp.fintype {ι π : Sort*} [decidable_eq ι] [has_zero π]
   [fintype ι] [fintype π] :
   fintype (ι →₀ π) :=
-fintype.of_equiv _ finsupp.equiv_fun_on_fintype.symm
+fintype.of_equiv _ finsupp.equiv_fun_on_finite.symm
 
 instance finsupp.infinite_of_left {ι π : Sort*} [nontrivial π] [has_zero π] [infinite ι] :
   infinite (ι →₀ π) :=

src/data/finsupp/pwo.lean

@@ -6,7 +6,6 @@ Authors: Alex J. Best
 import data.finsupp.order
 import order.well_founded_set
 
-
 /-!
 # Partial well ordering on finsupps
 
@@ -24,14 +23,11 @@ It is in a separate file for now so as to not add imports to the file `order.wel
 Dickson, order, partial well order
 -/
 
-
 /-- A version of **Dickson's lemma** any subset of functions `σ →₀ α` is partially well
-ordered, when `σ` is a `fintype` and `α` is a linear well order.
-This version uses finsupps on a fintype as it is intended for use with `mv_power_series`.
+ordered, when `σ` is `finite` and `α` is a linear well order.
+This version uses finsupps on a finite type as it is intended for use with `mv_power_series`.
 -/
-lemma finsupp.is_pwo {α σ : Type*} [has_zero α] [linear_order α] [is_well_order α (<)] [fintype σ]
+lemma finsupp.is_pwo {α σ : Type*} [has_zero α] [linear_order α] [is_well_order α (<)] [finite σ]
   (S : set (σ →₀ α)) : S.is_pwo :=
-begin
-  rw ← finsupp.equiv_fun_on_fintype.symm.image_preimage S,
-  refine set.partially_well_ordered_on.image_of_monotone_on (pi.is_pwo _) (λ a b ha hb, id),
-end
+finsupp.equiv_fun_on_finite.symm_image_image S ▸
+  set.partially_well_ordered_on.image_of_monotone_on (pi.is_pwo _) (λ a b ha hb, id)

src/data/finsupp/well_founded.lean

@@ -57,8 +57,7 @@ variable (r)
 
 theorem lex.well_founded_of_finite [is_strict_total_order α r] [finite α] [has_zero N]
   (hs : well_founded s) : well_founded (finsupp.lex r s) :=
-have _ := fintype.of_finite α,
-  by exactI inv_image.wf (@equiv_fun_on_fintype α N _ _) (pi.lex.well_founded r $ λ a, hs)
+inv_image.wf (@equiv_fun_on_finite α N _ _) (pi.lex.well_founded r $ λ a, hs)
 
 theorem lex.well_founded_lt_of_finite [linear_order α] [finite α] [has_zero N] [has_lt N]
   [hwf : well_founded_lt N] : well_founded_lt (lex (α →₀ N)) :=
@@ -74,7 +73,6 @@ finsupp.well_founded_lt $ λ a, (zero_le a).not_lt
 
 instance well_founded_lt_of_finite [finite α] [has_zero N] [preorder N]
   [well_founded_lt N] : well_founded_lt (α →₀ N) :=
-have _ := fintype.of_finite α,
-  by exactI ⟨inv_image.wf equiv_fun_on_fintype function.well_founded_lt.wf⟩
+⟨inv_image.wf equiv_fun_on_finite function.well_founded_lt.wf⟩
 
 end finsupp

src/field_theory/finite/polynomial.lean

@@ -186,7 +186,7 @@ calc module.rank K (R σ K) =
     by rw [finsupp.dim_eq, dim_self, mul_one]
   ... = #{s : σ → ℕ | ∀ (n : σ), s n < fintype.card K } :
   begin
-    refine quotient.sound ⟨equiv.subtype_equiv finsupp.equiv_fun_on_fintype $ assume f, _⟩,
+    refine quotient.sound ⟨equiv.subtype_equiv finsupp.equiv_fun_on_finite $ assume f, _⟩,
     refine forall_congr (assume n, le_tsub_iff_right _),
     exact fintype.card_pos_iff.2 ⟨0⟩
   end

src/linear_algebra/basic.lean

@@ -84,36 +84,36 @@ begin
   { intro i, exact (h i).map_zero },
 end
 
-variables (α : Type*) [fintype α]
+variables (α : Type*) [finite α]
 variables (R M) [add_comm_monoid M] [semiring R] [module R M]
 
-/-- Given `fintype α`, `linear_equiv_fun_on_fintype R` is the natural `R`-linear equivalence between
+/-- Given `finite α`, `linear_equiv_fun_on_finite R` is the natural `R`-linear equivalence between
 `α →₀ β` and `α → β`. -/
-@[simps apply] noncomputable def linear_equiv_fun_on_fintype :
+@[simps apply] noncomputable def linear_equiv_fun_on_finite :
   (α →₀ M) ≃ₗ[R] (α → M) :=
 { to_fun := coe_fn,
-  map_add' := λ f g, by { ext, refl },
-  map_smul' := λ c f, by { ext, refl },
-  .. equiv_fun_on_fintype }
+  map_add' := λ f g, rfl,
+  map_smul' := λ c f, rfl,
+  .. equiv_fun_on_finite }
 
-@[simp] lemma linear_equiv_fun_on_fintype_single [decidable_eq α] (x : α) (m : M) :
-  (linear_equiv_fun_on_fintype R M α) (single x m) = pi.single x m :=
-equiv_fun_on_fintype_single x m
+@[simp] lemma linear_equiv_fun_on_finite_single [decidable_eq α] (x : α) (m : M) :
+  (linear_equiv_fun_on_finite R M α) (single x m) = pi.single x m :=
+equiv_fun_on_finite_single x m
 
-@[simp] lemma linear_equiv_fun_on_fintype_symm_single [decidable_eq α]
-  (x : α) (m : M) : (linear_equiv_fun_on_fintype R M α).symm (pi.single x m) = single x m :=
-equiv_fun_on_fintype_symm_single x m
+@[simp] lemma linear_equiv_fun_on_finite_symm_single [decidable_eq α]
+  (x : α) (m : M) : (linear_equiv_fun_on_finite R M α).symm (pi.single x m) = single x m :=
+equiv_fun_on_finite_symm_single x m
 
-@[simp] lemma linear_equiv_fun_on_fintype_symm_coe (f : α →₀ M) :
-  (linear_equiv_fun_on_fintype R M α).symm f = f :=
-by { ext, simp [linear_equiv_fun_on_fintype], }
+@[simp] lemma linear_equiv_fun_on_finite_symm_coe (f : α →₀ M) :
+  (linear_equiv_fun_on_finite R M α).symm f = f :=
+(linear_equiv_fun_on_finite R M α).symm_apply_apply f
 
 /-- If `α` has a unique term, then the type of finitely supported functions `α →₀ M` is
 `R`-linearly equivalent to `M`. -/
 noncomputable def linear_equiv.finsupp_unique (α : Type*) [unique α] : (α →₀ M) ≃ₗ[R] M :=
 { map_add' := λ x y, rfl,
   map_smul' := λ r x, rfl,
-  ..finsupp.equiv_fun_on_fintype.trans (equiv.fun_unique α M) }
+  ..finsupp.equiv_fun_on_finite.trans (equiv.fun_unique α M) }
 
 variables {R M α}
 

src/linear_algebra/basis.lean

@@ -742,7 +742,7 @@ linear_equiv.trans b.repr
   ({ to_fun := coe_fn,
      map_add' := finsupp.coe_add,
      map_smul' := finsupp.coe_smul,
-     ..finsupp.equiv_fun_on_fintype } : (ι →₀ R) ≃ₗ[R] (ι → R))
+     ..finsupp.equiv_fun_on_finite } : (ι →₀ R) ≃ₗ[R] (ι → R))
 
 /-- A module over a finite ring that admits a finite basis is finite. -/
 def module.fintype_of_fintype [fintype R] : fintype M :=
@@ -792,7 +792,7 @@ end
 /-- Define a basis by mapping each vector `x : M` to its coordinates `e x : ι → R`,
 as long as `ι` is finite. -/
 def basis.of_equiv_fun (e : M ≃ₗ[R] (ι → R)) : basis ι R M :=
-basis.of_repr $ e.trans $ linear_equiv.symm $ finsupp.linear_equiv_fun_on_fintype R R ι
+basis.of_repr $ e.trans $ linear_equiv.symm $ finsupp.linear_equiv_fun_on_finite R R ι
 
 @[simp] lemma basis.of_equiv_fun_repr_apply (e : M ≃ₗ[R] (ι → R)) (x : M) (i : ι) :
   (basis.of_equiv_fun e).repr x i = e x i := rfl
@@ -822,11 +822,11 @@ by simp [b.constr_apply, b.equiv_fun_apply, finsupp.sum_fintype]
 `x ∈ P` iff it is a linear combination of basis vectors. -/
 lemma basis.mem_submodule_iff' {P : submodule R M} (b : basis ι R P) {x : M} :
   x ∈ P ↔ ∃ (c : ι → R), x = ∑ i, c i • b i :=
-b.mem_submodule_iff.trans $ finsupp.equiv_fun_on_fintype.exists_congr_left.trans $ exists_congr $
+b.mem_submodule_iff.trans $ finsupp.equiv_fun_on_finite.exists_congr_left.trans $ exists_congr $
 λ c, by simp [finsupp.sum_fintype]
 
 lemma basis.coord_equiv_fun_symm (i : ι) (f : ι → R) : b.coord i (b.equiv_fun.symm f) = f i :=
-b.coord_repr_symm i (finsupp.equiv_fun_on_fintype.symm f)
+b.coord_repr_symm i (finsupp.equiv_fun_on_finite.symm f)
 
 end fintype
 

src/linear_algebra/dimension.lean

@@ -514,8 +514,8 @@ begin
     simp only [cardinal.lift_nat_cast, cardinal.nat_cast_inj],
     -- Now we can use invariant basis number to show they have the same cardinality.
     apply card_eq_of_lequiv R,
-    exact (((finsupp.linear_equiv_fun_on_fintype R R ι).symm.trans v.repr.symm) ≪≫ₗ
-      v'.repr) ≪≫ₗ (finsupp.linear_equiv_fun_on_fintype R R ι'), },
+    exact (((finsupp.linear_equiv_fun_on_finite R R ι).symm.trans v.repr.symm) ≪≫ₗ
+      v'.repr) ≪≫ₗ (finsupp.linear_equiv_fun_on_finite R R ι'), },
   { -- `v` is an infinite basis,
     -- so by `infinite_basis_le_maximal_linear_independent`, `v'` is at least as big,
     -- and then applying `infinite_basis_le_maximal_linear_independent` again

src/linear_algebra/dual.lean

@@ -176,7 +176,7 @@ begin
   casesI nonempty_fintype ι,
   refine eq_top_iff'.2 (λ f, _),
   rw linear_map.mem_range,
-  let lin_comb : ι →₀ R := finsupp.equiv_fun_on_fintype.2 (λ i, f.to_fun (b i)),
+  let lin_comb : ι →₀ R := finsupp.equiv_fun_on_finite.symm (λ i, f.to_fun (b i)),
   refine ⟨finsupp.total ι M R b lin_comb, b.ext $ λ i, _⟩,
   rw [b.to_dual_eq_repr _ i, repr_total b],
   refl,

src/linear_algebra/finite_dimensional.lean

@@ -786,11 +786,7 @@ variables [division_ring K] [add_comm_group V] [module K V]
 
 instance finite_dimensional_finsupp {ι : Type*} [_root_.finite ι] [h : finite_dimensional K V] :
   finite_dimensional K (ι →₀ V) :=
-begin
-  casesI nonempty_fintype ι,
-  letI : is_noetherian K V := is_noetherian.iff_fg.2 infer_instance,
-  exact (finsupp.linear_equiv_fun_on_fintype K V ι).symm.finite_dimensional
-end
+(finsupp.linear_equiv_fun_on_finite K V ι).symm.finite_dimensional
 
 end
 
@@ -1477,7 +1473,7 @@ begin
   let s := basis.of_vector_space_index K V,
   let hs := basis.of_vector_space K V,
   calc #V = #(s →₀ K) : quotient.sound ⟨hs.repr.to_equiv⟩
-    ... = #(s → K) : quotient.sound ⟨finsupp.equiv_fun_on_fintype⟩
+    ... = #(s → K) : quotient.sound ⟨finsupp.equiv_fun_on_finite⟩
     ... = _ : by rw [← cardinal.lift_inj.1 hs.mk_eq_dim, cardinal.power_def]
 end
 

src/linear_algebra/finsupp.lean

@@ -866,7 +866,7 @@ end
 variables (S)
 
 lemma finsupp.total_eq_fintype_total_apply (x : α → R) :
-  finsupp.total α M R v ((finsupp.linear_equiv_fun_on_fintype R R α).symm x) =
+  finsupp.total α M R v ((finsupp.linear_equiv_fun_on_finite R R α).symm x) =
     fintype.total R S v x :=
 begin
   apply finset.sum_subset,
@@ -877,7 +877,7 @@ begin
 end
 
 lemma finsupp.total_eq_fintype_total :
-  (finsupp.total α M R v).comp (finsupp.linear_equiv_fun_on_fintype R R α).symm.to_linear_map =
+  (finsupp.total α M R v).comp (finsupp.linear_equiv_fun_on_finite R R α).symm.to_linear_map =
     fintype.total R S v :=
 linear_map.ext $ finsupp.total_eq_fintype_total_apply R S v
 
@@ -899,7 +899,7 @@ lemma mem_span_range_iff_exists_fun :
   x ∈ span R (range v) ↔ ∃ (c : α → R), ∑ i, c i • v i = x :=
 begin
   simp only [finsupp.mem_span_range_iff_exists_finsupp,
-    finsupp.equiv_fun_on_fintype.surjective.exists, finsupp.equiv_fun_on_fintype_apply],
+    finsupp.equiv_fun_on_finite.surjective.exists, finsupp.equiv_fun_on_finite_apply],
   exact exists_congr (λ c, eq.congr_left $ finsupp.sum_fintype _ _ $ λ i, zero_smul _ _)
 end
 
@@ -1027,15 +1027,15 @@ lemma splitting_of_finsupp_surjective_injective (f : M →ₗ[R] (α →₀ R))
 def splitting_of_fun_on_fintype_surjective [fintype α] (f : M →ₗ[R] (α → R)) (s : surjective f) :
   (α → R) →ₗ[R] M :=
 (finsupp.lift _ _ _ (λ x : α, (s (finsupp.single x 1)).some)).comp
-  (linear_equiv_fun_on_fintype R R α).symm.to_linear_map
+  (linear_equiv_fun_on_finite R R α).symm.to_linear_map
 
 lemma splitting_of_fun_on_fintype_surjective_splits
   [fintype α] (f : M →ₗ[R] (α → R)) (s : surjective f) :
   f.comp (splitting_of_fun_on_fintype_surjective f s) = linear_map.id :=
 begin
   ext x y,
   dsimp [splitting_of_fun_on_fintype_surjective],
-  rw [linear_equiv_fun_on_fintype_symm_single, finsupp.sum_single_index, one_smul,
+  rw [linear_equiv_fun_on_finite_symm_single, finsupp.sum_single_index, one_smul,
     (s (finsupp.single x 1)).some_spec, finsupp.single_eq_pi_single],
   rw [zero_smul],
 end

src/linear_algebra/invariant_basis_number.lean

@@ -106,8 +106,8 @@ end
 lemma card_le_of_injective' [strong_rank_condition R] {α β : Type*} [fintype α] [fintype β]
   (f : (α →₀ R) →ₗ[R] (β →₀ R)) (i : injective f) : fintype.card α ≤ fintype.card β :=
 begin
-  let P := (finsupp.linear_equiv_fun_on_fintype R R β),
-  let Q := (finsupp.linear_equiv_fun_on_fintype R R α).symm,
+  let P := (finsupp.linear_equiv_fun_on_finite R R β),
+  let Q := (finsupp.linear_equiv_fun_on_finite R R α).symm,
   exact card_le_of_injective R ((P.to_linear_map.comp f).comp Q.to_linear_map)
     ((P.injective.comp i).comp Q.injective)
 end
@@ -133,8 +133,8 @@ end
 lemma card_le_of_surjective' [rank_condition R] {α β : Type*} [fintype α] [fintype β]
   (f : (α →₀ R) →ₗ[R] (β →₀ R)) (i : surjective f) : fintype.card β ≤ fintype.card α :=
 begin
-  let P := (finsupp.linear_equiv_fun_on_fintype R R β),
-  let Q := (finsupp.linear_equiv_fun_on_fintype R R α).symm,
+  let P := (finsupp.linear_equiv_fun_on_finite R R β),
+  let Q := (finsupp.linear_equiv_fun_on_finite R R α).symm,
   exact card_le_of_surjective R ((P.to_linear_map.comp f).comp Q.to_linear_map)
     ((P.surjective.comp i).comp Q.surjective)
 end

src/set_theory/cardinal/basic.lean

@@ -886,7 +886,7 @@ lemma mk_finset_of_fintype [fintype α] : #(finset α) = 2 ^ℕ fintype.card α
 
 @[simp] lemma mk_finsupp_lift_of_fintype (α : Type u) (β : Type v) [fintype α] [has_zero β] :
   #(α →₀ β) = lift.{u} (#β) ^ℕ fintype.card α :=
-by simpa using (@finsupp.equiv_fun_on_fintype α β _ _).cardinal_eq
+by simpa using (@finsupp.equiv_fun_on_finite α β _ _).cardinal_eq
 
 lemma mk_finsupp_of_fintype (α β : Type u) [fintype α] [has_zero β] :
   #(α →₀ β) = (#β) ^ℕ fintype.card α :=