diff --git a/Mathlib/Algebra/BigOperators/Ring.lean b/Mathlib/Algebra/BigOperators/Ring.lean
index 5525f5782fdae7..c613a77696db9c 100644
--- a/Mathlib/Algebra/BigOperators/Ring.lean
+++ b/Mathlib/Algebra/BigOperators/Ring.lean
@@ -73,12 +73,13 @@ section CommSemiring
 variable [CommSemiring α]
 
 section DecidableEq
-variable [DecidableEq ι] [∀ i, DecidableEq (κ i)]
+variable [DecidableEq ι]
 
 /-- The product over a sum can be written as a sum over the product of sets, `Finset.Pi`.
   `Finset.prod_univ_sum` is an alternative statement when the product is over `univ`. -/
 lemma prod_sum (s : Finset ι) (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → α) :
     ∏ a in s, ∑ b in t a, f a b = ∑ p in s.pi t, ∏ x in s.attach, f x.1 (p x.1 x.2) := by
+  classical
   induction' s using Finset.induction with a s ha ih
   · rw [pi_empty, sum_singleton]
     rfl
@@ -121,7 +122,7 @@ lemma sum_prod_piFinset {κ : Type*} [Fintype ι] (s : Finset κ) (g : ι → κ
 
 lemma sum_pow' (s : Finset ι) (f : ι → α) (n : ℕ) :
     (∑ a in s, f a) ^ n = ∑ p in piFinset fun _i : Fin n ↦ s, ∏ i, f (p i) := by
-  classical convert @prod_univ_sum (Fin n) _ _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d; simp
+  classical convert @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d; simp
 
 /-- The product of `f a + g a` over all of `s` is the sum over the powerset of `s` of the product of
 `f` over a subset `t` times the product of `g` over the complement of `t`  -/
diff --git a/Mathlib/LinearAlgebra/DFinsupp.lean b/Mathlib/LinearAlgebra/DFinsupp.lean
index c44481084e4a59..acd6405f2002af 100644
--- a/Mathlib/LinearAlgebra/DFinsupp.lean
+++ b/Mathlib/LinearAlgebra/DFinsupp.lean
@@ -37,14 +37,16 @@ function with finite support, module, linear algebra
 
 variable {ι : Type*} {R : Type*} {S : Type*} {M : ι → Type*} {N : Type*}
 
-variable [dec_ι : DecidableEq ι]
-
 namespace DFinsupp
 
 variable [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
 
 variable [AddCommMonoid N] [Module R N]
 
+section DecidableEq
+
+variable [DecidableEq ι]
+
 /-- `DFinsupp.mk` as a `LinearMap`. -/
 def lmk (s : Finset ι) : (∀ i : (↑s : Set ι), M i) →ₗ[R] Π₀ i, M i where
   toFun := mk s
@@ -137,8 +139,7 @@ def lsum [Semiring S] [Module S N] [SMulCommClass R S N] :
     (∀ i, M i →ₗ[R] N) ≃ₗ[S] (Π₀ i, M i) →ₗ[R] N where
   toFun F :=
     { toFun := sumAddHom fun i => (F i).toAddMonoidHom
-      -- Porting note: needed to (β := M) hint below
-      map_add' := (DFinsupp.liftAddHom (β := M) (fun (i : ι) => (F i).toAddMonoidHom)).map_add
+      map_add' := (DFinsupp.liftAddHom fun (i : ι) => (F i).toAddMonoidHom).map_add
       map_smul' := fun c f => by
         dsimp
         apply DFinsupp.induction f
@@ -174,12 +175,13 @@ theorem lsum_single [Semiring S] [Module S N] [SMulCommClass R S N] (F : ∀ i,
 
 end Lsum
 
+end DecidableEq
+
 /-! ### Bundled versions of `DFinsupp.mapRange`
 
 The names should match the equivalent bundled `Finsupp.mapRange` definitions.
 -/
 
-
 section mapRange
 
 variable {β β₁ β₂ : ι → Type*}
@@ -217,13 +219,10 @@ theorem mapRange.linearMap_comp (f : ∀ i, β₁ i →ₗ[R] β₂ i) (f₂ : 
     (fun i => (f i).map_zero) (fun i => (f₂ i).map_zero) (by simp)
 #align dfinsupp.map_range.linear_map_comp DFinsupp.mapRange.linearMap_comp
 
-theorem sum_mapRange_index.linearMap [∀ (i : ι) (x : β₁ i), Decidable (x ≠ 0)]
-    [∀ (i : ι) (x : β₂ i), Decidable (x ≠ 0)] {f : ∀ i, β₁ i →ₗ[R] β₂ i} {h : ∀ i, β₂ i →ₗ[R] N}
-    {l : Π₀ i, β₁ i} :
-    -- Porting note: Needed to add (M := ...) below
-    (DFinsupp.lsum ℕ (M := β₂)) h (mapRange.linearMap f l)
-      = (DFinsupp.lsum ℕ (M := β₁)) (fun i => (h i).comp (f i)) l := by
-  simpa [DFinsupp.sumAddHom_apply] using sum_mapRange_index fun i => by simp
+theorem sum_mapRange_index.linearMap [DecidableEq ι] {f : ∀ i, β₁ i →ₗ[R] β₂ i}
+    {h : ∀ i, β₂ i →ₗ[R] N} {l : Π₀ i, β₁ i} :
+    DFinsupp.lsum ℕ h (mapRange.linearMap f l) = DFinsupp.lsum ℕ (fun i => (h i).comp (f i)) l := by
+  classical simpa [DFinsupp.sumAddHom_apply] using sum_mapRange_index fun i => by simp
 #align dfinsupp.sum_map_range_index.linear_map DFinsupp.sum_mapRange_index.linearMap
 
 /-- `DFinsupp.mapRange.linearMap` as a `LinearEquiv`. -/
@@ -289,6 +288,10 @@ variable [Semiring R] [AddCommMonoid N] [Module R N]
 
 open DFinsupp
 
+section DecidableEq
+
+variable [DecidableEq ι]
+
 theorem dfinsupp_sum_mem {β : ι → Type*} [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
     (S : Submodule R N) (f : Π₀ i, β i) (g : ∀ i, β i → N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) :
     f.sum g ∈ S :=
@@ -356,6 +359,16 @@ theorem mem_iSup_iff_exists_dfinsupp' (p : ι → Submodule R N) [∀ (i) (x : p
     LinearMap.toAddMonoidHom_coe, coeSubtype]
 #align submodule.mem_supr_iff_exists_dfinsupp' Submodule.mem_iSup_iff_exists_dfinsupp'
 
+theorem mem_biSup_iff_exists_dfinsupp (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N)
+    (x : N) :
+    (x ∈ ⨆ (i) (_ : p i), S i) ↔
+      ∃ f : Π₀ i, S i,
+        DFinsupp.lsum ℕ (M := fun i ↦ ↥(S i)) (fun i => (S i).subtype) (f.filter p) = x :=
+  SetLike.ext_iff.mp (biSup_eq_range_dfinsupp_lsum p S) x
+#align submodule.mem_bsupr_iff_exists_dfinsupp Submodule.mem_biSup_iff_exists_dfinsupp
+
+end DecidableEq
+
 lemma mem_iSup_iff_exists_finsupp (p : ι → Submodule R N) (x : N) :
     x ∈ iSup p ↔ ∃ (f : ι →₀ N), (∀ i, f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x := by
   classical
@@ -366,14 +379,6 @@ lemma mem_iSup_iff_exists_finsupp (p : ι → Submodule R N) (x : N) :
   · ext; simp
   · simp [Finsupp.mem_support_iff.mp hi]
 
-theorem mem_biSup_iff_exists_dfinsupp (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N)
-    (x : N) :
-    (x ∈ ⨆ (i) (_ : p i), S i) ↔
-      ∃ f : Π₀ i, S i,
-        DFinsupp.lsum ℕ (M := fun i ↦ ↥(S i)) (fun i => (S i).subtype) (f.filter p) = x :=
-  SetLike.ext_iff.mp (biSup_eq_range_dfinsupp_lsum p S) x
-#align submodule.mem_bsupr_iff_exists_dfinsupp Submodule.mem_biSup_iff_exists_dfinsupp
-
 open BigOperators
 
 theorem mem_iSup_finset_iff_exists_sum {s : Finset ι} (p : ι → Submodule R N) (a : N) :
@@ -421,7 +426,7 @@ open DFinsupp
 
 section Semiring
 
-variable [Semiring R] [AddCommMonoid N] [Module R N]
+variable [DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N]
 
 /-- Independence of a family of submodules can be expressed as a quantifier over `DFinsupp`s.
 
@@ -477,7 +482,7 @@ end Semiring
 
 section Ring
 
-variable [Ring R] [AddCommGroup N] [Module R N]
+variable [DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N]
 
 /- If `DFinsupp.sumAddHom` applied with `AddSubmonoid.subtype` is injective then the additive
 subgroups are independent. -/
diff --git a/Mathlib/LinearAlgebra/Matrix/PosDef.lean b/Mathlib/LinearAlgebra/Matrix/PosDef.lean
index 087e3c9586d139..bdc7c71d1a8d24 100644
--- a/Mathlib/LinearAlgebra/Matrix/PosDef.lean
+++ b/Mathlib/LinearAlgebra/Matrix/PosDef.lean
@@ -262,8 +262,9 @@ lemma eigenvalues_self_mul_conjTranspose_nonneg (A : Matrix m n 𝕜) [Decidable
   (posSemidef_self_mul_conjTranspose _).eigenvalues_nonneg _
 
 /-- A matrix is positive semidefinite if and only if it has the form `Bᴴ * B` for some `B`. -/
-lemma posSemidef_iff_eq_transpose_mul_self [DecidableEq n] {A : Matrix n n 𝕜} :
+lemma posSemidef_iff_eq_transpose_mul_self {A : Matrix n n 𝕜} :
     PosSemidef A ↔ ∃ (B : Matrix n n 𝕜), A = Bᴴ * B := by
+  classical
   refine ⟨fun hA ↦ ⟨hA.sqrt, ?_⟩, fun ⟨B, hB⟩ ↦ (hB ▸ posSemidef_conjTranspose_mul_self B)⟩
   simp_rw [← PosSemidef.sq_sqrt hA, pow_two]
   rw [hA.posSemidef_sqrt.1]
@@ -276,7 +277,7 @@ lemma IsHermitian.posSemidef_of_eigenvalues_nonneg [DecidableEq n] {A : Matrix n
   simpa using h i
 
 /-- For `A` positive semidefinite, we have `x⋆ A x = 0` iff `A x = 0`. -/
-theorem PosSemidef.dotProduct_mulVec_zero_iff [DecidableEq n]
+theorem PosSemidef.dotProduct_mulVec_zero_iff
     {A : Matrix n n 𝕜} (hA : PosSemidef A) (x : n → 𝕜) :
     star x ⬝ᵥ mulVec A x = 0 ↔ mulVec A x = 0 := by
   constructor
diff --git a/Mathlib/LinearAlgebra/Matrix/Spectrum.lean b/Mathlib/LinearAlgebra/Matrix/Spectrum.lean
index b9ae79079ebba5..334b7548535da4 100644
--- a/Mathlib/LinearAlgebra/Matrix/Spectrum.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Spectrum.lean
@@ -24,16 +24,18 @@ spectral theorem, diagonalization theorem
 
 namespace Matrix
 
-variable {𝕜 : Type*} [IsROrC 𝕜] {n : Type*} [Fintype n] [DecidableEq n]
+variable {𝕜 : Type*} [IsROrC 𝕜] {n : Type*} [Fintype n]
 
 variable {A : Matrix n n 𝕜}
 
-open scoped Matrix
-
 open scoped BigOperators
 
 namespace IsHermitian
 
+section DecidableEq
+
+variable [DecidableEq n]
+
 variable (hA : A.IsHermitian)
 
 /-- The eigenvalues of a hermitian matrix, indexed by `Fin (Fintype.card n)` where `n` is the index
@@ -172,9 +174,12 @@ lemma mulVec_eigenvectorBasis (i : n) :
   convert this using 1
   rw [mul_comm, Pi.smul_apply, IsROrC.real_smul_eq_coe_mul, hA.eigenvectorMatrix_apply]
 
+end DecidableEq
+
 /-- A nonzero Hermitian matrix has an eigenvector with nonzero eigenvalue. -/
-lemma exists_eigenvector_of_ne_zero (h_ne : A ≠ 0) :
+lemma exists_eigenvector_of_ne_zero (hA : IsHermitian A) (h_ne : A ≠ 0) :
     ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ mulVec A v = t • v := by
+  classical
   have : hA.eigenvalues ≠ 0
   · contrapose! h_ne
     have := hA.spectral_theorem'
diff --git a/Mathlib/Tactic/NormNum/BigOperators.lean b/Mathlib/Tactic/NormNum/BigOperators.lean
index a86608ae47dc32..552683704cff8e 100644
--- a/Mathlib/Tactic/NormNum/BigOperators.lean
+++ b/Mathlib/Tactic/NormNum/BigOperators.lean
@@ -171,9 +171,9 @@ def Multiset.ProveZeroOrConsResult.eq_trans {α : Q(Type u)} {s t : Q(Multiset $
   | .zero pf => .zero q(Eq.trans $eq $pf)
   | .cons a s' pf => .cons a s' q(Eq.trans $eq $pf)
 
-lemma Multiset.insert_eq_cons {α : Type*} [DecidableEq α] (a : α) (s : Multiset α) :
-    insert a s = Multiset.cons a s := by
-  ext; simp
+lemma Multiset.insert_eq_cons {α : Type*} (a : α) (s : Multiset α) :
+    insert a s = Multiset.cons a s :=
+  rfl
 
 lemma Multiset.range_zero' {n : ℕ} (pn : NormNum.IsNat n 0) :
     Multiset.range n = 0 := by rw [pn.out, Nat.cast_zero, Multiset.range_zero]