chore(group_theory/*): Fix lint (#16095)

Fix the linting errors coming from `fintype_finite` and `to_additive_doc` in the `group_theory` folder (+ some in `data` and `combinatorics`). Remove the decidability assumptions to `decidable_powers`/`decidable_zpowers` because they are already noncomputable.

## Lemma renames
* `fintype` → `finite` in lemmas that used to assume `fintype` and now only assume `finite`
* `fintype.induction_empty_option'` → `fintype.induction_empty_option`

Author: YaelDillies

archive/sensitivity.lean

@@ -393,7 +393,7 @@ begin
     rw set.mem_to_finset,
     exact (dual_pair_e_ε _).mem_of_mem_span y_mem_H p p_in },
   obtain ⟨q, H_max⟩ : ∃ q : Q (m+1), ∀ q' : Q (m+1), |(ε q' : _) y| ≤ |ε q y|,
-    from fintype.exists_max _,
+    from finite.exists_max _,
   have H_q_pos : 0 < |ε q y|,
   { contrapose! y_ne,
     exact epsilon_total (λ p, abs_nonpos_iff.mp (le_trans (H_max p) y_ne)) },

docs/overview.yaml

@@ -405,7 +405,7 @@ Combinatorics:
     adjacency matrix: 'simple_graph.adj_matrix'
   Pigeonhole principles:
     finite: 'fintype.exists_ne_map_eq_of_card_lt'
-    infinite: 'fintype.exists_infinite_fiber'
+    infinite: 'finite.exists_infinite_fiber'
     strong pigeonhole principle: 'fintype.exists_lt_card_fiber_of_mul_lt_card'
   Transversals:
     Hall's marriage theorem: 'finset.all_card_le_bUnion_card_iff_exists_injective'

src/algebra/char_p/basic.lean

@@ -354,7 +354,7 @@ begin
   unfreezingI { rintro rfl },
   haveI : char_zero R := char_p_to_char_zero R,
   casesI nonempty_fintype R,
-  exact absurd nat.cast_injective (not_injective_infinite_fintype (coe : ℕ → R))
+  exact absurd nat.cast_injective (not_injective_infinite_finite (coe : ℕ → R))
 end
 
 lemma ring_char_ne_zero_of_finite [finite R] : ring_char R ≠ 0 :=

src/combinatorics/hales_jewett.lean

@@ -172,10 +172,10 @@ by simp_rw [line.apply, line.diagonal, option.get_or_else_none]
 /-- The Hales-Jewett theorem. This version has a restriction on universe levels which is necessary
 for the proof. See `exists_mono_in_high_dimension` for a fully universe-polymorphic version. -/
 private theorem exists_mono_in_high_dimension' :
-  ∀ (α : Type u) [fintype α] (κ : Type (max v u)) [finite κ],
+  ∀ (α : Type u) [finite α] (κ : Type (max v u)) [finite κ],
   ∃ (ι : Type) (_ : fintype ι), ∀ C : (ι → α) → κ, ∃ l : line α ι, l.is_mono C :=
 -- The proof proceeds by induction on `α`.
-fintype.induction_empty_option
+finite.induction_empty_option
 -- We have to show that the theorem is invariant under `α ≃ α'` for the induction to work.
 (λ α α' e, forall_imp $ λ κ, forall_imp $ λ _, Exists.imp $ λ ι, Exists.imp $ λ _ h C,
   let ⟨l, c, lc⟩ := h (λ v, C (e ∘ v)) in
@@ -268,7 +268,7 @@ end
 
 /-- The Hales-Jewett theorem: for any finite types `α` and `κ`, there exists a finite type `ι` such
 that whenever the hypercube `ι → α` is `κ`-colored, there is a monochromatic combinatorial line. -/
-theorem exists_mono_in_high_dimension (α : Type u) [fintype α] (κ : Type v) [finite κ] :
+theorem exists_mono_in_high_dimension (α : Type u) [finite α] (κ : Type v) [finite κ] :
   ∃ (ι : Type) [fintype ι], ∀ C : (ι → α) → κ, ∃ l : line α ι, l.is_mono C :=
 let ⟨ι, ιfin, hι⟩ := exists_mono_in_high_dimension' α (ulift κ)
 in ⟨ι, ιfin, λ C, let ⟨l, c, hc⟩ := hι (ulift.up ∘ C) in ⟨l, c.down, λ x, by rw ←hc⟩ ⟩

src/combinatorics/pigeonhole.lean

@@ -23,8 +23,8 @@ following locations:
 
 * `data.finset.basic` has `finset.exists_ne_map_eq_of_card_lt_of_maps_to`
 * `data.fintype.basic` has `fintype.exists_ne_map_eq_of_card_lt`
-* `data.fintype.basic` has `fintype.exists_ne_map_eq_of_infinite`
-* `data.fintype.basic` has `fintype.exists_infinite_fiber`
+* `data.fintype.basic` has `finite.exists_ne_map_eq_of_infinite`
+* `data.fintype.basic` has `finite.exists_infinite_fiber`
 * `data.set.finite` has `set.infinite.exists_ne_map_eq_of_maps_to`
 
 This module gives access to these pigeonhole principles along with 20 more.

src/combinatorics/simple_graph/coloring.lean

@@ -365,7 +365,7 @@ end
 begin
   apply chromatic_number_eq_card_of_forall_surj (self_coloring _),
   intro C,
-  rw ←fintype.injective_iff_surjective,
+  rw ←finite.injective_iff_surjective,
   intros v w,
   contrapose,
   intro h,

src/computability/primrec.lean

@@ -648,7 +648,7 @@ theorem list_index_of₁ [decidable_eq α] (l : list α) :
   primrec (λ a, l.index_of a) := list_find_index₁ primrec.eq l
 
 theorem dom_fintype [fintype α] (f : α → σ) : primrec f :=
-let ⟨l, nd, m⟩ := fintype.exists_univ_list α in
+let ⟨l, nd, m⟩ := finite.exists_univ_list α in
 option_some_iff.1 $ begin
   haveI := decidable_eq_of_encodable α,
   refine ((list_nth₁ (l.map f)).comp (list_index_of₁ l)).of_eq (λ a, _),

src/data/W/basic.lean

@@ -90,7 +90,7 @@ lemma infinite_of_nonempty_of_is_empty (a b : α) [ha : nonempty (β a)]
 ⟨begin
   introsI hf,
   have hba : b ≠ a, from λ h, ha.elim (is_empty.elim' (show is_empty (β a), from h ▸ he)),
-  refine not_injective_infinite_fintype
+  refine not_injective_infinite_finite
     (λ n : ℕ, show W_type β, from nat.rec_on n
       ⟨b, is_empty.elim' he⟩
       (λ n ih, ⟨a, λ _, ih⟩)) _,

src/data/finite/basic.lean

@@ -42,38 +42,15 @@ open_locale classical
 
 variables {α β γ : Type*}
 
-lemma not_finite_iff_infinite {α : Type*} : ¬ finite α ↔ infinite α :=
-by rw [← is_empty_fintype, finite_iff_nonempty_fintype, not_nonempty_iff]
-
 lemma finite_or_infinite (α : Type*) :
   finite α ∨ infinite α :=
 begin
   rw ← not_finite_iff_infinite,
   apply em
 end
 
-lemma not_finite (α : Type*) [h1 : infinite α] [h2 : finite α] : false :=
-not_finite_iff_infinite.mpr h1 h2
-
-lemma finite.of_not_infinite {α : Type*} (h : ¬ infinite α) : finite α :=
-by rwa [← not_finite_iff_infinite, not_not] at h
-
-lemma infinite.of_not_finite {α : Type*} (h : ¬ finite α) : infinite α :=
-not_finite_iff_infinite.mp h
-
-lemma not_infinite_iff_finite {α : Type*} : ¬ infinite α ↔ finite α :=
-not_finite_iff_infinite.not_right.symm
-
 namespace finite
 
-lemma exists_max [finite α] [nonempty α] [linear_order β] (f : α → β) :
-  ∃ x₀ : α, ∀ x, f x ≤ f x₀ :=
-by { haveI := fintype.of_finite α, exact fintype.exists_max f }
-
-lemma exists_min [finite α] [nonempty α] [linear_order β] (f : α → β) :
-  ∃ x₀ : α, ∀ x, f x₀ ≤ f x :=
-by { haveI := fintype.of_finite α, exact fintype.exists_min f }
-
 @[priority 100] -- see Note [lower instance priority]
 instance of_subsingleton {α : Sort*} [subsingleton α] : finite α :=
 of_injective (function.const α ()) $ function.injective_of_subsingleton _
@@ -108,6 +85,8 @@ by { letI := fintype.of_finite α, letI := λ a, fintype.of_finite (β a), apply
 instance {ι : Sort*} {π : ι → Sort*} [finite ι] [Π i, finite (π i)] : finite (Σ' i, π i) :=
 of_equiv _ (equiv.psigma_equiv_sigma_plift π).symm
 
+instance [finite α] : finite (set α) := by { casesI nonempty_fintype α, apply_instance }
+
 end finite
 
 /-- This instance also provides `[finite s]` for `s : set α`. -/