diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
index e8dd715e3ea3be..b3863017dc3f63 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Clique.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
@@ -546,7 +546,6 @@ lemma CliqueFree.mem_of_sup_edge_isNClique {x y : α} {t : Finset α} {n : ℕ}
   have ht : (t : Set α) \ {x} = t := sdiff_eq_left.mpr <| Set.disjoint_singleton_right.mpr hf
   exact h t ⟨ht ▸ hc.1.sdiff_of_sup_edge, hc.2⟩
 
-open scoped Classical in
 /-- Adding an edge increases the clique number by at most one. -/
 protected theorem CliqueFree.sup_edge (h : G.CliqueFree n) (v w : α) :
     (G ⊔ edge v w).CliqueFree (n + 1) := by
diff --git a/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean b/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean
index cee815e014b520..3243f8425492a4 100644
--- a/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean
+++ b/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean
@@ -114,7 +114,6 @@ is the smallest natural number `e` such that `a ^ ringExpChar K ^ e ∈ K`. -/
 noncomputable def elemExponent (a : L) : ℕ :=
   Nat.find <| minpoly_eq_X_pow_sub_C K (ringExpChar K) a
 
-open scoped Classical in
 variable {K} in
 theorem elemExponent_eq_zero_of_mem_range {a : L} (h : a ∈ (algebraMap K L).range) :
     elemExponent K a = 0 := by
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
index 7da4f53aa81781..dcf939ca237774 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
@@ -533,7 +533,6 @@ theorem logMap_expMapBasis (x : realSpace K) :
     logMap (mixedSpaceOfRealSpace (expMapBasis x)) ∈
         ZSpan.fundamentalDomain ((basisUnitLattice K).ofZLatticeBasis ℝ (unitLattice K))
       ↔ ∀ w, w ≠ w₀ → x w ∈ Set.Ico 0 1 := by
-  classical
   simp_rw [ZSpan.mem_fundamentalDomain, equivFinRank.forall_congr_left, Subtype.forall]
   refine forall₂_congr fun w hw ↦ ?_
   rw [expMapBasis_apply'', map_smul, logMap_real_smul (norm_expMapBasis_ne_zero _)
diff --git a/Mathlib/RingTheory/DedekindDomain/Different.lean b/Mathlib/RingTheory/DedekindDomain/Different.lean
index 88a9307503810b..8637e97f1922c2 100644
--- a/Mathlib/RingTheory/DedekindDomain/Different.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Different.lean
@@ -112,7 +112,6 @@ open scoped Classical in
 lemma traceDual_top' :
     (⊤ : Submodule B L)ᵛ =
       if ((LinearMap.range (Algebra.trace K L)).restrictScalars A ≤ 1) then ⊤ else ⊥ := by
-  classical
   split_ifs with h
   · rw [_root_.eq_top_iff]
     exact fun _ _ _ _ ↦ h ⟨_, rfl⟩
@@ -224,11 +223,11 @@ variable [IsDomain A] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B]
 
 namespace FractionalIdeal
 
-open scoped Classical in
 /-- The dual of a non-zero fractional ideal is the dual of the submodule under the trace form. -/
 noncomputable
 def dual (I : FractionalIdeal B⁰ L) :
     FractionalIdeal B⁰ L :=
+  open scoped Classical in
   if hI : I = 0 then 0 else
   ⟨Iᵛ, by
     classical
diff --git a/Mathlib/RingTheory/Extension/Presentation/Submersive.lean b/Mathlib/RingTheory/Extension/Presentation/Submersive.lean
index 8ade816775c620..60e65585343dde 100644
--- a/Mathlib/RingTheory/Extension/Presentation/Submersive.lean
+++ b/Mathlib/RingTheory/Extension/Presentation/Submersive.lean
@@ -297,7 +297,6 @@ variable [Fintype σ] [Fintype σ']
 open scoped Classical in
 private lemma jacobiMatrix_comp_inl_inr (i : σ') (j : σ) :
     (Q.comp P).jacobiMatrix (Sum.inl i) (Sum.inr j) = 0 := by
-  classical
   rw [jacobiMatrix_apply]
   refine MvPolynomial.pderiv_eq_zero_of_notMem_vars (fun hmem ↦ ?_)
   apply MvPolynomial.vars_rename at hmem