diff --git a/Mathlib/Algebra/BigOperators/Ring/Nat.lean b/Mathlib/Algebra/BigOperators/Ring/Nat.lean
index a885e482d7318c..c9a30d36780429 100644
--- a/Mathlib/Algebra/BigOperators/Ring/Nat.lean
+++ b/Mathlib/Algebra/BigOperators/Ring/Nat.lean
@@ -30,9 +30,10 @@ lemma odd_sum_iff_odd_card_odd {s : Finset ι} (f : ι → ℕ) :
     Odd (∑ i ∈ s, f i) ↔ Odd #{x ∈ s | Odd (f x)} := by
   simp only [← Nat.not_even_iff_odd, even_sum_iff_even_card_odd]
 
-theorem card_preimage_eq_sum_card_image_eq {M : Type*} [DecidableEq M] {f : ι → M} {s : Finset M}
+theorem card_preimage_eq_sum_card_image_eq {M : Type*} {f : ι → M} {s : Finset M}
     (hb : ∀ b ∈ s, Set.Finite {a | f a = b}) :
     Nat.card (f⁻¹' s) = ∑ b ∈ s, Nat.card {a // f a = b} := by
+  classical
   -- `t = s ∩ Set.range f` as a `Finset`
   let t := (Set.finite_coe_iff.mp (Finite.Set.finite_inter_of_left ↑s (Set.range f))).toFinset
   rw [show Nat.card (f⁻¹' s) = Nat.card (f⁻¹' t) by simp [t]]
diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean
index 357698b8ba756b..2bff5db041c2a1 100644
--- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean
+++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean
@@ -191,13 +191,14 @@ theorem valuativeCriterion_existence_aux
     {O : Type*} [CommRing O] [IsDomain O] [ValuationRing O]
     {K : Type*} [Field K] [Algebra O K] [IsFractionRing O K]
     (φ₀ : (𝒜 0) →+* O)
-    (ι : Type*) [Fintype ι] (x : ι → A) (h2 : Algebra.adjoin (𝒜 0) (Set.range x) = ⊤)
+    (ι : Type*) [Finite ι] (x : ι → A) (h2 : Algebra.adjoin (𝒜 0) (Set.range x) = ⊤)
     (j : ι) (φ : Away 𝒜 (x j) →+* K)
     (hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 _))
     (d : ι → ℕ) (hdi : ∀ i, 0 < d i) (hxdi : ∀ i, x i ∈ 𝒜 (d i)) :
     ∃ (j₀ : ι) (φ' : Away 𝒜 (x j * x j₀) →+* K), φ'.comp (awayMap 𝒜 (hxdi j₀) rfl) = φ ∧
       (φ'.comp (awayMap 𝒜 (hxdi j) (mul_comm (x j) (x j₀)))).range ≤ (algebraMap O K).range := by
   classical
+  cases nonempty_fintype ι
   let ψ (i : ι) : ValueGroup O K :=
     valuation O K ((φ (Away.isLocalizationElem (hxdi j) (hxdi i))) ^ ∏ k ∈ Finset.univ.erase i, d k)
   have : Nonempty ι := ⟨j⟩
diff --git a/Mathlib/Combinatorics/SimpleGraph/Tutte.lean b/Mathlib/Combinatorics/SimpleGraph/Tutte.lean
index 0330044d03042d..d09d407176ff47 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Tutte.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Tutte.lean
@@ -52,7 +52,7 @@ private lemma tutte_exists_isAlternating_isCycles {x b a c : V} {M : Subgraph (G
   · simp +contextual [hnpxb, edge_adj, hnab.symm]
   · simpa [edge_adj, adj_congr_of_sym2 _ ((adj_edge _ _).mp hvw).1.symm] using .inl hgadj
 
-variable [Fintype V]
+variable [Finite V]
 
 lemma IsTutteViolator.mono {u : Set V} (h : G ≤ G') (ht : G'.IsTutteViolator u) :
     G.IsTutteViolator u := by
@@ -120,6 +120,7 @@ theorem Subgraph.IsPerfectMatching.exists_of_isClique_supp
       G.deleteUniversalVerts.coe.IsClique K.supp) :
     ∃ (M : Subgraph G), M.IsPerfectMatching := by
   classical
+  cases nonempty_fintype V
   obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
   obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
     (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
@@ -269,6 +270,7 @@ lemma exists_isTutteViolator (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching)
     (hvEven : Even (Nat.card V)) :
     ∃ u, G.IsTutteViolator u := by
   classical
+  cases nonempty_fintype V
   -- It suffices to consider the edge-maximal case
   obtain ⟨Gmax, hSubgraph, hMatchingFree, hMaximal⟩ := exists_maximal_isMatchingFree h
   refine ⟨Gmax.universalVerts, .mono hSubgraph ?_⟩
diff --git a/Mathlib/LinearAlgebra/Dual/Lemmas.lean b/Mathlib/LinearAlgebra/Dual/Lemmas.lean
index d9e0b9e81a0765..3d7fc036195e7d 100644
--- a/Mathlib/LinearAlgebra/Dual/Lemmas.lean
+++ b/Mathlib/LinearAlgebra/Dual/Lemmas.lean
@@ -105,8 +105,7 @@ variable {R : Type uR} {M : Type uM} {K : Type uK} {V : Type uV} {ι : Type uι}
 
 section CommSemiring
 
-variable [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι]
-variable (b : Basis ι R M)
+variable [CommSemiring R] [AddCommMonoid M] [Module R M]
 
 section Finite