diff --git a/archive/sensitivity.lean b/archive/sensitivity.lean
index b0dfa141ff98a..9c0342613cc0e 100644
--- a/archive/sensitivity.lean
+++ b/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)) },
diff --git a/docs/overview.yaml b/docs/overview.yaml
index ebc2cb1ada44f..448a2d9240055 100644
--- a/docs/overview.yaml
+++ b/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'
diff --git a/src/algebra/char_p/basic.lean b/src/algebra/char_p/basic.lean
index f2659a1c17441..46a92ff99b756 100644
--- a/src/algebra/char_p/basic.lean
+++ b/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 :=
diff --git a/src/combinatorics/hales_jewett.lean b/src/combinatorics/hales_jewett.lean
index 7f99050461080..0102dc5a1bf83 100644
--- a/src/combinatorics/hales_jewett.lean
+++ b/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⟩ ⟩
diff --git a/src/combinatorics/pigeonhole.lean b/src/combinatorics/pigeonhole.lean
index 7c3655380f457..e40201be6f968 100644
--- a/src/combinatorics/pigeonhole.lean
+++ b/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.
diff --git a/src/combinatorics/simple_graph/coloring.lean b/src/combinatorics/simple_graph/coloring.lean
index cfe23aca33b75..d6544452730ad 100644
--- a/src/combinatorics/simple_graph/coloring.lean
+++ b/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,
diff --git a/src/computability/primrec.lean b/src/computability/primrec.lean
index ab3c7282e898a..f67742e7b230c 100644
--- a/src/computability/primrec.lean
+++ b/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, _),
diff --git a/src/data/W/basic.lean b/src/data/W/basic.lean
index c359b858fd788..cd30bc7b23bfb 100644
--- a/src/data/W/basic.lean
+++ b/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⟩)) _,
diff --git a/src/data/finite/basic.lean b/src/data/finite/basic.lean
index f3700752eea39..cd984fca51e83 100644
--- a/src/data/finite/basic.lean
+++ b/src/data/finite/basic.lean
@@ -42,9 +42,6 @@ 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
@@ -52,28 +49,8 @@ begin
   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 α`. -/
diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
index e209416bcfe69..e4056cd670c4b 100644
--- a/src/data/fintype/basic.lean
+++ b/src/data/fintype/basic.lean
@@ -36,15 +36,15 @@ This file defines a typeclass to state that a type is finite.
   equivalent. See above.
 * `fin.equiv_iff_eq`: `fin m ≃ fin n` iff `m = n`.
 * `infinite α`: Typeclass saying that a type is infinite. Defined as `fintype α → false`.
-* `not_fintype`: No `fintype` has an `infinite` instance.
+* `not_finite`: No `finite` type has an `infinite` instance.
 * `infinite.nat_embedding`: An embedding of `ℕ` into an infinite type.
 
 We also provide the following versions of the pigeonholes principle.
 * `fintype.exists_ne_map_eq_of_card_lt` and `is_empty_of_card_lt`: Finitely many pigeons and
   pigeonholes. Weak formulation.
-* `fintype.exists_ne_map_eq_of_infinite`: Infinitely many pigeons in finitely many pigeonholes.
+* `finite.exists_ne_map_eq_of_infinite`: Infinitely many pigeons in finitely many pigeonholes.
   Weak formulation.
-* `fintype.exists_infinite_fiber`: Infinitely many pigeons in finitely many pigeonholes. Strong
+* `finite.exists_infinite_fiber`: Infinitely many pigeons in finitely many pigeonholes. Strong
   formulation.
 
 Some more pigeonhole-like statements can be found in `data.fintype.card_embedding`.
@@ -315,15 +315,6 @@ instance decidable_left_inverse_fintype [decidable_eq β] [fintype β] (f : α 
   decidable (function.left_inverse f g) :=
 show decidable (∀ x, f (g x) = x), by apply_instance
 
-lemma exists_max [fintype α] [nonempty α] {β : Type*} [linear_order β] (f : α → β) :
-  ∃ x₀ : α, ∀ x, f x ≤ f x₀ :=
-by simpa using exists_max_image univ f univ_nonempty
-
-lemma exists_min [fintype α] [nonempty α]
-  {β : Type*} [linear_order β] (f : α → β) :
-  ∃ x₀ : α, ∀ x, f x₀ ≤ f x :=
-by simpa using exists_min_image univ f univ_nonempty
-
 /-- Construct a proof of `fintype α` from a universal multiset -/
 def of_multiset [decidable_eq α] (s : multiset α) (H : ∀ x : α, x ∈ s) :
   fintype α :=
@@ -334,12 +325,6 @@ def of_list [decidable_eq α] (l : list α) (H : ∀ x : α, x ∈ l) :
   fintype α :=
 ⟨l.to_finset, by simpa using H⟩
 
-theorem exists_univ_list (α) [fintype α] :
-  ∃ l : list α, l.nodup ∧ ∀ x : α, x ∈ l :=
-let ⟨l, e⟩ := quotient.exists_rep (@univ α _).1 in
-by have := and.intro univ.2 mem_univ_val;
-   exact ⟨_, by rwa ←e at this⟩
-
 /-- `card α` is the number of elements in `α`, defined when `α` is a fintype. -/
 def card (α) [fintype α] : ℕ := (@univ α _).card
 
@@ -943,6 +928,7 @@ fintype.of_equiv _ equiv.plift.symm
 fintype.of_equiv_card _
 
 instance (α : Type*) [fintype α] : fintype αᵒᵈ := ‹fintype α›
+instance (α : Type*) [finite α] : finite αᵒᵈ := ‹finite α›
 
 @[simp] lemma fintype.card_order_dual (α : Type*) [fintype α] : fintype.card αᵒᵈ = fintype.card α :=
 rfl
@@ -1045,6 +1031,18 @@ lemma finite.of_surjective {α β : Sort*} [finite α] (f : α → β) (H : surj
   finite β :=
 finite.of_injective _ $ injective_surj_inv H
 
+lemma finite.exists_max [finite α] [nonempty α] [linear_order β] (f : α → β) :
+ ∃ x₀ : α, ∀ x, f x ≤ f x₀ :=
+by { casesI nonempty_fintype α, simpa using exists_max_image univ f univ_nonempty }
+
+lemma finite.exists_min [finite α] [nonempty α] [linear_order β] (f : α → β) :
+  ∃ x₀ : α, ∀ x, f x₀ ≤ f x :=
+by { casesI nonempty_fintype α, simpa using exists_min_image univ f univ_nonempty }
+
+lemma finite.exists_univ_list (α) [finite α] : ∃ l : list α, l.nodup ∧ ∀ x : α, x ∈ l :=
+by { casesI nonempty_fintype α, obtain ⟨l, e⟩ := quotient.exists_rep (@univ α _).1,
+  have := and.intro univ.2 mem_univ_val, exact ⟨_, by rwa ←e at this⟩ }
+
 namespace fintype
 variables [fintype α] [fintype β]
 
@@ -1154,8 +1152,16 @@ one_lt_card_iff_nontrivial.trans nontrivial_iff
 lemma two_lt_card_iff : 2 < card α ↔ ∃ a b c : α, a ≠ b ∧ a ≠ c ∧ b ≠ c :=
 by simp_rw [←finset.card_univ, two_lt_card_iff, mem_univ, true_and]
 
+lemma card_of_bijective {f : α → β} (hf : bijective f) : card α = card β :=
+card_congr (equiv.of_bijective f hf)
+
+end fintype
+
+namespace finite
+variables [finite α]
+
 lemma injective_iff_surjective {f : α → α} : injective f ↔ surjective f :=
-by haveI := classical.prop_decidable; exact
+by haveI := classical.prop_decidable; casesI nonempty_fintype α; exact
 have ∀ {f : α → α}, injective f → surjective f,
 from λ f hinj x,
   have h₁ : image f univ = univ := eq_of_subset_of_card_le (subset_univ _)
@@ -1173,19 +1179,23 @@ by simp [bijective, injective_iff_surjective]
 lemma surjective_iff_bijective {f : α → α} : surjective f ↔ bijective f :=
 by simp [bijective, injective_iff_surjective]
 
-lemma injective_iff_surjective_of_equiv {β : Type*} {f : α → β} (e : α ≃ β) :
-  injective f ↔ surjective f :=
+lemma injective_iff_surjective_of_equiv  {f : α → β} (e : α ≃ β) : injective f ↔ surjective f :=
 have injective (e.symm ∘ f) ↔ surjective (e.symm ∘ f), from injective_iff_surjective,
 ⟨λ hinj, by simpa [function.comp] using
   e.surjective.comp (this.1 (e.symm.injective.comp hinj)),
 λ hsurj, by simpa [function.comp] using
   e.injective.comp (this.2 (e.symm.surjective.comp hsurj))⟩
 
-alias fintype.injective_iff_surjective_of_equiv ↔ _root_.function.injective.surjective_of_fintype
+
+alias injective_iff_bijective ↔ _root_.function.injective.bijective_of_finite _
+alias surjective_iff_bijective ↔ _root_.function.surjective.bijective_of_finite _
+alias injective_iff_surjective_of_equiv ↔ _root_.function.injective.surjective_of_fintype
   _root_.function.surjective.injective_of_fintype
 
-lemma card_of_bijective {f : α → β} (hf : bijective f) : card α = card β :=
-card_congr (equiv.of_bijective f hf)
+end finite
+
+namespace fintype
+variables [fintype α] [fintype β]
 
 lemma bijective_iff_injective_and_card (f : α → β) :
   bijective f ↔ injective f ∧ card α = card β :=
@@ -1335,11 +1345,11 @@ end
 namespace function.embedding
 
 /-- An embedding from a `fintype` to itself can be promoted to an equivalence. -/
-noncomputable def equiv_of_fintype_self_embedding [fintype α] (e : α ↪ α) : α ≃ α :=
-equiv.of_bijective e (fintype.injective_iff_bijective.1 e.2)
+noncomputable def equiv_of_fintype_self_embedding [finite α] (e : α ↪ α) : α ≃ α :=
+equiv.of_bijective e e.2.bijective_of_finite
 
 @[simp]
-lemma equiv_of_fintype_self_embedding_to_embedding [fintype α] (e : α ↪ α) :
+lemma equiv_of_fintype_self_embedding_to_embedding [finite α] (e : α ↪ α) :
   e.equiv_of_fintype_self_embedding.to_embedding = e :=
 by { ext, refl, }
 
@@ -1560,13 +1570,12 @@ theorem fintype.card_subtype_mono (p q : α → Prop) (h : p ≤ q)
 fintype.card_le_of_embedding (subtype.imp_embedding _ _ h)
 
 /-- If two subtypes of a fintype have equal cardinality, so do their complements. -/
-lemma fintype.card_compl_eq_card_compl [fintype α]
-  (p q : α → Prop)
+lemma fintype.card_compl_eq_card_compl [finite α] (p q : α → Prop)
   [fintype {x // p x}] [fintype {x // ¬ p x}]
   [fintype {x // q x}] [fintype {x // ¬ q x}]
   (h : fintype.card {x // p x} = fintype.card {x // q x}) :
   fintype.card {x // ¬ p x} = fintype.card {x // ¬ q x} :=
-by simp only [fintype.card_subtype_compl, h]
+by { casesI nonempty_fintype α, simp only [fintype.card_subtype_compl, h] }
 
 theorem fintype.card_quotient_le [fintype α] (s : setoid α) [decidable_rel ((≈) : α → α → Prop)] :
   fintype.card (quotient s) ≤ fintype.card α :=
@@ -1600,6 +1609,10 @@ instance set.fintype [fintype α] : fintype (set α) :=
   apply (coe_filter _ _).trans, rw [coe_univ, set.sep_univ], refl
 end⟩
 
+-- Not to be confused with `set.finite`, the predicate
+instance set.finite' [finite α] : finite (set α) :=
+by { casesI nonempty_fintype α, apply_instance }
+
 @[simp] lemma fintype.card_set [fintype α] : fintype.card (set α) = 2 ^ fintype.card α :=
 (finset.card_map _).trans (finset.card_powerset _)
 
@@ -1877,10 +1890,14 @@ lemma bijective_bij_inv (f_bij : bijective f) : bijective (bij_inv f_bij) :=
 ⟨(right_inverse_bij_inv _).injective, (left_inverse_bij_inv _).surjective⟩
 
 end bijection_inverse
+end fintype
 
-lemma well_founded_of_trans_of_irrefl [fintype α] (r : α → α → Prop)
-  [is_trans α r] [is_irrefl α r] : well_founded r :=
-by classical; exact
+namespace finite
+variables [finite α]
+
+lemma well_founded_of_trans_of_irrefl (r : α → α → Prop) [is_trans α r] [is_irrefl α r] :
+  well_founded r :=
+by classical; casesI nonempty_fintype α; exact
 have ∀ x y, r x y → (univ.filter (λ z, r z x)).card < (univ.filter (λ z, r z y)).card,
   from λ x y hxy, finset.card_lt_card $
     by simp only [finset.lt_iff_ssubset.symm, lt_iff_le_not_le,
@@ -1888,39 +1905,45 @@ have ∀ x y, r x y → (univ.filter (λ z, r z x)).card < (univ.filter (λ z, r
     exact ⟨λ z hzx, trans hzx hxy, not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩,
 subrelation.wf this (measure_wf _)
 
-lemma preorder.well_founded_lt [fintype α] [preorder α] : well_founded ((<) : α → α → Prop) :=
+lemma preorder.well_founded_lt [preorder α] : well_founded ((<) : α → α → Prop) :=
 well_founded_of_trans_of_irrefl _
 
-lemma preorder.well_founded_gt [fintype α] [preorder α] : well_founded ((>) : α → α → Prop) :=
+lemma preorder.well_founded_gt [preorder α] : well_founded ((>) : α → α → Prop) :=
 well_founded_of_trans_of_irrefl _
 
-@[instance, priority 10] lemma linear_order.is_well_order_lt [fintype α] [linear_order α] :
-  is_well_order α (<) :=
+@[priority 10] instance linear_order.is_well_order_lt [linear_order α] : is_well_order α (<) :=
 { wf := preorder.well_founded_lt }
 
-@[instance, priority 10] lemma linear_order.is_well_order_gt [fintype α] [linear_order α] :
-  is_well_order α (>) :=
+@[priority 10] instance linear_order.is_well_order_gt [linear_order α] : is_well_order α (>) :=
 { wf := preorder.well_founded_gt }
 
-end fintype
+end finite
 
 /-- A type is said to be infinite if it has no fintype instance.
   Note that `infinite α` is equivalent to `is_empty (fintype α)`. -/
 class infinite (α : Type*) : Prop :=
 (not_fintype : fintype α → false)
 
-lemma not_fintype (α : Type*) [h1 : infinite α] [h2 : fintype α] : false :=
-infinite.not_fintype h2
+lemma not_finite (α : Type*) [infinite α] [finite α] : false :=
+by { casesI nonempty_fintype α, exact infinite.not_fintype ‹_› }
 
-protected lemma fintype.false {α : Type*} [infinite α] (h : fintype α) : false :=
-not_fintype α
+protected lemma finite.false [infinite α] (h : finite α) : false := not_finite α
 
-protected lemma infinite.false {α : Type*} [fintype α] (h : infinite α) : false :=
-not_fintype α
+@[nolint fintype_finite]
+protected lemma fintype.false [infinite α] (h : fintype α) : false := not_finite α
+protected lemma infinite.false [finite α] (h : infinite α) : false := not_finite α
 
 @[simp] lemma is_empty_fintype {α : Type*} : is_empty (fintype α) ↔ infinite α :=
 ⟨λ ⟨x⟩, ⟨x⟩, λ ⟨x⟩, ⟨x⟩⟩
 
+lemma not_finite_iff_infinite : ¬ finite α ↔ infinite α :=
+by rw [← is_empty_fintype, finite_iff_nonempty_fintype, not_nonempty_iff]
+
+lemma not_infinite_iff_finite : ¬ infinite α ↔ finite α := not_finite_iff_infinite.not_right.symm
+
+alias not_finite_iff_infinite ↔ infinite.of_not_finite infinite.not_finite
+alias not_infinite_iff_finite ↔ finite.of_not_infinite finite.not_infinite
+
 /-- A non-infinite type is a fintype. -/
 noncomputable def fintype_of_not_infinite {α : Type*} (h : ¬ infinite α) : fintype α :=
 nonempty.some $ by rwa [← not_is_empty_iff, is_empty_fintype]
@@ -1942,7 +1965,7 @@ lemma finset.exists_minimal {α : Type*} [preorder α] (s : finset α) (h : s.no
   ∃ m ∈ s, ∀ x ∈ s, ¬ (x < m) :=
 begin
   obtain ⟨c, hcs : c ∈ s⟩ := h,
-  have : well_founded (@has_lt.lt {x // x ∈ s} _) := fintype.well_founded_of_trans_of_irrefl _,
+  have : well_founded (@has_lt.lt {x // x ∈ s} _) := finite.well_founded_of_trans_of_irrefl _,
   obtain ⟨⟨m, hms : m ∈ s⟩, -, H⟩ := this.has_min set.univ ⟨⟨c, hcs⟩, trivial⟩,
   exact ⟨m, hms, λ x hx hxm, H ⟨x, hx⟩ trivial hxm⟩,
 end
@@ -2089,27 +2112,26 @@ begin
   exact nat.not_succ_le_self n w,
 end
 
-lemma not_injective_infinite_fintype [infinite α] [fintype β] (f : α → β) :
-  ¬ injective f :=
-λ hf, (fintype.of_injective f hf).false
+lemma not_injective_infinite_finite [infinite α] [finite β] (f : α → β) : ¬ injective f :=
+λ hf, (finite.of_injective f hf).not_infinite ‹_›
 
 /--
 The pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are
 infinitely many pigeons in finitely many pigeonholes, then there are at least two pigeons in the
 same pigeonhole.
 
-See also: `fintype.exists_ne_map_eq_of_card_lt`, `fintype.exists_infinite_fiber`.
+See also: `fintype.exists_ne_map_eq_of_card_lt`, `finite.exists_infinite_fiber`.
 -/
-lemma fintype.exists_ne_map_eq_of_infinite [infinite α] [fintype β] (f : α → β) :
+lemma finite.exists_ne_map_eq_of_infinite [infinite α] [finite β] (f : α → β) :
   ∃ x y : α, x ≠ y ∧ f x = f y :=
 begin
   classical, by_contra' hf,
-  apply not_injective_infinite_fintype f,
+  apply not_injective_infinite_finite f,
   intros x y, contrapose, apply hf,
 end
 
-instance function.embedding.is_empty {α β} [infinite α] [fintype β] : is_empty (α ↪ β) :=
-⟨λ f, let ⟨x, y, ne, feq⟩ := fintype.exists_ne_map_eq_of_infinite f in ne $ f.injective feq⟩
+instance function.embedding.is_empty {α β} [infinite α] [finite β] : is_empty (α ↪ β) :=
+⟨λ f, let ⟨x, y, ne, feq⟩ := finite.exists_ne_map_eq_of_infinite f in ne $ f.injective feq⟩
 
 /--
 The strong pigeonhole principle for infinitely many pigeons in
@@ -2117,14 +2139,14 @@ finitely many pigeonholes.  If there are infinitely many pigeons in
 finitely many pigeonholes, then there is a pigeonhole with infinitely
 many pigeons.
 
-See also: `fintype.exists_ne_map_eq_of_infinite`
+See also: `finite.exists_ne_map_eq_of_infinite`
 -/
-lemma fintype.exists_infinite_fiber [infinite α] [fintype β] (f : α → β) :
+lemma finite.exists_infinite_fiber [infinite α] [finite β] (f : α → β) :
   ∃ y : β, infinite (f ⁻¹' {y}) :=
 begin
   classical,
   by_contra' hf,
-
+  casesI nonempty_fintype β,
   haveI := λ y, fintype_of_not_infinite $ hf y,
   let key : fintype α :=
   { elems := univ.bUnion (λ (y : β), (f ⁻¹' {y}).to_finset),
@@ -2132,11 +2154,8 @@ begin
   exact key.false,
 end
 
-lemma not_surjective_fintype_infinite [fintype α] [infinite β] (f : α → β) :
-  ¬ surjective f :=
-assume (hf : surjective f),
-have H : infinite α := infinite.of_surjective f hf,
-by exactI not_fintype α
+lemma not_surjective_finite_infinite [finite α] [infinite β] (f : α → β) : ¬ surjective f :=
+λ hf, (infinite.of_surjective f hf).not_finite ‹_›
 
 section trunc
 
@@ -2218,7 +2237,7 @@ end
 /-- An induction principle for finite types, analogous to `nat.rec`. It effectively says
 that every `fintype` is either `empty` or `option α`, up to an `equiv`. -/
 @[elab_as_eliminator]
-lemma induction_empty_option' {P : Π (α : Type u) [fintype α], Prop}
+lemma induction_empty_option {P : Π (α : Type u) [fintype α], Prop}
   (of_equiv : ∀ α β [fintype β] (e : α ≃ β), @P α (@fintype.of_equiv α β ‹_› e.symm) → @P β ‹_›)
   (h_empty : P pempty)
   (h_option : ∀ α [fintype α], by exactI P α → P (option α))
@@ -2231,20 +2250,21 @@ begin
   { rintro α hα - Pα hα', resetI, convert h_option α (Pα _) }
 end
 
+end fintype
+
 /-- An induction principle for finite types, analogous to `nat.rec`. It effectively says
 that every `fintype` is either `empty` or `option α`, up to an `equiv`. -/
-lemma induction_empty_option {P : Type u → Prop}
+lemma finite.induction_empty_option {P : Type u → Prop}
   (of_equiv : ∀ {α β}, α ≃ β → P α → P β)
   (h_empty : P pempty)
   (h_option : ∀ {α} [fintype α], P α → P (option α))
-  (α : Type u) [fintype α] : P α :=
+  (α : Type u) [finite α] : P α :=
 begin
-  refine induction_empty_option' _ _ _ α,
+  casesI nonempty_fintype α,
+  refine fintype.induction_empty_option _ _ _ α,
   exacts [λ α β _, of_equiv, h_empty, @h_option]
 end
 
-end fintype
-
 /-- Auxiliary definition to show `exists_seq_of_forall_finset_exists`. -/
 noncomputable def seq_of_forall_finset_exists_aux
   {α : Type*} [decidable_eq α] (P : α → Prop) (r : α → α → Prop)
diff --git a/src/data/fintype/card_embedding.lean b/src/data/fintype/card_embedding.lean
index 4b8b24fcdc02e..f5f3a810df06b 100644
--- a/src/data/fintype/card_embedding.lean
+++ b/src/data/fintype/card_embedding.lean
@@ -29,7 +29,7 @@ lemma card_embedding_eq_of_unique {α β : Type*} [unique α] [fintype β] [fint
   ‖α ↪ β‖ = (‖β‖.desc_factorial ‖α‖) :=
 begin
   classical,
-  unfreezingI { induction ‹fintype α› using fintype.induction_empty_option'
+  unfreezingI { induction ‹fintype α› using fintype.induction_empty_option
     with α₁ α₂ h₂ e ih α h ih },
   { letI := fintype.of_equiv _ e.symm,
     rw [← card_congr (equiv.embedding_congr e (equiv.refl β)), ih, card_congr e] },
diff --git a/src/data/set_like/fintype.lean b/src/data/set_like/fintype.lean
index 1909ca5648ff7..92783be767416 100644
--- a/src/data/set_like/fintype.lean
+++ b/src/data/set_like/fintype.lean
@@ -20,4 +20,8 @@ set_like objects. If we add those instances, we should remove this one. -/
 noncomputable instance {A B : Type*} [fintype B] [set_like A B] : fintype A :=
 fintype.of_injective coe set_like.coe_injective
 
+@[nolint dangerous_instance, priority 100] -- See note [lower instance priority]
+instance {A B : Type*} [finite B] [set_like A B] : finite A :=
+finite.of_injective coe set_like.coe_injective
+
 end set_like
diff --git a/src/data/zmod/defs.lean b/src/data/zmod/defs.lean
index 320127f005773..92a5c05f6814c 100644
--- a/src/data/zmod/defs.lean
+++ b/src/data/zmod/defs.lean
@@ -91,7 +91,7 @@ int.infinite
 @[simp] lemma card (n : ℕ) [fintype (zmod n)] : fintype.card (zmod n) = n :=
 begin
   casesI n,
-  { exact (not_fintype (zmod 0)).elim },
+  { exact (not_finite (zmod 0)).elim },
   { convert fintype.card_fin (n+1) }
 end
 
diff --git a/src/field_theory/finite/basic.lean b/src/field_theory/finite/basic.lean
index 8a18cebbeec11..783b64567d4ae 100644
--- a/src/field_theory/finite/basic.lean
+++ b/src/field_theory/finite/basic.lean
@@ -535,7 +535,7 @@ begin
     split,
     { simp only [sq, one_pow, neg_one_sq], },
     { exact ring.neg_one_ne_one_of_char_ne_two hF, }, },
-  have h₁ := mt (fintype.injective_iff_surjective.mpr) h, -- sq not surjective
+  have h₁ := mt (finite.injective_iff_surjective.mpr) h, -- sq not surjective
   push_neg at h₁,
   cases h₁ with a h₁,
   use a,
diff --git a/src/group_theory/commutator.lean b/src/group_theory/commutator.lean
index c738ac771c4b2..c8f5200998a4a 100644
--- a/src/group_theory/commutator.lean
+++ b/src/group_theory/commutator.lean
@@ -174,7 +174,7 @@ end
 
 /-- The commutator of direct product is contained in the direct product of the commutators.
 
-See `commutator_pi_pi_of_fintype` for equality given `fintype η`.
+See `commutator_pi_pi_of_finite` for equality given `fintype η`.
 -/
 lemma commutator_pi_pi_le {η : Type*} {Gs : η → Type*} [∀ i, group (Gs i)]
   (H K : Π i, subgroup (Gs i)) :
@@ -183,7 +183,7 @@ commutator_le.mpr $ λ p hp q hq i hi, commutator_mem_commutator (hp i hi) (hq i
 
 /-- The commutator of a finite direct product is contained in the direct product of the commutators.
 -/
-lemma commutator_pi_pi_of_fintype {η : Type*} [fintype η] {Gs : η → Type*}
+lemma commutator_pi_pi_of_finite {η : Type*} [finite η] {Gs : η → Type*}
   [∀ i, group (Gs i)] (H K : Π i, subgroup (Gs i)) :
   ⁅subgroup.pi set.univ H, subgroup.pi set.univ K⁆ = subgroup.pi set.univ (λ i, ⁅H i, K i⁆) :=
 begin
diff --git a/src/group_theory/exponent.lean b/src/group_theory/exponent.lean
index 6761d0c2f95cc..b7a8183ec2526 100644
--- a/src/group_theory/exponent.lean
+++ b/src/group_theory/exponent.lean
@@ -235,8 +235,9 @@ section left_cancel_monoid
 variable [left_cancel_monoid G]
 
 @[to_additive]
-lemma exponent_ne_zero_of_fintype [fintype G] : exponent G ≠ 0 :=
-by simpa [←lcm_order_eq_exponent, finset.lcm_eq_zero_iff] using λ x, (order_of_pos x).ne'
+lemma exponent_ne_zero_of_finite [finite G] : exponent G ≠ 0 :=
+by { casesI nonempty_fintype G,
+  simpa [←lcm_order_eq_exponent, finset.lcm_eq_zero_iff] using λ x, (order_of_pos x).ne' }
 
 end left_cancel_monoid
 
diff --git a/src/group_theory/finite_abelian.lean b/src/group_theory/finite_abelian.lean
index f2408e8ba4162..4f0a5364c0624 100644
--- a/src/group_theory/finite_abelian.lean
+++ b/src/group_theory/finite_abelian.lean
@@ -64,10 +64,11 @@ end
 
 /-- **Structure theorem of finite abelian groups** : Any finite abelian group is a direct sum of
 some `zmod (p i ^ e i)` for some prime powers `p i ^ e i`. -/
-theorem equiv_direct_sum_zmod_of_fintype [fintype G] :
+theorem equiv_direct_sum_zmod_of_fintype [finite G] :
   ∃ (ι : Type) [fintype ι] (p : ι → ℕ) [∀ i, nat.prime $ p i] (e : ι → ℕ),
   nonempty $ G ≃+ ⨁ (i : ι), zmod (p i ^ e i) :=
 begin
+  casesI nonempty_fintype G,
   obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ := equiv_free_prod_direct_sum_zmod G,
   cases n,
   { exact ⟨ι, fι, p, hp, e, ⟨f.trans add_equiv.unique_prod⟩⟩ },
diff --git a/src/group_theory/finiteness.lean b/src/group_theory/finiteness.lean
index b8ffc51bd0564..e75ebff295765 100644
--- a/src/group_theory/finiteness.lean
+++ b/src/group_theory/finiteness.lean
@@ -102,8 +102,9 @@ instance monoid.fg_of_add_monoid_fg [add_monoid.fg N] : monoid.fg (multiplicativ
 add_monoid.fg_iff_mul_fg.1 ‹_›
 
 @[to_additive, priority 100]
-instance monoid.fg_of_fintype [fintype M] : monoid.fg M :=
-⟨⟨finset.univ, by rw finset.coe_univ; exact submonoid.closure_univ⟩⟩
+instance monoid.fg_of_finite [finite M] : monoid.fg M :=
+by { casesI nonempty_fintype M,
+  exact ⟨⟨finset.univ, by rw finset.coe_univ; exact submonoid.closure_univ⟩⟩ }
 
 end monoid
 
@@ -264,8 +265,9 @@ instance group.fg_of_mul_group_fg [add_group.fg H] : group.fg (multiplicative H)
 add_group.fg_iff_mul_fg.1 ‹_›
 
 @[to_additive, priority 100]
-instance group.fg_of_fintype [fintype G] : group.fg G :=
-⟨⟨finset.univ, by rw finset.coe_univ; exact subgroup.closure_univ⟩⟩
+instance group.fg_of_finite [finite G] : group.fg G :=
+by { casesI nonempty_fintype G,
+  exact ⟨⟨finset.univ, by rw finset.coe_univ; exact subgroup.closure_univ⟩⟩ }
 
 @[to_additive]
 lemma group.fg_of_surjective {G' : Type*} [group G'] [hG : group.fg G] {f : G →* G'}
diff --git a/src/group_theory/group_action/basic.lean b/src/group_theory/group_action/basic.lean
index 5948759be8e00..4a536bbd7f335 100644
--- a/src/group_theory/group_action/basic.lean
+++ b/src/group_theory/group_action/basic.lean
@@ -187,10 +187,11 @@ def orbit_rel : setoid β :=
 local attribute [instance] orbit_rel
 
 variables {α} {β}
+
 /-- When you take a set `U` in `β`, push it down to the quotient, and pull back, you get the union
-of the orbit of `U` under `α`.
--/
-@[to_additive] lemma quotient_preimage_image_eq_union_mul (U : set β) :
+of the orbit of `U` under `α`. -/
+@[to_additive "When you take a set `U` in `β`, push it down to the quotient, and pull back, you get
+the union of the orbit of `U` under `α`."] lemma quotient_preimage_image_eq_union_mul (U : set β) :
   quotient.mk ⁻¹' (quotient.mk '' U) = ⋃ a : α, ((•) a) '' U :=
 begin
   set f : β → quotient (mul_action.orbit_rel α β) := quotient.mk,
diff --git a/src/group_theory/group_action/group.lean b/src/group_theory/group_action/group.lean
index ab1d85d8eddaf..e09d120823255 100644
--- a/src/group_theory/group_action/group.lean
+++ b/src/group_theory/group_action/group.lean
@@ -40,7 +40,8 @@ by rw [smul_smul, mul_right_inv, one_smul]
 add_decl_doc add_action.to_perm
 
 /-- `mul_action.to_perm` is injective on faithful actions. -/
-@[to_additive] lemma mul_action.to_perm_injective [has_faithful_smul α β] :
+@[to_additive "`add_action.to_perm` is injective on faithful actions."]
+lemma mul_action.to_perm_injective [has_faithful_smul α β] :
   function.injective (mul_action.to_perm : α → equiv.perm β) :=
 (show function.injective (equiv.to_fun ∘ mul_action.to_perm), from smul_left_injective').of_comp
 
diff --git a/src/group_theory/group_action/opposite.lean b/src/group_theory/group_action/opposite.lean
index 65111b5354aed..cd5674bf9bd1e 100644
--- a/src/group_theory/group_action/opposite.lean
+++ b/src/group_theory/group_action/opposite.lean
@@ -42,6 +42,7 @@ instance (R : Type*) [monoid R] [monoid α] [mul_distrib_mul_action R α] :
   smul_one := λ r, unop_injective $ smul_one r,
   .. mul_opposite.mul_action α R }
 
+@[to_additive]
 instance {M N} [has_smul M N] [has_smul M α] [has_smul N α] [is_scalar_tower M N α] :
   is_scalar_tower M N αᵐᵒᵖ :=
 ⟨λ x y z, unop_injective $ smul_assoc _ _ _⟩
@@ -76,8 +77,10 @@ open mul_opposite
 /-- Like `has_mul.to_has_smul`, but multiplies on the right.
 
 See also `monoid.to_opposite_mul_action` and `monoid_with_zero.to_opposite_mul_action_with_zero`. -/
-@[to_additive] instance has_mul.to_has_opposite_smul [has_mul α] : has_smul αᵐᵒᵖ α :=
-{ smul := λ c x, x * c.unop }
+@[to_additive "Like `has_add.to_has_vadd`, but adds on the right.
+
+See also `add_monoid.to_opposite_add_action`."]
+instance has_mul.to_has_opposite_smul [has_mul α] : has_smul αᵐᵒᵖ α := ⟨λ c x, x * c.unop⟩
 
 @[to_additive] lemma op_smul_eq_mul [has_mul α] {a a' : α} : op a • a' = a' * a := rfl
 
@@ -102,18 +105,19 @@ instance comm_semigroup.is_central_scalar [comm_semigroup α] : is_central_scala
 ⟨λ r m, mul_comm _ _⟩
 
 /-- Like `monoid.to_mul_action`, but multiplies on the right. -/
-@[to_additive] instance monoid.to_opposite_mul_action [monoid α] : mul_action αᵐᵒᵖ α :=
+@[to_additive "Like `add_monoid.to_add_action`, but adds on the right."]
+instance monoid.to_opposite_mul_action [monoid α] : mul_action αᵐᵒᵖ α :=
 { smul := (•),
   one_smul := mul_one,
   mul_smul := λ x y r, (mul_assoc _ _ _).symm }
 
-instance is_scalar_tower.opposite_mid {M N} [has_mul N] [has_smul M N]
-  [smul_comm_class M N N] :
+@[to_additive]
+instance is_scalar_tower.opposite_mid {M N} [has_mul N] [has_smul M N] [smul_comm_class M N N] :
   is_scalar_tower M Nᵐᵒᵖ N :=
 ⟨λ x y z, mul_smul_comm _ _ _⟩
 
-instance smul_comm_class.opposite_mid {M N} [has_mul N] [has_smul M N]
-  [is_scalar_tower M N N] :
+@[to_additive]
+instance smul_comm_class.opposite_mid {M N} [has_mul N] [has_smul M N] [is_scalar_tower M N N] :
   smul_comm_class M Nᵐᵒᵖ N :=
 ⟨λ x y z, by { induction y using mul_opposite.rec, simp [smul_mul_assoc] }⟩
 
@@ -122,7 +126,8 @@ instance smul_comm_class.opposite_mid {M N} [has_mul N] [has_smul M N]
 example [monoid α] : monoid.to_mul_action αᵐᵒᵖ = mul_opposite.mul_action α αᵐᵒᵖ := rfl
 
 /-- `monoid.to_opposite_mul_action` is faithful on cancellative monoids. -/
-@[to_additive] instance left_cancel_monoid.to_has_faithful_opposite_scalar [left_cancel_monoid α] :
+@[to_additive "`add_monoid.to_opposite_add_action` is faithful on cancellative monoids."]
+instance left_cancel_monoid.to_has_faithful_opposite_scalar [left_cancel_monoid α] :
   has_faithful_smul αᵐᵒᵖ α :=
 ⟨λ x y h, unop_injective $ mul_left_cancel (h 1)⟩
 
diff --git a/src/group_theory/group_action/pi.lean b/src/group_theory/group_action/pi.lean
index 0686e87d3466e..09a98569c6953 100644
--- a/src/group_theory/group_action/pi.lean
+++ b/src/group_theory/group_action/pi.lean
@@ -74,7 +74,8 @@ instance {α : Type*} [Π i, has_smul α $ f i] [Π i, has_smul αᵐᵒᵖ $ f
 
 /-- If `f i` has a faithful scalar action for a given `i`, then so does `Π i, f i`. This is
 not an instance as `i` cannot be inferred. -/
-@[to_additive pi.has_faithful_vadd_at]
+@[to_additive pi.has_faithful_vadd_at "If `f i` has a faithful additive action for a given `i`, then
+so does `Π i, f i`. This is not an instance as `i` cannot be inferred"]
 lemma has_faithful_smul_at {α : Type*}
   [Π i, has_smul α $ f i] [Π i, nonempty (f i)] (i : I) [has_faithful_smul α (f i)] :
   has_faithful_smul α (Π i, f i) :=
@@ -153,14 +154,16 @@ namespace function
 
 /-- Non-dependent version of `pi.has_smul`. Lean gets confused by the dependent instance if this
 is not present. -/
-@[to_additive]
+@[to_additive "Non-dependent version of `pi.has_vadd`. Lean gets confused by the dependent instance
+if this is not present."]
 instance has_smul {ι R M : Type*} [has_smul R M] :
   has_smul R (ι → M) :=
 pi.has_smul
 
 /-- Non-dependent version of `pi.smul_comm_class`. Lean gets confused by the dependent instance if
 this is not present. -/
-@[to_additive]
+@[to_additive "Non-dependent version of `pi.vadd_comm_class`. Lean gets confused by the dependent
+instance if this is not present."]
 instance smul_comm_class {ι α β M : Type*}
   [has_smul α M] [has_smul β M] [smul_comm_class α β M] :
   smul_comm_class α β (ι → M) :=
diff --git a/src/group_theory/index.lean b/src/group_theory/index.lean
index c83b097b10af7..6d1281e746d6c 100644
--- a/src/group_theory/index.lean
+++ b/src/group_theory/index.lean
@@ -259,8 +259,8 @@ by simp_rw [←relindex_top_right, relindex_inf_le]
 ⟨λ h, quotient_group.subgroup_eq_top_of_subsingleton H (cardinal.to_nat_eq_one_iff_unique.mp h).1,
   λ h, (congr_arg index h).trans index_top⟩
 
-@[to_additive] lemma index_ne_zero_of_fintype [hH : fintype (G ⧸ H)] : H.index ≠ 0 :=
-by { rw index_eq_card, exact fintype.card_ne_zero }
+@[to_additive] lemma index_ne_zero_of_finite [hH : finite (G ⧸ H)] : H.index ≠ 0 :=
+by { casesI nonempty_fintype (G ⧸ H), rw index_eq_card, exact fintype.card_ne_zero }
 
 /-- Finite index implies finite quotient. -/
 @[to_additive "Finite index implies finite quotient."]
@@ -268,7 +268,7 @@ noncomputable def fintype_of_index_ne_zero (hH : H.index ≠ 0) : fintype (G ⧸
 (cardinal.lt_aleph_0_iff_fintype.mp (lt_of_not_ge (mt cardinal.to_nat_apply_of_aleph_0_le hH))).some
 
 @[to_additive one_lt_index_of_ne_top]
-lemma one_lt_index_of_ne_top [fintype (G ⧸ H)] (hH : H ≠ ⊤) : 1 < H.index :=
-nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨index_ne_zero_of_fintype, mt index_eq_one.mp hH⟩
+lemma one_lt_index_of_ne_top [finite (G ⧸ H)] (hH : H ≠ ⊤) : 1 < H.index :=
+nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨index_ne_zero_of_finite, mt index_eq_one.mp hH⟩
 
 end subgroup
diff --git a/src/group_theory/nilpotent.lean b/src/group_theory/nilpotent.lean
index d0c3a3505702a..3acfd6222da00 100644
--- a/src/group_theory/nilpotent.lean
+++ b/src/group_theory/nilpotent.lean
@@ -774,9 +774,9 @@ section finite_pi
 
 -- Now for finite products
 
-variables {η : Type*} [fintype η] {Gs : η → Type*} [∀ i, group (Gs i)]
+variables {η : Type*} {Gs : η → Type*} [∀ i, group (Gs i)]
 
-lemma lower_central_series_pi_of_fintype (n : ℕ):
+lemma lower_central_series_pi_of_finite [finite η] (n : ℕ) :
   lower_central_series (Π i, Gs i) n = subgroup.pi set.univ (λ i, lower_central_series (Gs i) n) :=
 begin
   let pi := λ (f : Π i, subgroup (Gs i)), subgroup.pi set.univ f,
@@ -786,17 +786,17 @@ begin
         = ⁅lower_central_series (Π i, Gs i) n, ⊤⁆          : rfl
     ... = ⁅pi (λ i, (lower_central_series (Gs i) n)), ⊤⁆   : by rw ih
     ... = ⁅pi (λ i, (lower_central_series (Gs i) n)), pi (λ i, ⊤)⁆ : by simp [pi, pi_top]
-    ... = pi (λ i, ⁅(lower_central_series (Gs i) n), ⊤⁆)   : commutator_pi_pi_of_fintype _ _
+    ... = pi (λ i, ⁅(lower_central_series (Gs i) n), ⊤⁆)   : commutator_pi_pi_of_finite _ _
     ... = pi (λ i, lower_central_series (Gs i) n.succ)     : rfl }
 end
 
 /-- n-ary products of nilpotent groups are nilpotent -/
-instance is_nilpotent_pi [∀ i, is_nilpotent (Gs i)] :
-  is_nilpotent (Π i, Gs i) :=
+instance is_nilpotent_pi [finite η] [∀ i, is_nilpotent (Gs i)] : is_nilpotent (Π i, Gs i) :=
 begin
+  casesI nonempty_fintype η,
   rw nilpotent_iff_lower_central_series,
   refine ⟨finset.univ.sup (λ i, group.nilpotency_class (Gs i)), _⟩,
-  rw [lower_central_series_pi_of_fintype, pi_eq_bot_iff],
+  rw [lower_central_series_pi_of_finite, pi_eq_bot_iff],
   intros i,
   apply lower_central_series_eq_bot_iff_nilpotency_class_le.mpr,
   exact @finset.le_sup _ _ _ _ finset.univ (λ i, group.nilpotency_class (Gs i)) _
@@ -804,13 +804,13 @@ begin
 end
 
 /-- The nilpotency class of an n-ary product is the sup of the nilpotency classes of the factors -/
-lemma nilpotency_class_pi [∀ i, is_nilpotent (Gs i)] :
+lemma nilpotency_class_pi [fintype η] [∀ i, is_nilpotent (Gs i)] :
   group.nilpotency_class (Π i, Gs i) = finset.univ.sup (λ i, group.nilpotency_class (Gs i)) :=
 begin
   apply eq_of_forall_ge_iff,
   intros k,
   simp only [finset.sup_le_iff, ← lower_central_series_eq_bot_iff_nilpotency_class_le,
-    lower_central_series_pi_of_fintype, pi_eq_bot_iff, finset.mem_univ, true_implies_iff ],
+    lower_central_series_pi_of_finite, pi_eq_bot_iff, finset.mem_univ, true_implies_iff ],
 end
 
 end finite_pi
@@ -852,17 +852,18 @@ section with_finite_group
 
 open group fintype
 
-variables {G : Type*} [hG : group G] [hf : fintype G]
-include hG hf
+variables {G : Type*} [hG : group G]
+include hG
 
 /-- A p-group is nilpotent -/
-lemma is_p_group.is_nilpotent {p : ℕ} [hp : fact (nat.prime p)] (h : is_p_group p G) :
+lemma is_p_group.is_nilpotent [finite G] {p : ℕ} [hp : fact (nat.prime p)] (h : is_p_group p G) :
   is_nilpotent G :=
 begin
+  casesI nonempty_fintype G,
   classical,
   unfreezingI
   { revert hG,
-    induction hf using fintype.induction_subsingleton_or_nontrivial with G hG hS G hG hN ih },
+    induction val using fintype.induction_subsingleton_or_nontrivial with G hG hS G hG hN ih },
   { apply_instance, },
   { introI _, intro h,
     have hcq : fintype.card (G ⧸ center G) < fintype.card G,
@@ -874,6 +875,8 @@ begin
     exact (of_quotient_center_nilpotent hnq), }
 end
 
+variables [fintype G]
+
 /-- If a finite group is the direct product of its Sylow groups, it is nilpotent -/
 theorem is_nilpotent_of_product_of_sylow_group
   (e : (Π p : (fintype.card G).factorization.support, Π P : sylow p G, (↑P : subgroup G)) ≃* G) :
diff --git a/src/group_theory/noncomm_pi_coprod.lean b/src/group_theory/noncomm_pi_coprod.lean
index 5dd7f2871e239..fdac562bc6549 100644
--- a/src/group_theory/noncomm_pi_coprod.lean
+++ b/src/group_theory/noncomm_pi_coprod.lean
@@ -185,11 +185,14 @@ end
 
 variable (hcomm)
 
+omit hfin
+
 @[to_additive]
-lemma independent_range_of_coprime_order [∀ i, fintype (H i)]
+lemma independent_range_of_coprime_order [finite ι] [Π i, fintype (H i)]
   (hcoprime : ∀ i j, i ≠ j → nat.coprime (fintype.card (H i)) (fintype.card (H j))) :
   complete_lattice.independent (λ i, (ϕ i).range) :=
 begin
+  casesI nonempty_fintype ι,
   classical,
   rintros i f ⟨hxi, hxp⟩, dsimp at hxi hxp,
   rw [supr_subtype', ← noncomm_pi_coprod_range] at hxp,
@@ -263,14 +266,14 @@ end
 
 variable (hcomm)
 
+omit hfin
+
 @[to_additive]
-lemma independent_of_coprime_order [∀ i, fintype (H i)]
+lemma independent_of_coprime_order [finite ι] [∀ i, fintype (H i)]
   (hcoprime : ∀ i j, i ≠ j → nat.coprime (fintype.card (H i)) (fintype.card (H j))) :
   complete_lattice.independent H :=
-begin
-  simpa using monoid_hom.independent_range_of_coprime_order
-    (λ i, (H i).subtype) (commute_subtype_of_commute hcomm) hcoprime,
-end
+by simpa using monoid_hom.independent_range_of_coprime_order (λ i, (H i).subtype)
+  (commute_subtype_of_commute hcomm) hcoprime
 
 end commuting_subgroups
 
diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean
index 32b543e312ecf..03e51ce62749d 100644
--- a/src/group_theory/order_of_element.lean
+++ b/src/group_theory/order_of_element.lean
@@ -69,7 +69,8 @@ lemma is_of_fin_order_iff_pow_eq_one (x : G) :
 by { convert iff.rfl, simp [is_periodic_pt_mul_iff_pow_eq_one] }
 
 /-- Elements of finite order are of finite order in submonoids.-/
-@[to_additive is_of_fin_add_order_iff_coe]
+@[to_additive is_of_fin_add_order_iff_coe "Elements of finite order are of finite order in
+submonoids."]
 lemma is_of_fin_order_iff_coe (H : submonoid G) (x : H) :
   is_of_fin_order x ↔ is_of_fin_order (x : G) :=
 by { rw [is_of_fin_order_iff_pow_eq_one, is_of_fin_order_iff_pow_eq_one], norm_cast }
@@ -192,11 +193,10 @@ begin
   exact ⟨m, by rw [←pow_mul, pow_eq_mod_order_of, hm, pow_one]⟩,
 end
 
-/--
-If `x^n = 1`, but `x^(n/p) ≠ 1` for all prime factors `p` of `r`,
-then `x` has order `n` in `G`.
+/-- If `x^n = 1`, but `x^(n/p) ≠ 1` for all prime factors `p` of `n`, then `x` has order `n` in `G`.
 -/
-@[to_additive add_order_of_eq_of_nsmul_and_div_prime_nsmul]
+@[to_additive add_order_of_eq_of_nsmul_and_div_prime_nsmul "If `n * x = 0`, but `n/p * x ≠ 0` for
+all prime factors `p` of `n`, then `x` has order `n` in `G`."]
 theorem order_of_eq_of_pow_and_pow_div_prime (hn : 0 < n) (hx : x^n = 1)
   (hd : ∀ p : ℕ, p.prime → p ∣ n → x^(n/p) ≠ 1) :
   order_of x = n :=
@@ -428,15 +428,12 @@ lemma is_of_fin_order.mul (hx : is_of_fin_order x) (hy : is_of_fin_order y) :
 
 end comm_monoid
 
-section fintype
-variables [fintype G] [fintype A]
-
 section finite_monoid
-variables [monoid G] [add_monoid A]
+variables [monoid G]
 open_locale big_operators
 
 @[to_additive sum_card_add_order_of_eq_card_nsmul_eq_zero]
-lemma sum_card_order_of_eq_card_pow_eq_one [decidable_eq G] (hn : 0 < n) :
+lemma sum_card_order_of_eq_card_pow_eq_one [fintype G] [decidable_eq G] (hn : 0 < n) :
   ∑ m in (finset.range n.succ).filter (∣ n), (finset.univ.filter (λ x : G, order_of x = m)).card
   = (finset.univ.filter (λ x : G, x ^ n = 1)).card :=
 calc ∑ m in (finset.range n.succ).filter (∣ n), (finset.univ.filter (λ x : G, order_of x = m)).card
@@ -457,19 +454,19 @@ variables [left_cancel_monoid G] [add_left_cancel_monoid A]
 
 -- TODO: Use this to show that a finite left cancellative monoid is a group.
 @[to_additive]
-lemma exists_pow_eq_one (x : G) : is_of_fin_order x :=
+lemma exists_pow_eq_one [finite G] (x : G) : is_of_fin_order x :=
 begin
   refine (is_of_fin_order_iff_pow_eq_one _).mpr _,
   obtain ⟨i, j, a_eq, ne⟩ : ∃(i j : ℕ), x ^ i = x ^ j ∧ i ≠ j :=
     by simpa only [not_forall, exists_prop, injective]
-      using (not_injective_infinite_fintype (λi:ℕ, x^i)),
+      using (not_injective_infinite_finite (λi:ℕ, x^i)),
   wlog h'' : j ≤ i,
   refine ⟨i - j, tsub_pos_of_lt (lt_of_le_of_ne h'' ne.symm), mul_right_injective (x^j) _⟩,
   rw [mul_one, ← pow_add, ← a_eq, add_tsub_cancel_of_le h''],
 end
 
 @[to_additive add_order_of_le_card_univ]
-lemma order_of_le_card_univ : order_of x ≤ fintype.card G :=
+lemma order_of_le_card_univ [fintype G] : order_of x ≤ fintype.card G :=
 finset.le_card_of_inj_on_range ((^) x)
   (assume n _, finset.mem_univ _)
   (assume i hi j hj, pow_injective_of_lt_order_of x hi hj)
@@ -479,7 +476,7 @@ finset.le_card_of_inj_on_range ((^) x)
 @[to_additive add_order_of_pos
 "This is the same as `add_order_of_pos' but with one fewer explicit assumption since this is
   automatic in case of a finite cancellative additive monoid."]
-lemma order_of_pos (x : G) : 0 < order_of x := order_of_pos' (exists_pow_eq_one x)
+lemma order_of_pos [finite G] (x : G) : 0 < order_of x := order_of_pos' (exists_pow_eq_one x)
 
 open nat
 
@@ -488,40 +485,34 @@ automatic in the case of a finite cancellative monoid.-/
 @[to_additive add_order_of_nsmul
 "This is the same as `add_order_of_nsmul'` and `add_order_of_nsmul` but with one assumption less
 which is automatic in the case of a finite cancellative additive monoid."]
-lemma order_of_pow (x : G) :
+lemma order_of_pow [finite G] (x : G) :
   order_of (x ^ n) = order_of x / gcd (order_of x) n := order_of_pow'' _ _ (exists_pow_eq_one _)
 
 @[to_additive mem_multiples_iff_mem_range_add_order_of]
-lemma mem_powers_iff_mem_range_order_of [decidable_eq G] :
+lemma mem_powers_iff_mem_range_order_of [finite G] [decidable_eq G] :
   y ∈ submonoid.powers x ↔ y ∈ (finset.range (order_of x)).image ((^) x : ℕ → G) :=
 finset.mem_range_iff_mem_finset_range_of_mod_eq' (order_of_pos x)
   (assume i, pow_eq_mod_order_of.symm)
 
 @[to_additive decidable_multiples]
-noncomputable instance decidable_powers [decidable_eq G] :
-  decidable_pred (∈ submonoid.powers x) :=
-begin
-  assume y,
-  apply decidable_of_iff'
-    (y ∈ (finset.range (order_of x)).image ((^) x)),
-  exact mem_powers_iff_mem_range_order_of
-end
+noncomputable instance decidable_powers : decidable_pred (∈ submonoid.powers x) :=
+classical.dec_pred _
 
 /--The equivalence between `fin (order_of x)` and `submonoid.powers x`, sending `i` to `x ^ i`."-/
 @[to_additive fin_equiv_multiples "The equivalence between `fin (add_order_of a)` and
 `add_submonoid.multiples a`, sending `i` to `i • a`."]
-noncomputable def fin_equiv_powers (x : G) :
+noncomputable def fin_equiv_powers [finite G] (x : G) :
   fin (order_of x) ≃ (submonoid.powers x : set G) :=
 equiv.of_bijective (λ n, ⟨x ^ ↑n, ⟨n, rfl⟩⟩) ⟨λ ⟨i, hi⟩ ⟨j, hj⟩ ij,
   subtype.mk_eq_mk.2 (pow_injective_of_lt_order_of x hi hj (subtype.mk_eq_mk.1 ij)),
   λ ⟨_, i, rfl⟩, ⟨⟨i % order_of x, mod_lt i (order_of_pos x)⟩, subtype.eq pow_eq_mod_order_of.symm⟩⟩
 
 @[simp, to_additive fin_equiv_multiples_apply]
-lemma fin_equiv_powers_apply {x : G} {n : fin (order_of x)} :
+lemma fin_equiv_powers_apply [finite G] {x : G} {n : fin (order_of x)} :
   fin_equiv_powers x n = ⟨x ^ ↑n, n, rfl⟩ := rfl
 
 @[simp, to_additive fin_equiv_multiples_symm_apply]
-lemma fin_equiv_powers_symm_apply (x : G) (n : ℕ)
+lemma fin_equiv_powers_symm_apply [finite G] (x : G) (n : ℕ)
   {hn : ∃ (m : ℕ), x ^ m = x ^ n} :
   ((fin_equiv_powers x).symm ⟨x ^ n, hn⟩) = ⟨n % order_of x, nat.mod_lt _ (order_of_pos x)⟩ :=
 by rw [equiv.symm_apply_eq, fin_equiv_powers_apply, subtype.mk_eq_mk,
@@ -532,12 +523,12 @@ by rw [equiv.symm_apply_eq, fin_equiv_powers_apply, subtype.mk_eq_mk,
 @[to_additive multiples_equiv_multiples
 "The equivalence between `submonoid.multiples` of two elements `a, b` of the same additive order,
   mapping `i • a` to `i • b`."]
-noncomputable def powers_equiv_powers (h : order_of x = order_of y) :
+noncomputable def powers_equiv_powers [finite G] (h : order_of x = order_of y) :
   (submonoid.powers x : set G) ≃ (submonoid.powers y : set G) :=
 (fin_equiv_powers x).symm.trans ((fin.cast h).to_equiv.trans (fin_equiv_powers y))
 
 @[simp, to_additive multiples_equiv_multiples_apply]
-lemma powers_equiv_powers_apply (h : order_of x = order_of y)
+lemma powers_equiv_powers_apply [finite G] (h : order_of x = order_of y)
   (n : ℕ) : powers_equiv_powers h ⟨x ^ n, n, rfl⟩ = ⟨y ^ n, n, rfl⟩ :=
 begin
   rw [powers_equiv_powers, equiv.trans_apply, equiv.trans_apply,
@@ -546,8 +537,7 @@ begin
 end
 
 @[to_additive add_order_of_eq_card_multiples]
-lemma order_eq_card_powers [decidable_eq G] :
-  order_of x = fintype.card (submonoid.powers x : set G) :=
+lemma order_eq_card_powers [fintype G] : order_of x = fintype.card (submonoid.powers x : set G) :=
 (fintype.card_fin (order_of x)).symm.trans (fintype.card_eq.2 ⟨fin_equiv_powers x⟩)
 
 end finite_cancel_monoid
@@ -556,7 +546,7 @@ section finite_group
 variables [group G] [add_group A]
 
 @[to_additive]
-lemma exists_zpow_eq_one (x : G) : ∃ (i : ℤ) (H : i ≠ 0), x ^ (i : ℤ) = 1 :=
+lemma exists_zpow_eq_one [finite G] (x : G) : ∃ (i : ℤ) (H : i ≠ 0), x ^ (i : ℤ) = 1 :=
 begin
   rcases exists_pow_eq_one x with ⟨w, hw1, hw2⟩,
   refine ⟨w, int.coe_nat_ne_zero.mpr (ne_of_gt hw1), _⟩,
@@ -567,7 +557,7 @@ end
 open subgroup
 
 @[to_additive mem_multiples_iff_mem_zmultiples]
-lemma mem_powers_iff_mem_zpowers : y ∈ submonoid.powers x ↔ y ∈ zpowers x :=
+lemma mem_powers_iff_mem_zpowers [finite G] : y ∈ submonoid.powers x ↔ y ∈ zpowers x :=
 ⟨λ ⟨n, hn⟩, ⟨n, by simp * at *⟩,
 λ ⟨i, hi⟩, ⟨(i % order_of x).nat_abs,
   by rwa [← zpow_coe_nat, int.nat_abs_of_nonneg (int.mod_nonneg _
@@ -575,37 +565,32 @@ lemma mem_powers_iff_mem_zpowers : y ∈ submonoid.powers x ↔ y ∈ zpowers x
     ← zpow_eq_mod_order_of]⟩⟩
 
 @[to_additive multiples_eq_zmultiples]
-lemma powers_eq_zpowers (x : G) : (submonoid.powers x : set G) = zpowers x :=
+lemma powers_eq_zpowers [finite G] (x : G) : (submonoid.powers x : set G) = zpowers x :=
 set.ext $ λ x, mem_powers_iff_mem_zpowers
 
 @[to_additive mem_zmultiples_iff_mem_range_add_order_of]
-lemma mem_zpowers_iff_mem_range_order_of [decidable_eq G] :
+lemma mem_zpowers_iff_mem_range_order_of [finite G] [decidable_eq G] :
   y ∈ subgroup.zpowers x ↔ y ∈ (finset.range (order_of x)).image ((^) x : ℕ → G) :=
 by rw [← mem_powers_iff_mem_zpowers, mem_powers_iff_mem_range_order_of]
 
 @[to_additive decidable_zmultiples]
-noncomputable instance decidable_zpowers [decidable_eq G] :
-  decidable_pred (∈ subgroup.zpowers x) :=
-begin
-  simp_rw ←set_like.mem_coe,
-  rw ← powers_eq_zpowers,
-  exact decidable_powers,
-end
+noncomputable instance decidable_zpowers : decidable_pred (∈ subgroup.zpowers x) :=
+classical.dec_pred _
 
 /-- The equivalence between `fin (order_of x)` and `subgroup.zpowers x`, sending `i` to `x ^ i`. -/
 @[to_additive fin_equiv_zmultiples
 "The equivalence between `fin (add_order_of a)` and `subgroup.zmultiples a`, sending `i`
 to `i • a`."]
-noncomputable def fin_equiv_zpowers (x : G) :
+noncomputable def fin_equiv_zpowers [finite G] (x : G) :
   fin (order_of x) ≃ (subgroup.zpowers x : set G) :=
 (fin_equiv_powers x).trans (equiv.set.of_eq (powers_eq_zpowers x))
 
 @[simp, to_additive fin_equiv_zmultiples_apply]
-lemma fin_equiv_zpowers_apply {n : fin (order_of x)} :
+lemma fin_equiv_zpowers_apply [finite G] {n : fin (order_of x)} :
   fin_equiv_zpowers x n = ⟨x ^ (n : ℕ), n, zpow_coe_nat x n⟩ := rfl
 
 @[simp, to_additive fin_equiv_zmultiples_symm_apply]
-lemma fin_equiv_zpowers_symm_apply (x : G) (n : ℕ)
+lemma fin_equiv_zpowers_symm_apply [finite G] (x : G) (n : ℕ)
   {hn : ∃ (m : ℤ), x ^ m = x ^ n} :
   ((fin_equiv_zpowers x).symm ⟨x ^ n, hn⟩) = ⟨n % order_of x, nat.mod_lt _ (order_of_pos x)⟩ :=
 by { rw [fin_equiv_zpowers, equiv.symm_trans_apply, equiv.set.of_eq_symm_apply],
@@ -616,12 +601,12 @@ by { rw [fin_equiv_zpowers, equiv.symm_trans_apply, equiv.set.of_eq_symm_apply],
 @[to_additive zmultiples_equiv_zmultiples
 "The equivalence between `subgroup.zmultiples` of two elements `a, b` of the same additive order,
   mapping `i • a` to `i • b`."]
-noncomputable def zpowers_equiv_zpowers (h : order_of x = order_of y) :
+noncomputable def zpowers_equiv_zpowers [finite G] (h : order_of x = order_of y) :
   (subgroup.zpowers x : set G) ≃ (subgroup.zpowers y : set G) :=
 (fin_equiv_zpowers x).symm.trans ((fin.cast h).to_equiv.trans (fin_equiv_zpowers y))
 
 @[simp, to_additive zmultiples_equiv_zmultiples_apply]
-lemma zpowers_equiv_zpowers_apply (h : order_of x = order_of y)
+lemma zpowers_equiv_zpowers_apply [finite G] (h : order_of x = order_of y)
   (n : ℕ) : zpowers_equiv_zpowers h ⟨x ^ n, n, zpow_coe_nat x n⟩ = ⟨y ^ n, n, zpow_coe_nat y n⟩ :=
 begin
   rw [zpowers_equiv_zpowers, equiv.trans_apply, equiv.trans_apply,
@@ -629,8 +614,10 @@ begin
   simp [h]
 end
 
+variables [fintype G]
+
 @[to_additive add_order_eq_card_zmultiples]
-lemma order_eq_card_zpowers [decidable_eq G] : order_of x = fintype.card (zpowers x) :=
+lemma order_eq_card_zpowers : order_of x = fintype.card (zpowers x) :=
 (fintype.card_fin (order_of x)).symm.trans (fintype.card_eq.2 ⟨fin_equiv_zpowers x⟩)
 
 open quotient_group
@@ -660,13 +647,15 @@ begin
           (by rw [eq₁, eq₂, mul_comm])
 end
 
-@[simp, to_additive card_nsmul_eq_zero] lemma pow_card_eq_one : x ^ fintype.card G = 1 :=
+@[simp, to_additive card_nsmul_eq_zero]
+lemma pow_card_eq_one : x ^ fintype.card G = 1 :=
 let ⟨m, hm⟩ := @order_of_dvd_card_univ _ x _ _ in
 by simp [hm, pow_mul, pow_order_of_eq_one]
 
 @[to_additive] lemma subgroup.pow_index_mem {G : Type*} [group G] (H : subgroup G)
-  [fintype (G ⧸ H)] [normal H] (g : G) : g ^ index H ∈ H :=
-by rw [←eq_one_iff, quotient_group.coe_pow H, index_eq_card, pow_card_eq_one]
+  [finite (G ⧸ H)] [normal H] (g : G) : g ^ index H ∈ H :=
+by { casesI nonempty_fintype (G ⧸ H),
+  rw [←eq_one_iff, quotient_group.coe_pow H, index_eq_card, pow_card_eq_one] }
 
 @[to_additive] lemma pow_eq_mod_card (n : ℕ) :
   x ^ n = x ^ (n % fintype.card G) :=
@@ -711,13 +700,13 @@ end
 variable (a)
 
 /-- TODO: Generalise to `submonoid.powers`.-/
-@[to_additive image_range_add_order_of]
+@[to_additive image_range_add_order_of, nolint to_additive_doc]
 lemma image_range_order_of [decidable_eq G] :
   finset.image (λ i, x ^ i) (finset.range (order_of x)) = (zpowers x : set G).to_finset :=
 by { ext x, rw [set.mem_to_finset, set_like.mem_coe, mem_zpowers_iff_mem_range_order_of] }
 
-/-- TODO: Generalise to `finite_cancel_monoid`. -/
-@[to_additive gcd_nsmul_card_eq_zero_iff]
+/-- TODO: Generalise to `finite` + `cancel_monoid`. -/
+@[to_additive gcd_nsmul_card_eq_zero_iff "TODO: Generalise to `finite` + `cancel_add_monoid`"]
 lemma pow_gcd_card_eq_one_iff : x ^ n = 1 ↔ x ^ (gcd n (fintype.card G)) = 1 :=
 ⟨λ h, pow_gcd_eq_one _ h $ pow_card_eq_one,
   λ h, let ⟨m, hm⟩ := gcd_dvd_left n (fintype.card G) in
@@ -725,8 +714,6 @@ lemma pow_gcd_card_eq_one_iff : x ^ n = 1 ↔ x ^ (gcd n (fintype.card G)) = 1 :
 
 end finite_group
 
-end fintype
-
 section pow_is_subgroup
 
 /-- A nonempty idempotent subset of a finite cancellative monoid is a submonoid -/
diff --git a/src/group_theory/perm/cycle/basic.lean b/src/group_theory/perm/cycle/basic.lean
index 804eba5fc61eb..1e70027498abd 100644
--- a/src/group_theory/perm/cycle/basic.lean
+++ b/src/group_theory/perm/cycle/basic.lean
@@ -101,14 +101,14 @@ let ⟨a, ha⟩ := hg.2 x hx in
 let ⟨b, hb⟩ := hg.2 y hy in
 ⟨b - a, by rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]⟩
 
-lemma is_cycle.exists_pow_eq [fintype β] {f : perm β} (hf : is_cycle f) {x y : β}
+lemma is_cycle.exists_pow_eq [finite β] {f : perm β} (hf : is_cycle f) {x y : β}
   (hx : f x ≠ x) (hy : f y ≠ y) : ∃ i : ℕ, (f ^ i) x = y :=
 let ⟨n, hn⟩ := hf.exists_zpow_eq hx hy in
 by classical; exact ⟨(n % order_of f).to_nat, by
 { have := n.mod_nonneg (int.coe_nat_ne_zero.mpr (ne_of_gt (order_of_pos f))),
   rwa [← zpow_coe_nat, int.to_nat_of_nonneg this, ← zpow_eq_mod_order_of] }⟩
 
-lemma is_cycle.exists_pow_eq_one [fintype β] {f : perm β} (hf : is_cycle f) :
+lemma is_cycle.exists_pow_eq_one [finite β] {f : perm β} (hf : is_cycle f) :
   ∃ (k : ℕ) (hk : 1 < k), f ^ k = 1 :=
 begin
   classical,
@@ -339,7 +339,7 @@ lemma is_cycle.same_cycle {f : perm β} (hf : is_cycle f) {x y : β}
   (hx : f x ≠ x) (hy : f y ≠ y) : same_cycle f x y :=
 hf.exists_zpow_eq hx hy
 
-lemma same_cycle.nat' [fintype β] {f : perm β} {x y : β} (h : same_cycle f x y) :
+lemma same_cycle.nat' [finite β] {f : perm β} {x y : β} (h : same_cycle f x y) :
   ∃ (i : ℕ) (h : i < order_of f), (f ^ i) x = y :=
 begin
   classical,
@@ -353,7 +353,7 @@ begin
   exact int.mod_lt_of_pos _ h₀,
 end
 
-lemma same_cycle.nat'' [fintype β] {f : perm β} {x y : β} (h : same_cycle f x y) :
+lemma same_cycle.nat'' [finite β] {f : perm β} {x y : β} (h : same_cycle f x y) :
   ∃ (i : ℕ) (hpos : 0 < i) (h : i ≤ order_of f), (f ^ i) x = y :=
 begin
   classical,
@@ -369,13 +369,12 @@ instance [fintype α] (f : perm α) : decidable_rel (same_cycle f) :=
   (int.coe_nat_lt.1 $
     by { rw int.nat_abs_of_nonneg (int.mod_nonneg _
         (int.coe_nat_ne_zero_iff_pos.2 (order_of_pos _))),
-      { apply lt_of_lt_of_le (int.mod_lt _ (int.coe_nat_ne_zero_iff_pos.2 (order_of_pos _))),
-        { simp [order_of_le_card_univ] },
-        exact fintype_perm },
-      exact fintype_perm, }),
+      { refine (int.mod_lt _ $ int.coe_nat_ne_zero_iff_pos.2 $ order_of_pos _).trans_le _,
+        simp [order_of_le_card_univ] },
+      apply_instance }),
   by { rw [← zpow_coe_nat, int.nat_abs_of_nonneg (int.mod_nonneg _
       (int.coe_nat_ne_zero_iff_pos.2 (order_of_pos _))), ← zpow_eq_mod_order_of, hi],
-    exact fintype_perm }⟩⟩
+    apply_instance }⟩⟩
 
 lemma same_cycle_apply {f : perm β} {x y : β} : same_cycle f x (f y) ↔ same_cycle f x y :=
 ⟨λ ⟨i, hi⟩, ⟨-1 + i, by rw [zpow_add, mul_apply, hi, zpow_neg_one, inv_apply_self]⟩,
@@ -474,10 +473,11 @@ begin
       simpa using H } }
 end
 
-lemma is_cycle.pow_iff [fintype β] {f : perm β} (hf : is_cycle f) {n : ℕ} :
+lemma is_cycle.pow_iff [finite β] {f : perm β} (hf : is_cycle f) {n : ℕ} :
   is_cycle (f ^ n) ↔ n.coprime (order_of f) :=
 begin
   classical,
+  casesI nonempty_fintype β,
   split,
   { intro h,
     have hr : support (f ^ n) = support f,
@@ -500,10 +500,11 @@ begin
     exact support_pow_le _ n hx }
 end
 
-lemma is_cycle.pow_eq_one_iff [fintype β] {f : perm β} (hf : is_cycle f) {n : ℕ} :
+lemma is_cycle.pow_eq_one_iff [finite β] {f : perm β} (hf : is_cycle f) {n : ℕ} :
   f ^ n = 1 ↔ ∃ x, f x ≠ x ∧ (f ^ n) x = x :=
 begin
   classical,
+  casesI nonempty_fintype β,
   split,
   { intro h,
     obtain ⟨x, hx, -⟩ := id hf,
@@ -517,10 +518,11 @@ begin
       rw [pow_mul, pow_order_of_eq_one, one_pow] } }
 end
 
-lemma is_cycle.pow_eq_pow_iff [fintype β] {f : perm β} (hf : is_cycle f) {a b : ℕ} :
+lemma is_cycle.pow_eq_pow_iff [finite β] {f : perm β} (hf : is_cycle f) {a b : ℕ} :
   f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x :=
 begin
   classical,
+  casesI nonempty_fintype β,
   split,
   { intro h,
     obtain ⟨x, hx, -⟩ := id hf,
@@ -550,10 +552,11 @@ begin
   rw this
 end
 
-lemma is_cycle.is_cycle_pow_pos_of_lt_prime_order [fintype β] {f : perm β} (hf : is_cycle f)
+lemma is_cycle.is_cycle_pow_pos_of_lt_prime_order [finite β] {f : perm β} (hf : is_cycle f)
   (hf' : (order_of f).prime) (n : ℕ) (hn : 0 < n) (hn' : n < order_of f) : is_cycle (f ^ n) :=
 begin
   classical,
+  casesI nonempty_fintype β,
   have : n.coprime (order_of f),
   { refine nat.coprime.symm _,
     rw nat.prime.coprime_iff_not_dvd hf',
@@ -817,7 +820,7 @@ else let ⟨m, hm₁, hm₂, hm₃⟩ := cycle_factors_aux l ((cycle_of f x)⁻
                 inv_apply_self, inv_eq_iff_eq, eq_comm] }),
         hm₃⟩⟩
 
-lemma mem_list_cycles_iff {α : Type*} [fintype α] {l : list (perm α)}
+lemma mem_list_cycles_iff {α : Type*} [finite α] {l : list (perm α)}
   (h1 : ∀ σ : perm α, σ ∈ l → σ.is_cycle)
   (h2 : l.pairwise disjoint) {σ : perm α} :
   σ ∈ l ↔ σ.is_cycle ∧ ∀ (a : α) (h4 : σ a ≠ a), σ a = l.prod a :=
@@ -826,6 +829,7 @@ begin
   { exact ⟨λ hσ, ⟨h1 σ hσ, (this (h1 σ hσ)).mp hσ⟩, λ hσ, (this hσ.1).mpr hσ.2⟩ },
   intro h3,
   classical,
+  casesI nonempty_fintype α,
   split,
   { intros h a ha,
     exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha) },
@@ -846,7 +850,7 @@ begin
     exact key a (mem_inter_of_mem ha hτa) }
 end
 
-lemma list_cycles_perm_list_cycles {α : Type*} [fintype α] {l₁ l₂ : list (perm α)}
+lemma list_cycles_perm_list_cycles {α : Type*} [finite α] {l₁ l₂ : list (perm α)}
   (h₀ : l₁.prod = l₂.prod)
   (h₁l₁ : ∀ σ : perm α, σ ∈ l₁ → σ.is_cycle) (h₁l₂ : ∀ σ : perm α, σ ∈ l₂ → σ.is_cycle)
   (h₂l₁ : l₁.pairwise disjoint) (h₂l₂ : l₂.pairwise disjoint) :
@@ -1090,11 +1094,12 @@ end
 
 end cycle_factors_finset
 
-@[elab_as_eliminator] lemma cycle_induction_on [fintype β] (P : perm β → Prop) (σ : perm β)
+@[elab_as_eliminator] lemma cycle_induction_on [finite β] (P : perm β → Prop) (σ : perm β)
   (base_one : P 1) (base_cycles : ∀ σ : perm β, σ.is_cycle → P σ)
   (induction_disjoint : ∀ σ τ : perm β, disjoint σ τ → is_cycle σ → P σ → P τ → P (σ * τ)) :
   P σ :=
 begin
+  casesI nonempty_fintype β,
   suffices :
     ∀ l : list (perm β), (∀ τ : perm β, τ ∈ l → τ.is_cycle) → l.pairwise disjoint → P l.prod,
   { classical,
@@ -1224,16 +1229,19 @@ end
 
 section generation
 
-variables [fintype α] [fintype β]
+variables [finite β]
 
 open subgroup
 
 lemma closure_is_cycle : closure {σ : perm β | is_cycle σ} = ⊤ :=
 begin
   classical,
+  casesI nonempty_fintype β,
   exact top_le_iff.mp (le_trans (ge_of_eq closure_is_swap) (closure_mono (λ _, is_swap.is_cycle))),
 end
 
+variables [fintype α]
+
 lemma closure_cycle_adjacent_swap {σ : perm α} (h1 : is_cycle σ) (h2 : σ.support = ⊤) (x : α) :
   closure ({σ, swap x (σ x)} : set (perm α)) = ⊤ :=
 begin
@@ -1377,12 +1385,13 @@ by simp
 
 end
 
-theorem disjoint.is_conj_mul {α : Type*} [fintype α] {σ τ π ρ : perm α}
+theorem disjoint.is_conj_mul {α : Type*} [finite α] {σ τ π ρ : perm α}
   (hc1 : is_conj σ π) (hc2 : is_conj τ ρ)
   (hd1 : disjoint σ τ) (hd2 : disjoint π ρ) :
   is_conj (σ * τ) (π * ρ) :=
 begin
   classical,
+  casesI nonempty_fintype α,
   obtain ⟨f, rfl⟩ := is_conj_iff.1 hc1,
   obtain ⟨g, rfl⟩ := is_conj_iff.1 hc2,
   have hd1' := coe_inj.2 hd1.support_mul,
diff --git a/src/group_theory/perm/cycle/concrete.lean b/src/group_theory/perm/cycle/concrete.lean
index 4e20b7e894866..fc7470c598f96 100644
--- a/src/group_theory/perm/cycle/concrete.lean
+++ b/src/group_theory/perm/cycle/concrete.lean
@@ -46,9 +46,11 @@ to show it takes a long time. TODO: is this because computing the cycle factors
 
 open equiv equiv.perm list
 
+variables {α : Type*}
+
 namespace list
 
-variables {α : Type*} [decidable_eq α] {l l' : list α}
+variables [decidable_eq α] {l l' : list α}
 
 lemma form_perm_disjoint_iff (hl : nodup l) (hl' : nodup l')
   (hn : 2 ≤ l.length) (hn' : 2 ≤ l'.length) :
@@ -124,7 +126,7 @@ end list
 
 namespace cycle
 
-variables {α : Type*} [decidable_eq α] (s s' : cycle α)
+variables [decidable_eq α] (s s' : cycle α)
 
 /--
 A cycle `s : cycle α` , given `nodup s` can be interpreted as a `equiv.perm α`
@@ -205,10 +207,9 @@ begin
 end
 
 end cycle
-variables {α : Type*}
 
 namespace equiv.perm
-
+section fintype
 variables [fintype α] [decidable_eq α] (p : equiv.perm α) (x : α)
 
 /--
@@ -397,49 +398,6 @@ begin
     simp [mem_to_list_iff, hy] }
 end
 
-lemma is_cycle.exists_unique_cycle {f : perm α} (hf : is_cycle f) :
-  ∃! (s : cycle α), ∃ (h : s.nodup), s.form_perm h = f :=
-begin
-  obtain ⟨x, hx, hy⟩ := id hf,
-  refine ⟨f.to_list x, ⟨nodup_to_list f x, _⟩, _⟩,
-  { simp [form_perm_to_list, hf.cycle_of_eq hx] },
-  { rintro ⟨l⟩ ⟨hn, rfl⟩,
-    simp only [cycle.mk_eq_coe, cycle.coe_eq_coe, subtype.coe_mk, cycle.form_perm_coe],
-    refine (to_list_form_perm_is_rotated_self _ _ hn _ _).symm,
-    { contrapose! hx,
-      suffices : form_perm l = 1,
-      { simp [this] },
-      rw form_perm_eq_one_iff _ hn,
-      exact nat.le_of_lt_succ hx },
-    { rw ←mem_to_finset,
-      refine support_form_perm_le l _,
-      simpa using hx } }
-end
-
-lemma is_cycle.exists_unique_cycle_subtype {f : perm α} (hf : is_cycle f) :
-  ∃! (s : {s : cycle α // s.nodup}), (s : cycle α).form_perm s.prop = f :=
-begin
-  obtain ⟨s, ⟨hs, rfl⟩, hs'⟩ := hf.exists_unique_cycle,
-  refine ⟨⟨s, hs⟩, rfl, _⟩,
-  rintro ⟨t, ht⟩ ht',
-  simpa using hs' _ ⟨ht, ht'⟩
-end
-
-lemma is_cycle.exists_unique_cycle_nontrivial_subtype {f : perm α} (hf : is_cycle f) :
-  ∃! (s : {s : cycle α // s.nodup ∧ s.nontrivial}), (s : cycle α).form_perm s.prop.left = f :=
-begin
-  obtain ⟨⟨s, hn⟩, hs, hs'⟩ := hf.exists_unique_cycle_subtype,
-  refine ⟨⟨s, hn, _⟩, _, _⟩,
-  { rw hn.nontrivial_iff,
-    subst f,
-    intro H,
-    refine hf.ne_one _,
-    simpa using cycle.form_perm_subsingleton _ H },
-  { simpa using hs },
-  { rintro ⟨t, ht, ht'⟩ ht'',
-    simpa using hs' ⟨t, ht⟩ ht'' }
-end
-
 /--
 Given a cyclic `f : perm α`, generate the `cycle α` in the order
 of application of `f`. Implemented by finding an element `x : α`
@@ -505,6 +463,59 @@ def iso_cycle : {f : perm α // is_cycle f} ≃ {s : cycle α // s.nodup ∧ s.n
       { rintro _ rfl,
         simpa [nat.succ_le_succ_iff] using hl } } } }
 
+end fintype
+
+section finite
+variables [finite α] [decidable_eq α]
+
+lemma is_cycle.exists_unique_cycle {f : perm α} (hf : is_cycle f) :
+  ∃! (s : cycle α), ∃ (h : s.nodup), s.form_perm h = f :=
+begin
+  casesI nonempty_fintype α,
+  obtain ⟨x, hx, hy⟩ := id hf,
+  refine ⟨f.to_list x, ⟨nodup_to_list f x, _⟩, _⟩,
+  { simp [form_perm_to_list, hf.cycle_of_eq hx] },
+  { rintro ⟨l⟩ ⟨hn, rfl⟩,
+    simp only [cycle.mk_eq_coe, cycle.coe_eq_coe, subtype.coe_mk, cycle.form_perm_coe],
+    refine (to_list_form_perm_is_rotated_self _ _ hn _ _).symm,
+    { contrapose! hx,
+      suffices : form_perm l = 1,
+      { simp [this] },
+      rw form_perm_eq_one_iff _ hn,
+      exact nat.le_of_lt_succ hx },
+    { rw ←mem_to_finset,
+      refine support_form_perm_le l _,
+      simpa using hx } }
+end
+
+lemma is_cycle.exists_unique_cycle_subtype {f : perm α} (hf : is_cycle f) :
+  ∃! (s : {s : cycle α // s.nodup}), (s : cycle α).form_perm s.prop = f :=
+begin
+  obtain ⟨s, ⟨hs, rfl⟩, hs'⟩ := hf.exists_unique_cycle,
+  refine ⟨⟨s, hs⟩, rfl, _⟩,
+  rintro ⟨t, ht⟩ ht',
+  simpa using hs' _ ⟨ht, ht'⟩
+end
+
+lemma is_cycle.exists_unique_cycle_nontrivial_subtype {f : perm α} (hf : is_cycle f) :
+  ∃! (s : {s : cycle α // s.nodup ∧ s.nontrivial}), (s : cycle α).form_perm s.prop.left = f :=
+begin
+  obtain ⟨⟨s, hn⟩, hs, hs'⟩ := hf.exists_unique_cycle_subtype,
+  refine ⟨⟨s, hn, _⟩, _, _⟩,
+  { rw hn.nontrivial_iff,
+    subst f,
+    intro H,
+    refine hf.ne_one _,
+    simpa using cycle.form_perm_subsingleton _ H },
+  { simpa using hs },
+  { rintro ⟨t, ht, ht'⟩ ht'',
+    simpa using hs' ⟨t, ht⟩ ht'' }
+end
+
+end finite
+
+variables [fintype α] [decidable_eq α]
+
 /--
 Any cyclic `f : perm α` is isomorphic to the nontrivial `cycle α`
 that corresponds to repeated application of `f`.
diff --git a/src/group_theory/perm/sign.lean b/src/group_theory/perm/sign.lean
index 125aab8691161..704ea1e95cc82 100644
--- a/src/group_theory/perm/sign.lean
+++ b/src/group_theory/perm/sign.lean
@@ -54,30 +54,27 @@ begin
   simp only [inv_apply_self]
 end
 
-lemma perm_inv_maps_to_of_maps_to (f : perm α) {s : set α} [fintype s]
-  (h : set.maps_to f s s) : set.maps_to (f⁻¹ : _) s s :=
-λ x hx, set.mem_to_finset.mp $
+lemma perm_inv_maps_to_of_maps_to (f : perm α) {s : set α} [finite s] (h : set.maps_to f s s) :
+  set.maps_to (f⁻¹ : _) s s :=
+by casesI nonempty_fintype s; exact λ x hx, set.mem_to_finset.mp $
   perm_inv_on_of_perm_on_finset
    (λ a ha, set.mem_to_finset.mpr (h (set.mem_to_finset.mp ha)))
    (set.mem_to_finset.mpr hx)
 
-@[simp] lemma perm_inv_maps_to_iff_maps_to {f : perm α} {s : set α} [fintype s] :
+@[simp] lemma perm_inv_maps_to_iff_maps_to {f : perm α} {s : set α} [finite s] :
   set.maps_to (f⁻¹ : _) s s ↔ set.maps_to f s s :=
 ⟨perm_inv_maps_to_of_maps_to f⁻¹, perm_inv_maps_to_of_maps_to f⟩
 
-lemma perm_inv_on_of_perm_on_fintype {f : perm α} {p : α → Prop} [fintype {x // p x}]
+lemma perm_inv_on_of_perm_on_finite {f : perm α} {p : α → Prop} [finite {x // p x}]
   (h : ∀ x, p x → p (f x)) {x : α} (hx : p x) : p (f⁻¹ x) :=
-begin
-  letI : fintype ↥(show set α, from p) := ‹fintype {x // p x}›,
-  exact perm_inv_maps_to_of_maps_to f h hx
-end
+perm_inv_maps_to_of_maps_to f h hx
 
 /-- If the permutation `f` maps `{x // p x}` into itself, then this returns the permutation
   on `{x // p x}` induced by `f`. Note that the `h` hypothesis is weaker than for
   `equiv.perm.subtype_perm`. -/
 abbreviation subtype_perm_of_fintype (f : perm α) {p : α → Prop} [fintype {x // p x}]
   (h : ∀ x, p x → p (f x)) : perm {x // p x} :=
-f.subtype_perm (λ x, ⟨h x, λ h₂, f.inv_apply_self x ▸ perm_inv_on_of_perm_on_fintype h h₂⟩)
+f.subtype_perm (λ x, ⟨h x, λ h₂, f.inv_apply_self x ▸ perm_inv_on_of_perm_on_finite h h₂⟩)
 
 @[simp] lemma subtype_perm_of_fintype_apply (f : perm α) {p : α → Prop} [fintype {x // p x}]
   (h : ∀ x, p x → p (f x)) (x : {x // p x}) : subtype_perm_of_fintype f h x = ⟨f x, h x x.2⟩ := rfl
@@ -86,11 +83,12 @@ f.subtype_perm (λ x, ⟨h x, λ h₂, f.inv_apply_self x ▸ perm_inv_on_of_per
   (h : ∀ x, p x → p ((1 : perm α) x)) : @subtype_perm_of_fintype α 1 p _ h = 1 :=
 equiv.ext $ λ ⟨_, _⟩, rfl
 
-lemma perm_maps_to_inl_iff_maps_to_inr {m n : Type*} [fintype m] [fintype n]
-  (σ : equiv.perm (m ⊕ n)) :
+lemma perm_maps_to_inl_iff_maps_to_inr {m n : Type*} [finite m] [finite n] (σ : perm (m ⊕ n)) :
   set.maps_to σ (set.range sum.inl) (set.range sum.inl) ↔
   set.maps_to σ (set.range sum.inr) (set.range sum.inr) :=
 begin
+  casesI nonempty_fintype m,
+  casesI nonempty_fintype n,
   split; id
   { intros h,
     classical,
@@ -109,10 +107,12 @@ begin
     exact absurd hy sum.inr_ne_inl},
 end
 
-lemma mem_sum_congr_hom_range_of_perm_maps_to_inl {m n : Type*} [fintype m] [fintype n]
+lemma mem_sum_congr_hom_range_of_perm_maps_to_inl {m n : Type*} [finite m] [finite n]
   {σ : perm (m ⊕ n)} (h : set.maps_to σ (set.range sum.inl) (set.range sum.inl)) :
   σ ∈ (sum_congr_hom m n).range :=
 begin
+  casesI nonempty_fintype m,
+  casesI nonempty_fintype n,
   classical,
   have h1 : ∀ (x : m ⊕ n), (∃ (a : m), sum.inl a = x) → (∃ (a : m), sum.inl a = σ x),
   { rintros x ⟨a, ha⟩, apply h, rw ← ha, exact ⟨a, rfl⟩ },
@@ -212,9 +212,10 @@ quotient.rec_on_subsingleton (@univ α _).1
 
 /-- An induction principle for permutations. If `P` holds for the identity permutation, and
 is preserved under composition with a non-trivial swap, then `P` holds for all permutations. -/
-@[elab_as_eliminator] lemma swap_induction_on [fintype α] {P : perm α → Prop} (f : perm α) :
+@[elab_as_eliminator] lemma swap_induction_on [finite α] {P : perm α → Prop} (f : perm α) :
   P 1 → (∀ f x y, x ≠ y → P f → P (swap x y * f)) → P f :=
 begin
+  casesI nonempty_fintype α,
   cases (trunc_swap_factors f).out with l hl,
   induction l with g l ih generalizing f,
   { simp only [hl.left.symm, list.prod_nil, forall_true_iff] {contextual := tt} },
@@ -225,8 +226,9 @@ begin
       (ih _ ⟨rfl, λ v hv, hl.2 _ (list.mem_cons_of_mem _ hv)⟩ h1 hmul_swap) }
 end
 
-lemma closure_is_swap [fintype α] : subgroup.closure {σ : perm α | is_swap σ} = ⊤ :=
+lemma closure_is_swap [finite α] : subgroup.closure {σ : perm α | is_swap σ} = ⊤ :=
 begin
+  casesI nonempty_fintype α,
   refine eq_top_iff.mpr (λ x hx, _),
   obtain ⟨h1, h2⟩ := subtype.mem (trunc_swap_factors x).out,
   rw ← h1,
@@ -237,7 +239,7 @@ end
 
 An induction principle for permutations. If `P` holds for the identity permutation, and
 is preserved under composition with a non-trivial swap, then `P` holds for all permutations. -/
-@[elab_as_eliminator] lemma swap_induction_on' [fintype α] {P : perm α → Prop} (f : perm α) :
+@[elab_as_eliminator] lemma swap_induction_on' [finite α] {P : perm α → Prop} (f : perm α) :
   P 1 → (∀ f x y, x ≠ y → P f → P (f * swap x y)) → P f :=
 λ h1 IH, inv_inv f ▸ swap_induction_on f⁻¹ h1 (λ f, IH f⁻¹)
 
@@ -636,7 +638,7 @@ sign_bij (λ (ab : α × β) _, ab.snd)
 lemma sign_prod_congr_right (σ : α → perm β) :
   sign (prod_congr_right σ) = ∏ k, (σ k).sign :=
 begin
-  obtain ⟨l, hl, mem_l⟩ := fintype.exists_univ_list α,
+  obtain ⟨l, hl, mem_l⟩ := finite.exists_univ_list α,
   have l_to_finset : l.to_finset = finset.univ,
   { apply eq_top_iff.mpr,
     intros b _,
diff --git a/src/group_theory/schur_zassenhaus.lean b/src/group_theory/schur_zassenhaus.lean
index ddc8d4688c836..a425f1600e0d7 100644
--- a/src/group_theory/schur_zassenhaus.lean
+++ b/src/group_theory/schur_zassenhaus.lean
@@ -177,12 +177,12 @@ begin
   contrapose! h4,
   have h5 : fintype.card (G ⧸ K) < fintype.card G,
   { rw [←index_eq_card, ←K.index_mul_card],
-    refine lt_mul_of_one_lt_right (nat.pos_of_ne_zero index_ne_zero_of_fintype)
+    refine lt_mul_of_one_lt_right (nat.pos_of_ne_zero index_ne_zero_of_finite)
       (K.one_lt_card_iff_ne_bot.mpr h4.1) },
   have h6 : nat.coprime (fintype.card (N.map (quotient_group.mk' K)))
     (N.map (quotient_group.mk' K)).index,
   { have index_map := N.index_map_eq this (by rwa quotient_group.ker_mk),
-    have index_pos : 0 < N.index := nat.pos_of_ne_zero index_ne_zero_of_fintype,
+    have index_pos : 0 < N.index := nat.pos_of_ne_zero index_ne_zero_of_finite,
     rw index_map,
     refine h1.coprime_dvd_left _,
     rw [←nat.mul_dvd_mul_iff_left index_pos, index_mul_card, ←index_map, index_mul_card],
diff --git a/src/group_theory/specific_groups/cyclic.lean b/src/group_theory/specific_groups/cyclic.lean
index 3499df0fee3b9..234e9c3513e62 100644
--- a/src/group_theory/specific_groups/cyclic.lean
+++ b/src/group_theory/specific_groups/cyclic.lean
@@ -99,7 +99,7 @@ begin
 end
 
 /-- A finite group of prime order is cyclic. -/
-@[to_additive is_add_cyclic_of_prime_card]
+@[to_additive is_add_cyclic_of_prime_card "A finite group of prime order is cyclic."]
 lemma is_cyclic_of_prime_card {α : Type u} [group α] [fintype α] {p : ℕ} [hp : fact p.prime]
   (h : fintype.card α = p) : is_cyclic α :=
 ⟨begin
@@ -246,8 +246,8 @@ calc (univ.filter (λ a : α, a ^ n = 1)).card
 end classical
 
 @[to_additive]
-lemma is_cyclic.exists_monoid_generator [fintype α]
-[is_cyclic α] : ∃ x : α, ∀ y : α, y ∈ submonoid.powers x :=
+lemma is_cyclic.exists_monoid_generator [finite α] [is_cyclic α] :
+  ∃ x : α, ∀ y : α, y ∈ submonoid.powers x :=
 by { simp_rw [mem_powers_iff_mem_zpowers], exact is_cyclic.exists_generator α }
 
 section
@@ -382,7 +382,7 @@ end
 attribute [to_additive is_cyclic.card_order_of_eq_totient] is_add_cyclic.card_order_of_eq_totient
 
 /-- A finite group of prime order is simple. -/
-@[to_additive]
+@[to_additive "A finite group of prime order is simple."]
 lemma is_simple_group_of_prime_card {α : Type u} [group α] [fintype α] {p : ℕ} [hp : fact p.prime]
   (h : fintype.card α = p) : is_simple_group α :=
 ⟨begin
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index 97174d54c780b..b09bcb9c45d46 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -702,7 +702,8 @@ H.eq_bot_of_card_le (le_of_eq h)
 subtype.nontrivial_iff_exists_ne (λ x, x ∈ H) (1 : H)
 
 /-- A subgroup is either the trivial subgroup or nontrivial. -/
-@[to_additive] lemma bot_or_nontrivial (H : subgroup G) : H = ⊥ ∨ nontrivial H :=
+@[to_additive "A subgroup is either the trivial subgroup or nontrivial."]
+lemma bot_or_nontrivial (H : subgroup G) : H = ⊥ ∨ nontrivial H :=
 begin
   classical,
   by_cases h : ∀ x ∈ H, x = (1 : G),
@@ -713,8 +714,9 @@ begin
     simpa only [nontrivial_iff_exists_ne_one] }
 end
 
-/-- A subgroup is either the trivial subgroup or contains a nonzero element. -/
-@[to_additive] lemma bot_or_exists_ne_one (H : subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ (1:G) :=
+/-- A subgroup is either the trivial subgroup or contains a non-identity element. -/
+@[to_additive "A subgroup is either the trivial subgroup or contains a nonzero element."]
+lemma bot_or_exists_ne_one (H : subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ (1:G) :=
 begin
   convert H.bot_or_nontrivial,
   rw nontrivial_iff_exists_ne_one
@@ -1465,15 +1467,16 @@ begin
 end
 
 @[to_additive]
-lemma pi_mem_of_mul_single_mem [fintype η] [decidable_eq η] {H : subgroup (Π i, f i)}
+lemma pi_mem_of_mul_single_mem [finite η] [decidable_eq η] {H : subgroup (Π i, f i)}
   (x : Π i, f i) (h : ∀ i, pi.mul_single i (x i) ∈ H) : x ∈ H :=
-pi_mem_of_mul_single_mem_aux finset.univ x (by simp) (λ i _, h i)
+by { casesI nonempty_fintype η,
+   exact pi_mem_of_mul_single_mem_aux finset.univ x (by simp) (λ i _, h i) }
 
 /-- For finite index types, the `subgroup.pi` is generated by the embeddings of the groups.  -/
 @[to_additive "For finite index types, the `subgroup.pi` is generated by the embeddings of the
 additive groups."]
-lemma pi_le_iff [decidable_eq η] [fintype η] {H : Π i, subgroup (f i)} {J : subgroup (Π i, f i)} :
-  pi univ H ≤ J ↔ (∀ i : η, map (monoid_hom.single f i) (H i) ≤ J) :=
+lemma pi_le_iff [decidable_eq η] [finite η] {H : Π i, subgroup (f i)} {J : subgroup (Π i, f i)} :
+  pi univ H ≤ J ↔ ∀ i : η, map (monoid_hom.single f i) (H i) ≤ J :=
 begin
   split,
   { rintros h i _ ⟨x, hx, rfl⟩, apply h, simpa using hx },
@@ -1674,9 +1677,9 @@ def set_normalizer (S : set G) : subgroup G :=
   inv_mem' := λ a (ha : ∀ n, n ∈ S ↔ a * n * a⁻¹ ∈ S) n,
     by { rw [ha (a⁻¹ * n * a⁻¹⁻¹)], simp [mul_assoc] } }
 
-lemma mem_normalizer_fintype {S : set G} [fintype S] {x : G}
+lemma mem_normalizer_fintype {S : set G} [finite S] {x : G}
   (h : ∀ n, n ∈ S → x * n * x⁻¹ ∈ S) : x ∈ subgroup.set_normalizer S :=
-by haveI := classical.prop_decidable;
+by haveI := classical.prop_decidable; casesI nonempty_fintype S;
 haveI := set.fintype_image S (λ n, x * n * x⁻¹); exact
 λ n, ⟨h n, λ h₁,
 have heq : (λ n, x * n * x⁻¹) '' S = S := set.eq_of_subset_of_card_le
@@ -1817,8 +1820,9 @@ structure _root_.add_subgroup.is_commutative (H : add_subgroup A) : Prop :=
 attribute [to_additive add_subgroup.is_commutative] subgroup.is_commutative
 attribute [class] add_subgroup.is_commutative
 
-/-- A commutative subgroup is commutative -/
-@[to_additive] instance is_commutative.comm_group [h : H.is_commutative] : comm_group H :=
+/-- A commutative subgroup is commutative. -/
+@[to_additive "A commutative subgroup is commutative."]
+instance is_commutative.comm_group [h : H.is_commutative] : comm_group H :=
 { mul_comm := h.is_comm.comm, .. H.to_group }
 
 instance center.is_commutative : (center G).is_commutative :=
@@ -2157,9 +2161,9 @@ def eq_locus (f g : G →* N) : subgroup G :=
   .. eq_mlocus f g}
 
 /-- If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure. -/
-@[to_additive]
-lemma eq_on_closure {f g : G →* N} {s : set G} (h : set.eq_on f g s) :
-  set.eq_on f g (closure s) :=
+@[to_additive "If two monoid homomorphisms are equal on a set, then they are equal on its subgroup
+closure."]
+lemma eq_on_closure {f g : G →* N} {s : set G} (h : set.eq_on f g s) : set.eq_on f g (closure s) :=
 show closure s ≤ f.eq_locus g, from (closure_le _).2 h
 
 @[to_additive]
@@ -2337,8 +2341,9 @@ lemma map_eq_comap_of_inverse {f : G →* N} {g : N →* G} (hl : function.left_
   (hr : function.right_inverse g f) (H : subgroup G) : map f H = comap g H :=
 set_like.ext' $ by rw [coe_map, coe_comap, set.image_eq_preimage_of_inverse hl hr]
 
-/-- Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`  -/
-@[to_additive] lemma map_injective_of_ker_le
+/-- Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`. -/
+@[to_additive "Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`."]
+lemma map_injective_of_ker_le
   {H K : subgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K) (hf : map f H = map f K) :
   H = K :=
 begin
@@ -2967,8 +2972,8 @@ begin
   rwa [mul_assoc, mul_assoc, mul_right_inv, mul_one] at this,
 end
 
-/-- Elements of disjoint, normal subgroups commute -/
-@[to_additive] lemma commute_of_normal_of_disjoint
+/-- Elements of disjoint, normal subgroups commute. -/
+@[to_additive "Elements of disjoint, normal subgroups commute."] lemma commute_of_normal_of_disjoint
   (H₁ H₂ : subgroup G) (hH₁ : H₁.normal) (hH₂ : H₂.normal) (hdis : disjoint H₁ H₂)
   (x y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) :
   commute x y :=
diff --git a/src/group_theory/submonoid/basic.lean b/src/group_theory/submonoid/basic.lean
index d202fefda1ffa..99493198c8db4 100644
--- a/src/group_theory/submonoid/basic.lean
+++ b/src/group_theory/submonoid/basic.lean
@@ -449,7 +449,8 @@ def eq_mlocus (f g : M →* N) : submonoid M :=
   mul_mem' := λ x y (hx : _ = _) (hy : _ = _), by simp [*] }
 
 /-- If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure. -/
-@[to_additive]
+@[to_additive "If two monoid homomorphisms are equal on a set, then they are equal on its submonoid
+closure."]
 lemma eq_on_mclosure {f g : M →* N} {s : set M} (h : set.eq_on f g s) :
   set.eq_on f g (closure s) :=
 show closure s ≤ f.eq_mlocus g, from closure_le.2 h
diff --git a/src/group_theory/sylow.lean b/src/group_theory/sylow.lean
index bdf9eb26baa6a..304130b9e3113 100644
--- a/src/group_theory/sylow.lean
+++ b/src/group_theory/sylow.lean
@@ -158,6 +158,10 @@ sylow.fintype_of_ker_is_p_group (is_p_group.ker_is_p_group_of_injective hf)
 noncomputable instance (H : subgroup G) [fintype (sylow p G)] : fintype (sylow p H) :=
 sylow.fintype_of_injective (show function.injective H.subtype, from subtype.coe_injective)
 
+/-- If `H` is a subgroup of `G`, then `finite (sylow p G)` implies `finite (sylow p H)`. -/
+instance (H : subgroup G) [finite (sylow p G)] : finite (sylow p H) :=
+by { casesI nonempty_fintype (sylow p G), apply_instance }
+
 open_locale pointwise
 
 /-- `subgroup.pointwise_mul_action` preserves Sylow subgroups. -/
@@ -219,9 +223,10 @@ by rw [P.sylow_mem_fixed_points_iff, ←inf_eq_left, hP.inf_normalizer_sylow, in
 
 /-- A generalization of **Sylow's second theorem**.
   If the number of Sylow `p`-subgroups is finite, then all Sylow `p`-subgroups are conjugate. -/
-instance [hp : fact p.prime] [fintype (sylow p G)] : is_pretransitive G (sylow p G) :=
+instance [hp : fact p.prime] [finite (sylow p G)] : is_pretransitive G (sylow p G) :=
 ⟨λ P Q, by
 { classical,
+  casesI nonempty_fintype (sylow p G),
   have H := λ {R : sylow p G} {S : orbit G P},
   calc S ∈ fixed_points R (orbit G P)
       ↔ S.1 ∈ fixed_points R (sylow p G) : forall_congr (λ a, subtype.ext_iff)
@@ -267,14 +272,14 @@ def sylow.equiv_smul (P : sylow p G) (g : G) : P ≃* (g • P : sylow p G) :=
 equiv_smul (mul_aut.conj g) ↑P
 
 /-- Sylow subgroups are isomorphic -/
-noncomputable def sylow.equiv [fact p.prime] [fintype (sylow p G)] (P Q : sylow p G) :
+noncomputable def sylow.equiv [fact p.prime] [finite (sylow p G)] (P Q : sylow p G) :
   P ≃* Q :=
 begin
   rw ← classical.some_spec (exists_smul_eq G P Q),
   exact P.equiv_smul (classical.some (exists_smul_eq G P Q)),
 end
 
-@[simp] lemma sylow.orbit_eq_top [fact p.prime] [fintype (sylow p G)] (P : sylow p G) :
+@[simp] lemma sylow.orbit_eq_top [fact p.prime] [finite (sylow p G)] (P : sylow p G) :
   orbit G P = ⊤ :=
 top_le_iff.mp (λ Q hQ, exists_smul_eq G P Q)
 
@@ -325,9 +330,10 @@ begin
   exact hp.ne' (P.3 hQ hp.le),
 end
 
-lemma not_dvd_index_sylow [hp : fact p.prime] [fintype (sylow p G)] (P : sylow p G)
+lemma not_dvd_index_sylow [hp : fact p.prime] [finite (sylow p G)] (P : sylow p G)
   (hP : relindex ↑P (P : subgroup G).normalizer ≠ 0) : ¬ p ∣ (P : subgroup G).index :=
 begin
+  casesI nonempty_fintype (sylow p G),
   rw [←relindex_mul_index le_normalizer, ←card_sylow_eq_index_normalizer],
   haveI : (P.subtype le_normalizer : subgroup (P : subgroup G).normalizer).normal :=
   subgroup.normal_in_normalizer,
@@ -338,7 +344,7 @@ end
 /-- Frattini's Argument: If `N` is a normal subgroup of `G`, and if `P` is a Sylow `p`-subgroup
   of `N`, then `N_G(P) ⊔ N = G`. -/
 lemma sylow.normalizer_sup_eq_top {p : ℕ} [fact p.prime] {N : subgroup G} [N.normal]
-  [fintype (sylow p N)] (P : sylow p N) : ((↑P : subgroup N).map N.subtype).normalizer ⊔ N = ⊤ :=
+  [finite (sylow p N)] (P : sylow p N) : ((↑P : subgroup N).map N.subtype).normalizer ⊔ N = ⊤ :=
 begin
   refine top_le_iff.mp (λ g hg, _),
   obtain ⟨n, hn⟩ := exists_smul_eq N ((mul_aut.conj_normal g : mul_aut N) • P) P,
@@ -371,12 +377,12 @@ namespace sylow
 
 open subgroup submonoid mul_action
 
-lemma mem_fixed_points_mul_left_cosets_iff_mem_normalizer {H : subgroup G}
-  [fintype ((H : set G) : Type u)] {x : G} :
+lemma mem_fixed_points_mul_left_cosets_iff_mem_normalizer {H : subgroup G} [finite ↥(H : set G)]
+  {x : G} :
   (x : G ⧸ H) ∈ fixed_points H (G ⧸ H) ↔ x ∈ normalizer H :=
 ⟨λ hx, have ha : ∀ {y : G ⧸ H}, y ∈ orbit H (x : G ⧸ H) → y = x,
   from λ _, ((mem_fixed_points' _).1 hx _),
-  inv_mem_iff.1 (@mem_normalizer_fintype _ _ _ _ _ (λ n (hn : n ∈ H),
+  inv_mem_iff.1 (mem_normalizer_fintype (λ n (hn : n ∈ H),
     have (n⁻¹ * x)⁻¹ * x ∈ H := quotient_group.eq.1 (ha (mem_orbit _ ⟨n⁻¹, H.inv_mem hn⟩)),
     show _ ∈ H, by {rw [mul_inv_rev, inv_inv] at this, convert this, rw inv_inv}
     )),
@@ -388,7 +394,8 @@ lemma mem_fixed_points_mul_left_cosets_iff_mem_normalizer {H : subgroup G}
   $ by rw hx at hb₂;
     simpa [mul_inv_rev, mul_assoc] using hb₂)⟩
 
-def fixed_points_mul_left_cosets_equiv_quotient (H : subgroup G) [fintype (H : set G)] :
+/-- The fixed points of the action of `H` on its cosets correspond to `normalizer H / H`. -/
+def fixed_points_mul_left_cosets_equiv_quotient (H : subgroup G) [finite (H : set G)] :
   mul_action.fixed_points H (G ⧸ H) ≃
   normalizer H ⧸ (subgroup.comap ((normalizer H).subtype : normalizer H →* G) H) :=
 @subtype_quotient_equiv_quotient_subtype G (normalizer H : set G) (id _) (id _) (fixed_points _ _)
@@ -523,7 +530,7 @@ let ⟨K, hK⟩ := exists_subgroup_card_pow_prime_le p hdvd ⊥ (by simp) n.zero
 lemma pow_dvd_card_of_pow_dvd_card [fintype G] {p n : ℕ} [hp : fact p.prime] (P : sylow p G)
   (hdvd : p ^ n ∣ card G) : p ^ n ∣ card P :=
 (hp.1.coprime_pow_of_not_dvd (not_dvd_index_sylow P
-  index_ne_zero_of_fintype)).symm.dvd_of_dvd_mul_left ((index_mul_card P.1).symm ▸ hdvd)
+  index_ne_zero_of_finite)).symm.dvd_of_dvd_mul_left ((index_mul_card P.1).symm ▸ hdvd)
 
 lemma dvd_card_of_dvd_card [fintype G] {p : ℕ} [fact p.prime] (P : sylow p G)
   (hdvd : p ∣ card G) : p ∣ card P :=
@@ -537,7 +544,7 @@ end
 lemma card_coprime_index [fintype G] {p : ℕ} [hp : fact p.prime] (P : sylow p G) :
   (card P).coprime (index (P : subgroup G)) :=
 let ⟨n, hn⟩ := is_p_group.iff_card.mp P.2 in
-hn.symm ▸ (hp.1.coprime_pow_of_not_dvd (not_dvd_index_sylow P index_ne_zero_of_fintype)).symm
+hn.symm ▸ (hp.1.coprime_pow_of_not_dvd (not_dvd_index_sylow P index_ne_zero_of_finite)).symm
 
 lemma ne_bot_of_dvd_card [fintype G] {p : ℕ} [hp : fact p.prime] (P : sylow p G)
   (hdvd : p ∣ card G) : (P : subgroup G) ≠ ⊥ :=
@@ -558,7 +565,7 @@ begin
   exact P.1.card_subgroup_dvd_card,
 end
 
-lemma subsingleton_of_normal {p : ℕ} [fact p.prime] [fintype (sylow p G)] (P : sylow p G)
+lemma subsingleton_of_normal {p : ℕ} [fact p.prime] [finite (sylow p G)] (P : sylow p G)
   (h : (P : subgroup G).normal) : subsingleton (sylow p G) :=
 begin
   apply subsingleton.intro,
@@ -573,7 +580,7 @@ section pointwise
 
 open_locale pointwise
 
-lemma characteristic_of_normal {p : ℕ} [fact p.prime] [fintype (sylow p G)] (P : sylow p G)
+lemma characteristic_of_normal {p : ℕ} [fact p.prime] [finite (sylow p G)] (P : sylow p G)
   (h : (P : subgroup G).normal) :
   (P : subgroup G).characteristic :=
 begin
@@ -586,14 +593,13 @@ end
 
 end pointwise
 
-lemma normal_of_normalizer_normal {p : ℕ} [fact p.prime] [fintype (sylow p G)]
+lemma normal_of_normalizer_normal {p : ℕ} [fact p.prime] [finite (sylow p G)]
   (P : sylow p G) (hn : (↑P : subgroup G).normalizer.normal) :
   (↑P : subgroup G).normal :=
 by rw [←normalizer_eq_top, ←normalizer_sup_eq_top (P.subtype le_normalizer), coe_subtype,
   map_comap_eq_self (le_normalizer.trans (ge_of_eq (subtype_range _))), sup_idem]
 
-@[simp] lemma normalizer_normalizer {p : ℕ} [fact p.prime] [fintype (sylow p G)]
- (P : sylow p G) :
+@[simp] lemma normalizer_normalizer {p : ℕ} [fact p.prime] [finite (sylow p G)] (P : sylow p G) :
  (↑P : subgroup G).normalizer.normalizer = (↑P : subgroup G).normalizer :=
 begin
   have := normal_of_normalizer_normal (P.subtype (le_normalizer.trans le_normalizer)),
@@ -603,9 +609,9 @@ begin
   exact map_comap_eq_self (le_normalizer.trans (ge_of_eq (subtype_range _))),
 end
 
-lemma normal_of_all_max_subgroups_normal [fintype G]
+lemma normal_of_all_max_subgroups_normal [finite G]
   (hnc : ∀ (H : subgroup G), is_coatom H → H.normal)
-  {p : ℕ} [fact p.prime] [fintype (sylow p G)] (P : sylow p G) :
+  {p : ℕ} [fact p.prime] [finite (sylow p G)] (P : sylow p G) :
   (↑P : subgroup G).normal :=
 normalizer_eq_top.mp begin
   rcases eq_top_or_exists_le_coatom ((↑P : subgroup G).normalizer) with heq | ⟨K, hK, hNK⟩,
@@ -621,7 +627,7 @@ normalizer_eq_top.mp begin
 end
 
 lemma normal_of_normalizer_condition (hnc : normalizer_condition G)
- {p : ℕ} [fact p.prime] [fintype (sylow p G)] (P : sylow p G) :
+ {p : ℕ} [fact p.prime] [finite (sylow p G)] (P : sylow p G) :
  (↑P : subgroup G).normal :=
 normalizer_eq_top.mp $ normalizer_condition_iff_only_full_group_self_normalizing.mp hnc _ $
   normalizer_normalizer _
diff --git a/src/group_theory/torsion.lean b/src/group_theory/torsion.lean
index cdbda5bc76059..d68a355364f98 100644
--- a/src/group_theory/torsion.lean
+++ b/src/group_theory/torsion.lean
@@ -135,9 +135,9 @@ exponent_exists_iff_ne_zero.mpr $
   (exponent_ne_zero_iff_range_order_of_finite (λ g, order_of_pos' (tG g))).mpr bounded
 
 /-- Finite groups are torsion groups. -/
-@[to_additive is_add_torsion_of_fintype "Finite additive groups are additive torsion groups."]
-lemma is_torsion_of_fintype [fintype G] : is_torsion G :=
-exponent_exists.is_torsion $ exponent_exists_iff_ne_zero.mpr exponent_ne_zero_of_fintype
+@[to_additive is_add_torsion_of_finite "Finite additive groups are additive torsion groups."]
+lemma is_torsion_of_finite [finite G] : is_torsion G :=
+exponent_exists.is_torsion $ exponent_exists_iff_ne_zero.mpr exponent_ne_zero_of_finite
 
 end group
 
@@ -156,8 +156,8 @@ is_torsion M := λ f, (is_of_fin_add_order_iff_nsmul_eq_zero _).mpr $ begin
 end
 
 /-- A module with a finite ring of scalars is additively torsion. -/
-lemma is_torsion.module_of_fintype [ring R] [fintype R] [module R M] : is_torsion M :=
-(is_add_torsion_of_fintype : is_torsion R).module_of_torsion _ _
+lemma is_torsion.module_of_finite [ring R] [finite R] [module R M] : is_torsion M :=
+(is_add_torsion_of_finite : is_torsion R).module_of_torsion _ _
 
 end add_monoid
 
diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean
index cf98839b81982..d4b585cf250f1 100644
--- a/src/linear_algebra/determinant.lean
+++ b/src/linear_algebra/determinant.lean
@@ -486,7 +486,7 @@ map with respect to that basis, multiplied by the value of that alternating map
 lemma alternating_map.eq_smul_basis_det (f : alternating_map R M R ι) : f = f e • e.det :=
 begin
   refine basis.ext_alternating e (λ i h, _),
-  let σ : equiv.perm ι := equiv.of_bijective i (fintype.injective_iff_bijective.1 h),
+  let σ : equiv.perm ι := equiv.of_bijective i (finite.injective_iff_bijective.1 h),
   change f (e ∘ σ) = (f e • e.det) (e ∘ σ),
   simp [alternating_map.map_perm, basis.det_self]
 end
diff --git a/src/linear_algebra/matrix/determinant.lean b/src/linear_algebra/matrix/determinant.lean
index ed3bbdb4c5700..41c348c2bb706 100644
--- a/src/linear_algebra/matrix/determinant.lean
+++ b/src/linear_algebra/matrix/determinant.lean
@@ -125,7 +125,7 @@ lemma det_mul_aux {M N : matrix n n R} {p : n → n} (H : ¬bijective p) :
   ∑ σ : perm n, (ε σ) * ∏ x, (M (σ x) (p x) * N (p x) x) = 0 :=
 begin
   obtain ⟨i, j, hpij, hij⟩ : ∃ i j, p i = p j ∧ i ≠ j,
-  { rw [← fintype.injective_iff_bijective, injective] at H,
+  { rw [← finite.injective_iff_bijective, injective] at H,
     push_neg at H,
     exact H },
   exact sum_involution
diff --git a/src/order/atoms.lean b/src/order/atoms.lean
index b5d0d3b564794..a4281d76cac69 100644
--- a/src/order/atoms.lean
+++ b/src/order/atoms.lean
@@ -45,7 +45,7 @@ which are lattices with only two elements, and related ideas.
   * `is_compl.is_atom_iff_is_coatom` and `is_compl.is_coatom_if_is_atom`: In a modular
   bounded lattice, a complement of an atom is a coatom and vice versa.
   * `is_atomic_iff_is_coatomic`: A modular complemented lattice is atomic iff it is coatomic.
-  * `fintype.to_is_atomic`, `fintype.to_is_coatomic`: Finite partial orders with bottom resp. top
+  * `finite.to_is_atomic`, `finite.to_is_coatomic`: Finite partial orders with bottom resp. top
     are atomic resp. coatomic.
 
 -/
@@ -665,7 +665,7 @@ section fintype
 open finset
 
 @[priority 100]  -- see Note [lower instance priority]
-instance fintype.to_is_coatomic [partial_order α] [order_top α] [fintype α] : is_coatomic α :=
+instance finite.to_is_coatomic [partial_order α] [order_top α] [finite α] : is_coatomic α :=
 begin
   refine is_coatomic.mk (λ b, or_iff_not_imp_left.2 (λ ht, _)),
   obtain ⟨c, hc, hmax⟩ := set.finite.exists_maximal_wrt id { x : α | b ≤ x ∧ x ≠ ⊤ }
@@ -677,7 +677,7 @@ begin
 end
 
 @[priority 100]  -- see Note [lower instance priority]
-instance fintype.to_is_atomic [partial_order α] [order_bot α] [fintype α] : is_atomic α :=
-is_coatomic_dual_iff_is_atomic.mp fintype.to_is_coatomic
+instance finite.to_is_atomic [partial_order α] [order_bot α] [finite α] : is_atomic α :=
+is_coatomic_dual_iff_is_atomic.mp finite.to_is_coatomic
 
 end fintype
diff --git a/src/ring_theory/algebraic.lean b/src/ring_theory/algebraic.lean
index 8c6ca718ac655..d43cd89b05fb0 100644
--- a/src/ring_theory/algebraic.lean
+++ b/src/ring_theory/algebraic.lean
@@ -229,7 +229,7 @@ begin
   obtain ⟨p, hp, he⟩ := ha b,
   let f' : p.root_set L → p.root_set L :=
     set.maps_to.restrict f _ _ (root_set_maps_to (map_ne_zero hp) f),
-  have : function.surjective f' := fintype.injective_iff_surjective.1
+  have : function.surjective f' := finite.injective_iff_surjective.1
     (λ _ _ h, subtype.eq $ f.to_ring_hom.injective $ subtype.ext_iff.1 h),
   obtain ⟨a, ha⟩ := this ⟨b, (mem_root_set_iff hp b).2 he⟩,
   exact ⟨a, subtype.ext_iff.1 ha⟩,
diff --git a/src/ring_theory/artinian.lean b/src/ring_theory/artinian.lean
index f7268c73e48e8..d565adb36caf6 100644
--- a/src/ring_theory/artinian.lean
+++ b/src/ring_theory/artinian.lean
@@ -111,15 +111,14 @@ is_artinian_of_range_eq_ker
 
 @[priority 100]
 instance is_artinian_of_finite [finite M] : is_artinian R M :=
-let ⟨_⟩ := nonempty_fintype M in by exactI
-⟨fintype.well_founded_of_trans_of_irrefl _⟩
+⟨finite.well_founded_of_trans_of_irrefl _⟩
 
-local attribute [elab_as_eliminator] fintype.induction_empty_option
+local attribute [elab_as_eliminator] finite.induction_empty_option
 
-instance is_artinian_pi {R ι : Type*} [fintype ι] : Π {M : ι → Type*} [ring R]
+instance is_artinian_pi {R ι : Type*} [finite ι] : Π {M : ι → Type*} [ring R]
   [Π i, add_comm_group (M i)], by exactI Π [Π i, module R (M i)],
   by exactI Π [∀ i, is_artinian R (M i)], is_artinian R (Π i, M i) :=
-fintype.induction_empty_option
+finite.induction_empty_option
   (begin
     introsI α β e hα M _ _ _ _,
     exact is_artinian_of_linear_equiv
@@ -136,7 +135,7 @@ fintype.induction_empty_option
 /-- A version of `is_artinian_pi` for non-dependent functions. We need this instance because
 sometimes Lean fails to apply the dependent version in non-dependent settings (e.g., it fails to
 prove that `ι → ℝ` is finite dimensional over `ℝ`). -/
-instance is_artinian_pi' {R ι M : Type*} [ring R] [add_comm_group M] [module R M] [fintype ι]
+instance is_artinian_pi' {R ι M : Type*} [ring R] [add_comm_group M] [module R M] [finite ι]
   [is_artinian R M] : is_artinian R (ι → M) :=
 is_artinian_pi
 
diff --git a/src/ring_theory/integral_domain.lean b/src/ring_theory/integral_domain.lean
index aa57cd585aec2..90f9b905daf1d 100644
--- a/src/ring_theory/integral_domain.lean
+++ b/src/ring_theory/integral_domain.lean
@@ -35,18 +35,18 @@ open_locale big_operators nat
 
 section cancel_monoid_with_zero
 -- There doesn't seem to be a better home for these right now
-variables {M : Type*} [cancel_monoid_with_zero M] [fintype M]
+variables {M : Type*} [cancel_monoid_with_zero M] [finite M]
 
-lemma mul_right_bijective_of_fintype₀ {a : M} (ha : a ≠ 0) : bijective (λ b, a * b) :=
-fintype.injective_iff_bijective.1 $ mul_right_injective₀ ha
+lemma mul_right_bijective_of_finite₀ {a : M} (ha : a ≠ 0) : bijective (λ b, a * b) :=
+finite.injective_iff_bijective.1 $ mul_right_injective₀ ha
 
-lemma mul_left_bijective_of_fintype₀ {a : M} (ha : a ≠ 0) : bijective (λ b, b * a) :=
-fintype.injective_iff_bijective.1 $ mul_left_injective₀ ha
+lemma mul_left_bijective_of_finite₀ {a : M} (ha : a ≠ 0) : bijective (λ b, b * a) :=
+finite.injective_iff_bijective.1 $ mul_left_injective₀ ha
 
 /-- Every finite nontrivial cancel_monoid_with_zero is a group_with_zero. -/
 def fintype.group_with_zero_of_cancel (M : Type*) [cancel_monoid_with_zero M] [decidable_eq M]
   [fintype M] [nontrivial M] : group_with_zero M :=
-{ inv := λ a, if h : a = 0 then 0 else fintype.bij_inv (mul_right_bijective_of_fintype₀ h) 1,
+{ inv := λ a, if h : a = 0 then 0 else fintype.bij_inv (mul_right_bijective_of_finite₀ h) 1,
   mul_inv_cancel := λ a ha,
     by { simp [has_inv.inv, dif_neg ha], exact fintype.right_inverse_bij_inv _ _ },
   inv_zero := by { simp [has_inv.inv, dif_pos rfl] },
@@ -79,14 +79,16 @@ def fintype.field_of_domain (R) [comm_ring R] [is_domain R] [decidable_eq R] [fi
 { .. fintype.group_with_zero_of_cancel R,
   .. ‹comm_ring R› }
 
-lemma fintype.is_field_of_domain (R) [comm_ring R] [is_domain R] [fintype R] :
-  is_field R := @field.to_is_field R $ @@fintype.field_of_domain R _ _ (classical.dec_eq R) _
+lemma finite.is_field_of_domain (R) [comm_ring R] [is_domain R] [finite R] : is_field R :=
+by { casesI nonempty_fintype R,
+  exact @field.to_is_field R (@@fintype.field_of_domain R _ _ (classical.dec_eq R) _) }
 
 end ring
 
-variables [comm_ring R] [is_domain R] [group G] [fintype G]
+variables [comm_ring R] [is_domain R] [group G]
 
-lemma card_nth_roots_subgroup_units (f : G →* R) (hf : injective f) {n : ℕ} (hn : 0 < n) (g₀ : G) :
+lemma card_nth_roots_subgroup_units [fintype G] (f : G →* R) (hf : injective f) {n : ℕ} (hn : 0 < n)
+  (g₀ : G) :
   ({g ∈ univ | g ^ n = g₀} : finset G).card ≤ (nth_roots n (f g₀)).card :=
 begin
   haveI : decidable_eq R := classical.dec_eq _,
@@ -99,9 +101,10 @@ begin
 end
 
 /-- A finite subgroup of the unit group of an integral domain is cyclic. -/
-lemma is_cyclic_of_subgroup_is_domain (f : G →* R) (hf : injective f) : is_cyclic G :=
+lemma is_cyclic_of_subgroup_is_domain [finite G] (f : G →* R) (hf : injective f) : is_cyclic G :=
 begin
   classical,
+  casesI nonempty_fintype G,
   apply is_cyclic_of_card_pow_eq_one_le,
   intros n hn,
   convert (le_trans (card_nth_roots_subgroup_units f hf hn 1) (card_nth_roots n (f 1)))
@@ -110,13 +113,13 @@ end
 /-- The unit group of a finite integral domain is cyclic.
 
 To support `ℤˣ` and other infinite monoids with finite groups of units, this requires only
-`fintype Rˣ` rather than deducing it from `fintype R`. -/
-instance [fintype Rˣ] : is_cyclic Rˣ :=
+`finite Rˣ` rather than deducing it from `finite R`. -/
+instance [finite Rˣ] : is_cyclic Rˣ :=
 is_cyclic_of_subgroup_is_domain (units.coe_hom R) $ units.ext
 
 section
 
-variables (S : subgroup Rˣ) [fintype S]
+variables (S : subgroup Rˣ) [finite S]
 
 /-- A finite subgroup of the units of an integral domain is cyclic. -/
 instance subgroup_units_cyclic : is_cyclic S :=
@@ -129,6 +132,8 @@ end
 
 end
 
+variables [fintype G]
+
 lemma card_fiber_eq_of_mem_range {H : Type*} [group H] [decidable_eq H]
   (f : G →* H) {x y : H} (hx : x ∈ set.range f) (hy : y ∈ set.range f) :
   (univ.filter $ λ g, f g = x).card = (univ.filter $ λ g, f g = y).card :=
diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean
index 04449d9b69cf8..8583fd931b065 100644
--- a/src/set_theory/cardinal/basic.lean
+++ b/src/set_theory/cardinal/basic.lean
@@ -314,7 +314,7 @@ mk_congr ((equiv.ulift).symm.sum_congr (equiv.ulift).symm)
 
 @[simp] lemma mk_fintype (α : Type u) [fintype α] : #α = fintype.card α :=
 begin
-  refine fintype.induction_empty_option' _ _ _ α,
+  refine fintype.induction_empty_option _ _ _ α,
   { introsI α β h e hα, letI := fintype.of_equiv β e.symm,
     rwa [mk_congr e, fintype.card_congr e] at hα },
   { refl },
diff --git a/src/topology/noetherian_space.lean b/src/topology/noetherian_space.lean
index a63d323cbbfa3..7806a0c6a7bb7 100644
--- a/src/topology/noetherian_space.lean
+++ b/src/topology/noetherian_space.lean
@@ -167,11 +167,7 @@ end
 
 @[priority 100]
 instance finite.to_noetherian_space [finite α] : noetherian_space α :=
-begin
-  casesI nonempty_fintype α,
-  classical,
-  exact ⟨@@fintype.well_founded_of_trans_of_irrefl (subtype.fintype _) _ _ _⟩
-end
+⟨finite.well_founded_of_trans_of_irrefl _⟩
 
 lemma noetherian_space.exists_finset_irreducible [noetherian_space α] (s : closeds α) :
   ∃ S : finset (closeds α), (∀ k : S, is_irreducible (k : set α)) ∧ s = S.sup id :=
diff --git a/src/topology/sets/opens.lean b/src/topology/sets/opens.lean
index d1c609ee5179b..0a8fd73565891 100644
--- a/src/topology/sets/opens.lean
+++ b/src/topology/sets/opens.lean
@@ -267,4 +267,6 @@ def open_nhds_of (x : α) : Type* := { s : set α // is_open s ∧ x ∈ s }
 instance open_nhds_of.inhabited {α : Type*} [topological_space α] (x : α) :
   inhabited (open_nhds_of x) := ⟨⟨set.univ, is_open_univ, set.mem_univ _⟩⟩
 
+instance [finite α] : finite (opens α) := subtype.finite
+
 end topological_space