chore: fix more unused decidable instances in types (#32153)

Found by #31747. After this, we should be able to turn on the unused decidable in type linter by default.

Author: thorimur

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -190,8 +190,9 @@ theorem isTree_iff_existsUnique_path :
 lemma IsTree.existsUnique_path (hG : G.IsTree) : ∀ v w, ∃! p : G.Walk v w, p.IsPath :=
   (isTree_iff_existsUnique_path.1 hG).2
 
-theorem IsAcyclic.isPath_iff_isChain [DecidableEq V] (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) :
+theorem IsAcyclic.isPath_iff_isChain (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) :
      p.IsPath ↔ List.IsChain (· ≠ ·) p.edges := by
+  classical
   refine ⟨fun h ↦ (edges_nodup_of_support_nodup <| p.isPath_def.mp h).isChain, fun h ↦ ?_⟩
   induction p with
   | nil => simp
@@ -214,7 +215,7 @@ theorem IsAcyclic.isPath_iff_isChain [DecidableEq V] (hG : G.IsAcyclic) {v w : V
       have := IsPath.mk' this |>.eq_snd_of_mem_edges (by simp [head.ne.symm]) (Sym2.eq_swap ▸ hhh)
       simp [this, snd_takeUntil head.ne]
 
-theorem IsAcyclic.isPath_iff_isTrail [DecidableEq V] (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) :
+theorem IsAcyclic.isPath_iff_isTrail (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) :
     p.IsPath ↔ p.IsTrail :=
   ⟨IsPath.isTrail, fun h ↦ hG.isPath_iff_isChain p |>.mpr <| p.isTrail_def.mp h |>.isChain⟩
 

Mathlib/Data/Finsupp/Sigma.lean

@@ -116,11 +116,10 @@ end EmbSigmaAdd
 
 section EmbSigmaSingle
 
-variable [Zero M] [DecidableEq κ] [∀ k, DecidableEq (ι k)]
-
 @[simp]
-theorem embSigma_single {k : κ} (i : ι k) (m : M) :
+theorem embSigma_single [Zero M] {k : κ} (i : ι k) (m : M) :
     embSigma (single i m) = single ⟨k, i⟩ m := by
+  classical
   ext ⟨k', j⟩
   by_cases hk : k' = k
   · subst hk