diff --git a/Archive/Imo/Imo1998Q2.lean b/Archive/Imo/Imo1998Q2.lean
index 94378d663c520..88e40d89763aa 100644
--- a/Archive/Imo/Imo1998Q2.lean
+++ b/Archive/Imo/Imo1998Q2.lean
@@ -39,9 +39,6 @@ the lower bound: `a(b-1)^2/2 ≤ |A|`.
 Rearranging gives the result.
 -/
 
-
-open scoped Classical
-
 variable {C J : Type*} (r : C → J → Prop)
 
 namespace Imo1998Q2
@@ -86,6 +83,7 @@ theorem JudgePair.agree_iff_same_rating (p : JudgePair J) (c : C) :
     p.Agree r c ↔ (r c p.judge₁ ↔ r c p.judge₂) :=
   Iff.rfl
 
+open scoped Classical in
 /-- The set of contestants on which two judges agree. -/
 def agreedContestants [Fintype C] (p : JudgePair J) : Finset C :=
   Finset.univ.filter fun c => p.Agree r c
@@ -93,14 +91,17 @@ section
 
 variable [Fintype J] [Fintype C]
 
+open scoped Classical in
 /-- All incidences of agreement. -/
 def A : Finset (AgreedTriple C J) :=
   Finset.univ.filter @fun (a : AgreedTriple C J) =>
     (a.judgePair.Agree r a.contestant ∧ a.judgePair.Distinct)
 
+open scoped Classical in
 theorem A_maps_to_offDiag_judgePair (a : AgreedTriple C J) :
     a ∈ A r → a.judgePair ∈ Finset.offDiag (@Finset.univ J _) := by simp [A, Finset.mem_offDiag]
 
+open scoped Classical in
 theorem A_fibre_over_contestant (c : C) :
     (Finset.univ.filter fun p : JudgePair J => p.Agree r c ∧ p.Distinct) =
       ((A r).filter fun a : AgreedTriple C J => a.contestant = c).image Prod.snd := by
@@ -110,6 +111,7 @@ theorem A_fibre_over_contestant (c : C) :
   · rintro ⟨_, h₂⟩; refine ⟨(c, p), ?_⟩; tauto
   · intro h; aesop
 
+open scoped Classical in
 theorem A_fibre_over_contestant_card (c : C) :
     (Finset.univ.filter fun p : JudgePair J => p.Agree r c ∧ p.Distinct).card =
       ((A r).filter fun a : AgreedTriple C J => a.contestant = c).card := by
@@ -119,6 +121,7 @@ theorem A_fibre_over_contestant_card (c : C) :
   rintro ⟨a, p⟩ h ⟨a', p'⟩ h' rfl
   aesop (add simp AgreedTriple.contestant)
 
+open scoped Classical in
 theorem A_fibre_over_judgePair {p : JudgePair J} (h : p.Distinct) :
     agreedContestants r p = ((A r).filter fun a : AgreedTriple C J => a.judgePair = p).image
     AgreedTriple.contestant := by
@@ -126,6 +129,7 @@ theorem A_fibre_over_judgePair {p : JudgePair J} (h : p.Distinct) :
   · rw [Finset.mem_image]; refine ⟨⟨c, p⟩, ?_⟩; aesop
   · aesop
 
+open scoped Classical in
 theorem A_fibre_over_judgePair_card {p : JudgePair J} (h : p.Distinct) :
     (agreedContestants r p).card =
       ((A r).filter fun a : AgreedTriple C J => a.judgePair = p).card := by
@@ -138,6 +142,7 @@ theorem A_card_upper_bound {k : ℕ}
     (hk : ∀ p : JudgePair J, p.Distinct → (agreedContestants r p).card ≤ k) :
     (A r).card ≤ k * (Fintype.card J * Fintype.card J - Fintype.card J) := by
   change _ ≤ k * (Finset.card _ * Finset.card _ - Finset.card _)
+  classical
   rw [← Finset.offDiag_card]
   apply Finset.card_le_mul_card_image_of_maps_to (A_maps_to_offDiag_judgePair r)
   intro p hp
@@ -162,6 +167,7 @@ section
 
 variable [Fintype J]
 
+open scoped Classical in
 theorem judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) (c : C) :
     2 * z * z + 2 * z + 1 ≤ (Finset.univ.filter fun p : JudgePair J => p.Agree r c).card := by
   let x := (Finset.univ.filter fun j => r c j).card
@@ -173,6 +179,7 @@ theorem judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1)
   suffices x + y = 2 * z + 1 by simp [← Int.ofNat_add, this]
   rw [Finset.filter_card_add_filter_neg_card_eq_card, ← hJ]; rfl
 
+open scoped Classical in
 theorem distinct_judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) (c : C) :
     2 * z * z ≤ (Finset.univ.filter fun p : JudgePair J => p.Agree r c ∧ p.Distinct).card := by
   let s := Finset.univ.filter fun p : JudgePair J => p.Agree r c
@@ -192,6 +199,7 @@ theorem distinct_judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2
 
 theorem A_card_lower_bound [Fintype C] {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) :
     2 * z * z * Fintype.card C ≤ (A r).card := by
+  classical
   have h : ∀ a, a ∈ A r → Prod.fst a ∈ @Finset.univ C _ := by intros; apply Finset.mem_univ
   apply Finset.mul_card_image_le_card_of_maps_to h
   intro c _
diff --git a/Archive/Wiedijk100Theorems/FriendshipGraphs.lean b/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
index b4e7f16d0b902..c5d0604033257 100644
--- a/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
+++ b/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
@@ -38,8 +38,6 @@ be phrased in terms of counting walks.
 
 -/
 
-open scoped Classical
-
 namespace Theorems100
 
 noncomputable section
@@ -54,6 +52,7 @@ section FriendshipDef
 
 variable (G : SimpleGraph V)
 
+open scoped Classical in
 /-- This property of a graph is the hypothesis of the friendship theorem:
 every pair of nonadjacent vertices has exactly one common friend,
 a vertex to which both are adjacent.
@@ -74,6 +73,7 @@ namespace Friendship
 
 variable (R)
 
+open scoped Classical in
 include hG in
 /-- One characterization of a friendship graph is that there is exactly one walk of length 2
   between distinct vertices. These walks are counted in off-diagonal entries of the square of
@@ -86,6 +86,7 @@ theorem adjMatrix_sq_of_ne {v w : V} (hvw : v ≠ w) :
     Fintype.card_ofFinset (s := filter (fun x ↦ x ∈ G.neighborSet v ∩ G.neighborSet w) univ),
     Set.mem_inter_iff, mem_neighborSet]
 
+open scoped Classical in
 include hG in
 /-- This calculation amounts to counting the number of length 3 walks between nonadjacent vertices.
   We use it to show that nonadjacent vertices have equal degrees. -/
@@ -101,6 +102,7 @@ theorem adjMatrix_pow_three_of_not_adj {v w : V} (non_adj : ¬G.Adj v w) :
 
 variable {R}
 
+open scoped Classical in
 include hG in
 /-- As `v` and `w` not being adjacent implies
   `degree G v = ((G.adjMatrix R) ^ 3) v w` and `degree G w = ((G.adjMatrix R) ^ 3) v w`,
@@ -115,6 +117,7 @@ theorem degree_eq_of_not_adj {v w : V} (hvw : ¬G.Adj v w) : degree G v = degree
   simp only [pow_succ _ 2, sq, ← transpose_mul, transpose_apply]
   simp only [mul_assoc]
 
+open scoped Classical in
 include hG in
 /-- Let `A` be the adjacency matrix of a graph `G`.
   If `G` is a friendship graph, then all of the off-diagonal entries of `A^2` are 1.
@@ -126,6 +129,7 @@ theorem adjMatrix_sq_of_regular (hd : G.IsRegularOfDegree d) :
   · rw [h, sq, adjMatrix_mul_self_apply_self, hd]; simp
   · rw [adjMatrix_sq_of_ne R hG h, of_apply, if_neg h]
 
+open scoped Classical in
 include hG in
 theorem adjMatrix_sq_mod_p_of_regular {p : ℕ} (dmod : (d : ZMod p) = 1)
     (hd : G.IsRegularOfDegree d) : G.adjMatrix (ZMod p) ^ 2 = of fun _ _ => 1 := by
@@ -135,6 +139,7 @@ section Nonempty
 
 variable [Nonempty V]
 
+open scoped Classical in
 include hG in
 /-- If `G` is a friendship graph without a politician (a vertex adjacent to all others), then
   it is regular. We have shown that nonadjacent vertices of a friendship graph have the same degree,
@@ -168,6 +173,7 @@ theorem isRegularOf_not_existsPolitician (hG' : ¬ExistsPolitician G) :
   rw [key ((mem_commonNeighbors G).mpr ⟨hvx, G.symm hxw⟩),
     key ((mem_commonNeighbors G).mpr ⟨hvy, G.symm hcontra⟩)]
 
+open scoped Classical in
 include hG in
 /-- Let `A` be the adjacency matrix of a `d`-regular friendship graph, and let `v` be a vector
   all of whose components are `1`. Then `v` is an eigenvector of `A ^ 2`, and we can compute
@@ -187,6 +193,7 @@ theorem card_of_regular (hd : G.IsRegularOfDegree d) : d + (Fintype.card V - 1)
       card_neighborSet_eq_degree, hd v, Function.const_def, adjMatrix_mulVec_apply _ _ (mulVec _ _),
       mul_one, sum_const, Set.toFinset_card, Algebra.id.smul_eq_mul, Nat.cast_id]
 
+open scoped Classical in
 include hG in
 /-- The size of a `d`-regular friendship graph is `1 mod (d-1)`, and thus `1 mod p` for a
   factor `p ∣ d-1`. -/
@@ -200,17 +207,20 @@ theorem card_mod_p_of_regular {p : ℕ} (dmod : (d : ZMod p) = 1) (hd : G.IsRegu
 
 end Nonempty
 
+open scoped Classical in
 theorem adjMatrix_sq_mul_const_one_of_regular (hd : G.IsRegularOfDegree d) :
     G.adjMatrix R * of (fun _ _ => 1) = of (fun _ _ => (d : R)) := by
   ext x
   simp only [← hd x, degree, adjMatrix_mul_apply, sum_const, Nat.smul_one_eq_cast,
     of_apply]
 
+open scoped Classical in
 theorem adjMatrix_mul_const_one_mod_p_of_regular {p : ℕ} (dmod : (d : ZMod p) = 1)
     (hd : G.IsRegularOfDegree d) :
     G.adjMatrix (ZMod p) * of (fun _ _ => 1) = of (fun _ _ => 1) := by
   rw [adjMatrix_sq_mul_const_one_of_regular hd, dmod]
 
+open scoped Classical in
 include hG in
 /-- Modulo a factor of `d-1`, the square and all higher powers of the adjacency matrix
   of a `d`-regular friendship graph reduce to the matrix whose entries are all 1. -/
@@ -227,6 +237,7 @@ theorem adjMatrix_pow_mod_p_of_regular {p : ℕ} (dmod : (d : ZMod p) = 1)
 
 variable [Nonempty V]
 
+open scoped Classical in
 include hG in
 /-- This is the main proof. Assuming that `3 ≤ d`, we take `p` to be a prime factor of `d-1`.
   Then the `p`th power of the adjacency matrix of a `d`-regular friendship graph must have trace 1
@@ -260,6 +271,7 @@ theorem false_of_three_le_degree (hd : G.IsRegularOfDegree d) (h : 3 ≤ d) : Fa
     Nat.dvd_one, Nat.minFac_eq_one_iff]
   omega
 
+open scoped Classical in
 include hG in
 /-- If `d ≤ 1`, a `d`-regular friendship graph has at most one vertex, which is
   trivially a politician. -/
@@ -277,6 +289,7 @@ theorem existsPolitician_of_degree_le_one (hd : G.IsRegularOfDegree d) (hd1 : d
   apply h
   apply Fintype.card_le_one_iff.mp this
 
+open scoped Classical in
 include hG in
 /-- If `d = 2`, a `d`-regular friendship graph has 3 vertices, so it must be complete graph,
   and all the vertices are politicians. -/
@@ -295,6 +308,7 @@ theorem neighborFinset_eq_of_degree_eq_two (hd : G.IsRegularOfDegree 2) (v : V)
   · dsimp only [IsRegularOfDegree, degree] at hd
     rw [hd]
 
+open scoped Classical in
 include hG in
 theorem existsPolitician_of_degree_eq_two (hd : G.IsRegularOfDegree 2) : ExistsPolitician G := by
   have v := Classical.arbitrary V
@@ -303,6 +317,7 @@ theorem existsPolitician_of_degree_eq_two (hd : G.IsRegularOfDegree 2) : ExistsP
   rw [← mem_neighborFinset, neighborFinset_eq_of_degree_eq_two hG hd v, Finset.mem_erase]
   exact ⟨hvw.symm, Finset.mem_univ _⟩
 
+open scoped Classical in
 include hG in
 theorem existsPolitician_of_degree_le_two (hd : G.IsRegularOfDegree d) (h : d ≤ 2) :
     ExistsPolitician G := by
diff --git a/Archive/Wiedijk100Theorems/Partition.lean b/Archive/Wiedijk100Theorems/Partition.lean
index 96f1877c186a5..caf136306ff69 100644
--- a/Archive/Wiedijk100Theorems/Partition.lean
+++ b/Archive/Wiedijk100Theorems/Partition.lean
@@ -64,8 +64,6 @@ variable {α : Type*}
 
 open Finset
 
-open scoped Classical
-
 /-- The partial product for the generating function for odd partitions.
 TODO: As `m` tends to infinity, this converges (in the `X`-adic topology).
 
@@ -92,10 +90,12 @@ open Finset.HasAntidiagonal
 universe u
 variable {ι : Type u}
 
+open scoped Classical in
 /-- A convenience constructor for the power series whose coefficients indicate a subset. -/
 def indicatorSeries (α : Type*) [Semiring α] (s : Set ℕ) : PowerSeries α :=
   PowerSeries.mk fun n => if n ∈ s then 1 else 0
 
+open scoped Classical in
 theorem coeff_indicator (s : Set ℕ) [Semiring α] (n : ℕ) :
     coeff α n (indicatorSeries _ s) = if n ∈ s then 1 else 0 :=
   coeff_mk _ _
@@ -106,6 +106,7 @@ theorem coeff_indicator_pos (s : Set ℕ) [Semiring α] (n : ℕ) (h : n ∈ s)
 theorem coeff_indicator_neg (s : Set ℕ) [Semiring α] (n : ℕ) (h : n ∉ s) :
     coeff α n (indicatorSeries _ s) = 0 := by rw [coeff_indicator, if_neg h]
 
+open scoped Classical in
 theorem constantCoeff_indicator (s : Set ℕ) [Semiring α] :
     constantCoeff α (indicatorSeries _ s) = if 0 ∈ s then 1 else 0 :=
   rfl
@@ -162,6 +163,7 @@ theorem num_series' [Field α] (i : ℕ) :
 def mkOdd : ℕ ↪ ℕ :=
   ⟨fun i => 2 * i + 1, fun x y h => by linarith⟩
 
+open scoped Classical in
 -- The main workhorse of the partition theorem proof.
 theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ) (hs : ∀ i ∈ s, 0 < i)
     (c : ℕ → Set ℕ) (hc : ∀ i, i ∉ s → 0 ∈ c i) :
diff --git a/Counterexamples/IrrationalPowerOfIrrational.lean b/Counterexamples/IrrationalPowerOfIrrational.lean
index 75e822d68b149..6061a15b832af 100644
--- a/Counterexamples/IrrationalPowerOfIrrational.lean
+++ b/Counterexamples/IrrationalPowerOfIrrational.lean
@@ -17,7 +17,7 @@ If `c` is irrational, then `c^√2 = 2` is rational, so we are done.
 -/
 
 
-open Classical Real
+open Real
 
 namespace Counterexample
 
diff --git a/Mathlib/CategoryTheory/Preadditive/Mat.lean b/Mathlib/CategoryTheory/Preadditive/Mat.lean
index 17cee933b9716..2a27f9a373550 100644
--- a/Mathlib/CategoryTheory/Preadditive/Mat.lean
+++ b/Mathlib/CategoryTheory/Preadditive/Mat.lean
@@ -51,8 +51,6 @@ Ideally this would conveniently interact with both `Mat_` and `Matrix`.
 
 open CategoryTheory CategoryTheory.Preadditive
 
-open scoped Classical
-
 noncomputable section
 
 namespace CategoryTheory
@@ -81,6 +79,7 @@ def Hom (M N : Mat_ C) : Type v₁ :=
 
 namespace Hom
 
+open scoped Classical in
 /-- The identity matrix consists of identity morphisms on the diagonal, and zeros elsewhere. -/
 def id (M : Mat_ C) : Hom M M := fun i j => if h : i = j then eqToHom (congr_arg M.X h) else 0
 
@@ -98,8 +97,12 @@ instance : Category.{v₁} (Mat_ C) where
   Hom := Hom
   id := Hom.id
   comp f g := f.comp g
-  id_comp f := by simp (config := { unfoldPartialApp := true }) [dite_comp]
-  comp_id f := by simp (config := { unfoldPartialApp := true }) [comp_dite]
+  id_comp f := by
+    classical
+    simp (config := { unfoldPartialApp := true }) [dite_comp]
+  comp_id f := by
+    classical
+    simp (config := { unfoldPartialApp := true }) [comp_dite]
   assoc f g h := by
     apply DMatrix.ext
     intros
@@ -110,10 +113,12 @@ instance : Category.{v₁} (Mat_ C) where
 theorem hom_ext {M N : Mat_ C} (f g : M ⟶ N) (H : ∀ i j, f i j = g i j) : f = g :=
   DMatrix.ext_iff.mp H
 
+open scoped Classical in
 theorem id_def (M : Mat_ C) :
     (𝟙 M : Hom M M) = fun i j => if h : i = j then eqToHom (congr_arg M.X h) else 0 :=
   rfl
 
+open scoped Classical in
 theorem id_apply (M : Mat_ C) (i j : M.ι) :
     (𝟙 M : Hom M M) i j = if h : i = j then eqToHom (congr_arg M.X h) else 0 :=
   rfl
@@ -155,6 +160,7 @@ instance : Preadditive (Mat_ C) where
 
 open CategoryTheory.Limits
 
+open scoped Classical in
 /-- We now prove that `Mat_ C` has finite biproducts.
 
 Be warned, however, that `Mat_ C` is not necessarily Krull-Schmidt,
@@ -249,6 +255,7 @@ def mapMat_ (F : C ⥤ D) [Functor.Additive F] : Mat_ C ⥤ Mat_ D where
 @[simps!]
 def mapMatId : (𝟭 C).mapMat_ ≅ 𝟭 (Mat_ C) :=
   NatIso.ofComponents (fun M => eqToIso (by cases M; rfl)) fun {M N} f => by
+    classical
     ext
     cases M; cases N
     simp [comp_dite, dite_comp]
@@ -259,6 +266,7 @@ def mapMatId : (𝟭 C).mapMat_ ≅ 𝟭 (Mat_ C) :=
 def mapMatComp {E : Type*} [Category.{v₁} E] [Preadditive E] (F : C ⥤ D) [Functor.Additive F]
     (G : D ⥤ E) [Functor.Additive G] : (F ⋙ G).mapMat_ ≅ F.mapMat_ ⋙ G.mapMat_ :=
   NatIso.ofComponents (fun M => eqToIso (by cases M; rfl)) fun {M N} f => by
+    classical
     ext
     cases M; cases N
     simp [comp_dite, dite_comp]
@@ -294,6 +302,7 @@ open CategoryTheory.Limits
 
 variable {C}
 
+open scoped Classical in
 /-- Every object in `Mat_ C` is isomorphic to the biproduct of its summands.
 -/
 @[simps]
@@ -365,6 +374,7 @@ theorem additiveObjIsoBiproduct_naturality (F : Mat_ C ⥤ D) [Functor.Additive
     F.map f ≫ (additiveObjIsoBiproduct F N).hom =
       (additiveObjIsoBiproduct F M).hom ≫
         biproduct.matrix fun i j => F.map ((embedding C).map (f i j)) := by
+  classical
   ext i : 1
   simp only [Category.assoc, additiveObjIsoBiproduct_hom_π, isoBiproductEmbedding_hom,
     embedding_obj_ι, embedding_obj_X, biproduct.lift_π, biproduct.matrix_π,
@@ -492,6 +502,7 @@ instance (R : Type u) : CoeSort (Mat R) (Type u) :=
 
 open Matrix
 
+open scoped Classical in
 instance (R : Type u) [Semiring R] : Category (Mat R) where
   Hom X Y := Matrix X Y R
   id X := (1 : Matrix X X R)
@@ -510,9 +521,11 @@ theorem hom_ext {X Y : Mat R} (f g : X ⟶ Y) (h : ∀ i j, f i j = g i j) : f =
 
 variable (R)
 
+open scoped Classical in
 theorem id_def (M : Mat R) : 𝟙 M = fun i j => if i = j then 1 else 0 :=
   rfl
 
+open scoped Classical in
 theorem id_apply (M : Mat R) (i j : M) : (𝟙 M : Matrix M M R) i j = if i = j then 1 else 0 :=
   rfl
 
diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean
index 19a73e31325fb..33c511f86aaa4 100644
--- a/Mathlib/Computability/TuringMachine.lean
+++ b/Mathlib/Computability/TuringMachine.lean
@@ -580,8 +580,7 @@ def SupportsStmt (S : Finset Λ) : Stmt₁ → Prop
   | goto l => ∀ a v, l a v ∈ S
   | halt => True
 
-open scoped Classical
-
+open scoped Classical in
 /-- The subterm closure of a statement. -/
 noncomputable def stmts₁ : Stmt₁ → Finset Stmt₁
   | Q@(move _ q) => insert Q (stmts₁ q)
@@ -594,6 +593,7 @@ theorem stmts₁_self {q : Stmt₁} : q ∈ stmts₁ q := by
   cases q <;> simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]
 
 theorem stmts₁_trans {q₁ q₂ : Stmt₁} : q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂ := by
+  classical
   intro h₁₂ q₀ h₀₁
   induction q₂ with (
     simp only [stmts₁] at h₁₂ ⊢
@@ -621,6 +621,7 @@ theorem stmts₁_supportsStmt_mono {S : Finset Λ} {q₁ q₂ : Stmt₁} (h : q
   | halt => subst h; trivial
   | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
 
+open scoped Classical in
 /-- The set of all statements in a Turing machine, plus one extra value `none` representing the
 halt state. This is used in the TM1 to TM0 reduction. -/
 noncomputable def stmts (M : Λ → Stmt₁) (S : Finset Λ) : Finset (Option Stmt₁) :=
@@ -781,12 +782,11 @@ machine states in the target (even though the type `Λ'` is infinite). -/
 noncomputable def trStmts (S : Finset Λ) : Finset Λ'₁₀ :=
   (TM1.stmts M S) ×ˢ Finset.univ
 
-open scoped Classical
-
 attribute [local simp] TM1.stmts₁_self
 
 theorem tr_supports {S : Finset Λ} (ss : TM1.Supports M S) :
     TM0.Supports (tr M) ↑(trStmts M S) := by
+  classical
   constructor
   · apply Finset.mem_product.2
     constructor
@@ -1113,10 +1113,10 @@ theorem tr_respects :
 
 end
 
-open scoped Classical
 
 variable [Fintype Γ]
 
+open scoped Classical in
 /-- The set of accessible `Λ'.write` machine states. -/
 noncomputable def writes : Stmt₁ → Finset Λ'₁
   | Stmt.move _ q => writes q
@@ -1126,11 +1126,13 @@ noncomputable def writes : Stmt₁ → Finset Λ'₁
   | Stmt.goto _ => ∅
   | Stmt.halt => ∅
 
+open scoped Classical in
 /-- The set of accessible machine states, assuming that the input machine is supported on `S`,
 are the normal states embedded from `S`, plus all write states accessible from these states. -/
 noncomputable def trSupp (S : Finset Λ) : Finset Λ'₁ :=
   S.biUnion fun l ↦ insert (Λ'.normal l) (writes (M l))
 
+open scoped Classical in
 theorem tr_supports [Inhabited Λ] {S : Finset Λ} (ss : Supports M S) :
     Supports (tr enc dec M) (trSupp M S) :=
   ⟨Finset.mem_biUnion.2 ⟨_, ss.1, Finset.mem_insert_self _ _⟩, fun q h ↦ by
@@ -1378,8 +1380,8 @@ def SupportsStmt (S : Finset Λ) : Stmt₂ → Prop
   | halt => True
 
 section
-open scoped Classical
 
+open scoped Classical in
 /-- The set of subtree statements in a statement. -/
 noncomputable def stmts₁ : Stmt₂ → Finset Stmt₂
   | Q@(push _ _ q) => insert Q (stmts₁ q)
@@ -1394,6 +1396,7 @@ theorem stmts₁_self {q : Stmt₂} : q ∈ stmts₁ q := by
   cases q <;> simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]
 
 theorem stmts₁_trans {q₁ q₂ : Stmt₂} : q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂ := by
+  classical
   intro h₁₂ q₀ h₀₁
   induction q₂ with (
     simp only [stmts₁] at h₁₂ ⊢
@@ -1422,6 +1425,7 @@ theorem stmts₁_supportsStmt_mono {S : Finset Λ} {q₁ q₂ : Stmt₂} (h : q
   | halt => subst h; trivial
   | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
 
+open scoped Classical in
 /-- The set of statements accessible from initial set `S` of labels. -/
 noncomputable def stmts (M : Λ → Stmt₂) (S : Finset Λ) : Finset (Option Stmt₂) :=
   Finset.insertNone (S.biUnion fun q ↦ stmts₁ (M q))
@@ -1698,8 +1702,8 @@ theorem trNormal_run {k : K} (s : StAct₂ k) (q : Stmt₂) :
   cases s <;> rfl
 
 section
-open scoped Classical
 
+open scoped Classical in
 /-- The set of machine states accessible from an initial TM2 statement. -/
 noncomputable def trStmts₁ : Stmt₂ → Finset Λ'₂₁
   | TM2.Stmt.push k f q => {go k (StAct.push f) q, ret q} ∪ trStmts₁ q
@@ -1709,6 +1713,7 @@ noncomputable def trStmts₁ : Stmt₂ → Finset Λ'₂₁
   | TM2.Stmt.branch _ q₁ q₂ => trStmts₁ q₁ ∪ trStmts₁ q₂
   | _ => ∅
 
+open scoped Classical in
 theorem trStmts₁_run {k : K} {s : StAct₂ k} {q : Stmt₂} :
     trStmts₁ (stRun s q) = {go k s q, ret q} ∪ trStmts₁ q := by
   cases s <;> simp only [trStmts₁, stRun]
@@ -1927,13 +1932,15 @@ theorem tr_eval (k) (L : List (Γ k)) {L₁ L₂} (H₁ : L₁ ∈ TM1.eval (tr
 end
 
 section
-open scoped Classical
+
 variable [Inhabited Λ]
 
+open scoped Classical in
 /-- The support of a set of TM2 states in the TM2 emulator. -/
 noncomputable def trSupp (S : Finset Λ) : Finset Λ'₂₁ :=
   S.biUnion fun l ↦ insert (normal l) (trStmts₁ (M l))
 
+open scoped Classical in
 theorem tr_supports {S} (ss : TM2.Supports M S) : TM1.Supports (tr M) (trSupp M S) :=
   ⟨Finset.mem_biUnion.2 ⟨_, ss.1, Finset.mem_insert.2 <| Or.inl rfl⟩, fun l' h ↦ by
     suffices ∀ (q) (_ : TM2.SupportsStmt S q) (_ : ∀ x ∈ trStmts₁ q, x ∈ trSupp M S),
diff --git a/Mathlib/Control/LawfulFix.lean b/Mathlib/Control/LawfulFix.lean
index f22207cffe5c1..9c9a30c5b82a3 100644
--- a/Mathlib/Control/LawfulFix.lean
+++ b/Mathlib/Control/LawfulFix.lean
@@ -22,8 +22,6 @@ omega complete partial orders (ωCPO). Proofs of the lawfulness of all `Fix` ins
 
 universe u v
 
-open scoped Classical
-
 variable {α : Type*} {β : α → Type*}
 
 open OmegaCompletePartialOrder
@@ -63,6 +61,7 @@ theorem approx_mono ⦃i j : ℕ⦄ (hij : i ≤ j) : approx f i ≤ approx f j
   exact le_trans (ih ‹_›) (approx_mono' f)
 
 theorem mem_iff (a : α) (b : β a) : b ∈ Part.fix f a ↔ ∃ i, b ∈ approx f i a := by
+  classical
   by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
   · simp only [Part.fix_def f h₀]
     constructor <;> intro hh
diff --git a/Mathlib/Data/Int/ConditionallyCompleteOrder.lean b/Mathlib/Data/Int/ConditionallyCompleteOrder.lean
index 077cb7a5b47c8..03ec19f1799b6 100644
--- a/Mathlib/Data/Int/ConditionallyCompleteOrder.lean
+++ b/Mathlib/Data/Int/ConditionallyCompleteOrder.lean
@@ -17,8 +17,8 @@ open Int
 
 
 noncomputable section
-open scoped Classical
 
+open scoped Classical in
 instance instConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder ℤ where
   __ := instLinearOrder
   __ := LinearOrder.toLattice
diff --git a/Mathlib/Data/Nat/Lattice.lean b/Mathlib/Data/Nat/Lattice.lean
index cd3c50fdd53c6..69b77b20877e1 100644
--- a/Mathlib/Data/Nat/Lattice.lean
+++ b/Mathlib/Data/Nat/Lattice.lean
@@ -21,17 +21,19 @@ open Set
 
 namespace Nat
 
-open scoped Classical
-
+open scoped Classical in
 noncomputable instance : InfSet ℕ :=
   ⟨fun s ↦ if h : ∃ n, n ∈ s then @Nat.find (fun n ↦ n ∈ s) _ h else 0⟩
 
+open scoped Classical in
 noncomputable instance : SupSet ℕ :=
   ⟨fun s ↦ if h : ∃ n, ∀ a ∈ s, a ≤ n then @Nat.find (fun n ↦ ∀ a ∈ s, a ≤ n) _ h else 0⟩
 
+open scoped Classical in
 theorem sInf_def {s : Set ℕ} (h : s.Nonempty) : sInf s = @Nat.find (fun n ↦ n ∈ s) _ h :=
   dif_pos _
 
+open scoped Classical in
 theorem sSup_def {s : Set ℕ} (h : ∃ n, ∀ a ∈ s, a ≤ n) :
     sSup s = @Nat.find (fun n ↦ ∀ a ∈ s, a ≤ n) _ h :=
   dif_pos _
@@ -65,15 +67,18 @@ lemma iInf_const_zero {ι : Sort*} : ⨅ _ : ι, 0 = 0 :=
   (isEmpty_or_nonempty ι).elim (fun h ↦ by simp) fun h ↦ sInf_eq_zero.2 <| by simp
 
 theorem sInf_mem {s : Set ℕ} (h : s.Nonempty) : sInf s ∈ s := by
+  classical
   rw [Nat.sInf_def h]
   exact Nat.find_spec h
 
 theorem not_mem_of_lt_sInf {s : Set ℕ} {m : ℕ} (hm : m < sInf s) : m ∉ s := by
+  classical
   cases eq_empty_or_nonempty s with
   | inl h => subst h; apply not_mem_empty
   | inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm
 
 protected theorem sInf_le {s : Set ℕ} {m : ℕ} (hm : m ∈ s) : sInf s ≤ m := by
+  classical
   rw [Nat.sInf_def ⟨m, hm⟩]
   exact Nat.find_min' ⟨m, hm⟩ hm
 
@@ -95,6 +100,7 @@ theorem eq_Ici_of_nonempty_of_upward_closed {s : Set ℕ} (hs : s.Nonempty)
 
 theorem sInf_upward_closed_eq_succ_iff {s : Set ℕ} (hs : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s)
     (k : ℕ) : sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s := by
+  classical
   constructor
   · intro H
     rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]
@@ -110,6 +116,7 @@ theorem sInf_upward_closed_eq_succ_iff {s : Set ℕ} (hs : ∀ k₁ k₂ : ℕ,
 instance : Lattice ℕ :=
   LinearOrder.toLattice
 
+open scoped Classical in
 noncomputable instance : ConditionallyCompleteLinearOrderBot ℕ :=
   { (inferInstance : OrderBot ℕ), (LinearOrder.toLattice : Lattice ℕ),
     (inferInstance : LinearOrder ℕ) with
@@ -140,6 +147,7 @@ theorem sSup_mem {s : Set ℕ} (h₁ : s.Nonempty) (h₂ : BddAbove s) : sSup s
 
 theorem sInf_add {n : ℕ} {p : ℕ → Prop} (hn : n ≤ sInf { m | p m }) :
     sInf { m | p (m + n) } + n = sInf { m | p m } := by
+  classical
   obtain h | ⟨m, hm⟩ := { m | p (m + n) }.eq_empty_or_nonempty
   · rw [h, Nat.sInf_empty, zero_add]
     obtain hnp | hnp := hn.eq_or_lt
diff --git a/Mathlib/Data/Nat/PartENat.lean b/Mathlib/Data/Nat/PartENat.lean
index 5b4dd68288d83..0350d9d4b3cb9 100644
--- a/Mathlib/Data/Nat/PartENat.lean
+++ b/Mathlib/Data/Nat/PartENat.lean
@@ -640,8 +640,7 @@ theorem ofENat_lt {x y : ℕ∞} : ofENat x < ofENat y ↔ x < y := by
 
 section WithTopEquiv
 
-open scoped Classical
-
+open scoped Classical in
 @[simp]
 theorem toWithTop_add {x y : PartENat} : toWithTop (x + y) = toWithTop x + toWithTop y := by
   refine PartENat.casesOn y ?_ ?_ <;> refine PartENat.casesOn x ?_ ?_
@@ -651,6 +650,7 @@ theorem toWithTop_add {x y : PartENat} : toWithTop (x + y) = toWithTop x + toWit
   · simp only [top_add, toWithTop_top', toWithTop_natCast', _root_.top_add, forall_const]
   · simp_rw [toWithTop_natCast', ← Nat.cast_add, toWithTop_natCast', forall_const]
 
+open scoped Classical in
 /-- `Equiv` between `PartENat` and `ℕ∞` (for the order isomorphism see
 `withTopOrderIso`). -/
 @[simps]
diff --git a/Mathlib/Data/Option/Basic.lean b/Mathlib/Data/Option/Basic.lean
index 8a275196668f5..d6f5815d92c9e 100644
--- a/Mathlib/Data/Option/Basic.lean
+++ b/Mathlib/Data/Option/Basic.lean
@@ -289,8 +289,6 @@ theorem orElse_eq_none' (o o' : Option α) : o.orElse (fun _ ↦ o') = none ↔
 
 section
 
-open scoped Classical
-
 theorem choice_eq_none (α : Type*) [IsEmpty α] : choice α = none :=
   dif_neg (not_nonempty_iff_imp_false.mpr isEmptyElim)
 
diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
index faf9e2b92885d..394f2d018f935 100644
--- a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
+++ b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@@ -288,8 +288,7 @@ open Finset Nat
 
 section Classical
 
-open scoped Classical
-
+open scoped Classical in
 @[to_additive IsAddCyclic.card_nsmul_eq_zero_le]
 theorem IsCyclic.card_pow_eq_one_le [DecidableEq α] [Fintype α] [IsCyclic α] {n : ℕ} (hn0 : 0 < n) :
     #{a : α | a ^ n = 1} ≤ n :=
diff --git a/Mathlib/Probability/Density.lean b/Mathlib/Probability/Density.lean
index 8100dd885dedf..a89d87c31a792 100644
--- a/Mathlib/Probability/Density.lean
+++ b/Mathlib/Probability/Density.lean
@@ -50,7 +50,7 @@ which we currently do not have.
 -/
 
 
-open scoped Classical MeasureTheory NNReal ENNReal
+open scoped MeasureTheory NNReal ENNReal
 
 open TopologicalSpace MeasureTheory.Measure
 
diff --git a/Mathlib/Probability/Distributions/Uniform.lean b/Mathlib/Probability/Distributions/Uniform.lean
index 77f3a13bb4a8c..3efd4efda464d 100644
--- a/Mathlib/Probability/Distributions/Uniform.lean
+++ b/Mathlib/Probability/Distributions/Uniform.lean
@@ -39,7 +39,7 @@ This file defines a number of uniform `PMF` distributions from various inputs,
 * Refactor the `PMF` definitions to come from a `uniformMeasure` on a `Finset`/`Fintype`/`Multiset`.
 -/
 
-open scoped Classical MeasureTheory NNReal ENNReal
+open scoped MeasureTheory NNReal ENNReal
 
 -- TODO: We can't `open ProbabilityTheory` without opening the `ProbabilityTheory` locale :(
 open TopologicalSpace MeasureTheory.Measure PMF
@@ -193,6 +193,7 @@ lemma uniformPDF_eq_pdf {s : Set E} (hs : MeasurableSet s) (hu : pdf.IsUniform X
   unfold uniformPDF
   exact Filter.EventuallyEq.trans (pdf.IsUniform.pdf_eq hs hu).symm (ae_eq_refl _)
 
+open scoped Classical in
 /-- Alternative way of writing the uniformPDF. -/
 lemma uniformPDF_ite {s : Set E} {x : E} :
     uniformPDF s x μ = if x ∈ s then (μ s)⁻¹ else 0 := by
diff --git a/Mathlib/Probability/ProbabilityMassFunction/Basic.lean b/Mathlib/Probability/ProbabilityMassFunction/Basic.lean
index f5124ea768ad5..cf45350093d48 100644
--- a/Mathlib/Probability/ProbabilityMassFunction/Basic.lean
+++ b/Mathlib/Probability/ProbabilityMassFunction/Basic.lean
@@ -34,7 +34,6 @@ noncomputable section
 
 variable {α : Type*}
 
-open scoped Classical
 open NNReal ENNReal MeasureTheory
 
 /-- A probability mass function, or discrete probability measures is a function `α → ℝ≥0∞` such
@@ -99,6 +98,7 @@ theorem apply_eq_one_iff (p : PMF α) (a : α) : p a = 1 ↔ p.support = {a} :=
     fun h => _root_.trans (symm <| tsum_eq_single a
       fun a' ha' => (p.apply_eq_zero_iff a').2 (h.symm ▸ ha')) p.tsum_coe⟩
   suffices 1 < ∑' a, p a from ne_of_lt this p.tsum_coe.symm
+  classical
   have : 0 < ∑' b, ite (b = a) 0 (p b) := lt_of_le_of_ne' zero_le'
     ((tsum_ne_zero_iff ENNReal.summable).2
       ⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩)
@@ -114,6 +114,7 @@ theorem apply_eq_one_iff (p : PMF α) (a : α) : p a = 1 ↔ p.support = {a} :=
     _ = ∑' b, p b := tsum_congr fun b => by split_ifs <;> simp only [zero_add, add_zero, le_rfl]
 
 theorem coe_le_one (p : PMF α) (a : α) : p a ≤ 1 := by
+  classical
   refine hasSum_le (fun b => ?_) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)
   split_ifs with h <;> simp only [h, zero_le', le_rfl]
 
@@ -152,8 +153,8 @@ theorem toOuterMeasure_apply_finset (s : Finset α) : p.toOuterMeasure s = ∑ x
 
 theorem toOuterMeasure_apply_singleton (a : α) : p.toOuterMeasure {a} = p a := by
   refine (p.toOuterMeasure_apply {a}).trans ((tsum_eq_single a fun b hb => ?_).trans ?_)
-  · exact ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'
-  · exact ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl
+  · classical exact ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'
+  · classical exact ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl
 
 theorem toOuterMeasure_injective : (toOuterMeasure : PMF α → OuterMeasure α).Injective :=
   fun p q h => PMF.ext fun x => (p.toOuterMeasure_apply_singleton x).symm.trans
@@ -174,7 +175,7 @@ theorem toOuterMeasure_apply_eq_one_iff : p.toOuterMeasure s = 1 ↔ p.support 
     have hsa : s.indicator p a < p a := hs'.symm ▸ (p.apply_pos_iff a).2 hap
     exact ENNReal.tsum_lt_tsum (p.tsum_coe_indicator_ne_top s)
       (fun x => Set.indicator_apply_le fun _ => le_rfl) hsa
-  · suffices ∀ (x) (_ : x ∉ s), p x = 0 from
+  · classical suffices ∀ (x) (_ : x ∉ s), p x = 0 from
       _root_.trans (tsum_congr
         fun a => (Set.indicator_apply s p a).trans
           (ite_eq_left_iff.2 <| symm ∘ this a)) p.tsum_coe
diff --git a/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean b/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
index 6ef283f1de7dc..95ab35f0e5b9f 100644
--- a/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
+++ b/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
@@ -32,7 +32,6 @@ noncomputable section
 
 variable {α β γ : Type*}
 
-open scoped Classical
 open NNReal ENNReal Finset MeasureTheory
 
 section Map
@@ -45,6 +44,7 @@ variable (f : α → β) (p : PMF α) (b : β)
 
 theorem monad_map_eq_map {α β : Type u} (f : α → β) (p : PMF α) : f <$> p = p.map f := rfl
 
+open scoped Classical in
 @[simp]
 theorem map_apply : (map f p) b = ∑' a, if b = f a then p a else 0 := by simp [map]
 
@@ -82,6 +82,7 @@ variable (s : Set β)
 @[simp]
 theorem toOuterMeasure_map_apply : (p.map f).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s) := by
   simp [map, Set.indicator, toOuterMeasure_apply p (f ⁻¹' s)]
+  rfl
 
 variable {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
 
@@ -110,6 +111,7 @@ variable (q : PMF (α → β)) (p : PMF α) (b : β)
 
 theorem monad_seq_eq_seq {α β : Type u} (q : PMF (α → β)) (p : PMF α) : q <*> p = q.seq p := rfl
 
+open scoped Classical in
 @[simp]
 theorem seq_apply : (seq q p) b = ∑' (f : α → β) (a : α), if b = f a then q f * p a else 0 := by
   simp only [seq, mul_boole, bind_apply, pure_apply]
@@ -207,6 +209,7 @@ theorem support_ofFintype : (ofFintype f h).support = Function.support f := rfl
 
 theorem mem_support_ofFintype_iff (a : α) : a ∈ (ofFintype f h).support ↔ f a ≠ 0 := Iff.rfl
 
+open scoped Classical in
 @[simp]
 lemma map_ofFintype [Fintype β] (f : α → ℝ≥0∞) (h : ∑ a, f a = 1) (g : α → β) :
     (ofFintype f h).map g = ofFintype (fun b ↦ ∑ a with g a = b, f a)
diff --git a/Mathlib/Probability/ProbabilityMassFunction/Monad.lean b/Mathlib/Probability/ProbabilityMassFunction/Monad.lean
index acf07b214fb38..ee267a4c971de 100644
--- a/Mathlib/Probability/ProbabilityMassFunction/Monad.lean
+++ b/Mathlib/Probability/ProbabilityMassFunction/Monad.lean
@@ -23,7 +23,6 @@ noncomputable section
 
 variable {α β γ : Type*}
 
-open scoped Classical
 open NNReal ENNReal
 
 open MeasureTheory
@@ -32,6 +31,7 @@ namespace PMF
 
 section Pure
 
+open scoped Classical in
 /-- The pure `PMF` is the `PMF` where all the mass lies in one point.
   The value of `pure a` is `1` at `a` and `0` elsewhere. -/
 def pure (a : α) : PMF α :=
@@ -39,6 +39,7 @@ def pure (a : α) : PMF α :=
 
 variable (a a' : α)
 
+open scoped Classical in
 @[simp]
 theorem pure_apply : pure a a' = if a' = a then 1 else 0 := rfl
 
@@ -61,6 +62,7 @@ section Measure
 
 variable (s : Set α)
 
+open scoped Classical in
 @[simp]
 theorem toOuterMeasure_pure_apply : (pure a).toOuterMeasure s = if a ∈ s then 1 else 0 := by
   refine (toOuterMeasure_apply (pure a) s).trans ?_
@@ -74,6 +76,7 @@ theorem toOuterMeasure_pure_apply : (pure a).toOuterMeasure s = if a ∈ s then
 
 variable [MeasurableSpace α]
 
+open scoped Classical in
 /-- The measure of a set under `pure a` is `1` for sets containing `a` and `0` otherwise. -/
 @[simp]
 theorem toMeasure_pure_apply (hs : MeasurableSet s) :
@@ -115,6 +118,7 @@ theorem mem_support_bind_iff (b : β) :
 
 @[simp]
 theorem pure_bind (a : α) (f : α → PMF β) : (pure a).bind f = f a := by
+  classical
   have : ∀ b a', ite (a' = a) (f a' b) 0 = ite (a' = a) (f a b) 0 := fun b a' => by
     split_ifs with h <;> simp [h]
   ext b
@@ -148,7 +152,8 @@ variable (s : Set β)
 
 @[simp]
 theorem toOuterMeasure_bind_apply :
-    (p.bind f).toOuterMeasure s = ∑' a, p a * (f a).toOuterMeasure s :=
+    (p.bind f).toOuterMeasure s = ∑' a, p a * (f a).toOuterMeasure s := by
+  classical
   calc
     (p.bind f).toOuterMeasure s = ∑' b, if b ∈ s then ∑' a, p a * f a b else 0 := by
       simp [toOuterMeasure_apply, Set.indicator_apply]
@@ -236,6 +241,7 @@ theorem pure_bindOnSupport (a : α) (f : ∀ (a' : α) (_ : a' ∈ (pure a).supp
     (pure a).bindOnSupport f = f a ((mem_support_pure_iff a a).mpr rfl) := by
   refine PMF.ext fun b => ?_
   simp only [bindOnSupport_apply, pure_apply]
+  classical
   refine _root_.trans (tsum_congr fun a' => ?_) (tsum_ite_eq a _)
   by_cases h : a' = a <;> simp [h]
 
@@ -252,6 +258,7 @@ theorem bindOnSupport_bindOnSupport (p : PMF α) (f : ∀ a ∈ p.support, PMF 
   refine PMF.ext fun a => ?_
   dsimp only [bindOnSupport_apply]
   simp only [← tsum_dite_right, ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm]
+  classical
   simp only [ENNReal.tsum_eq_zero, dite_eq_left_iff]
   refine ENNReal.tsum_comm.trans (tsum_congr fun a' => tsum_congr fun b => ?_)
   split_ifs with h _ h_1 _ h_2
@@ -279,6 +286,7 @@ theorem toOuterMeasure_bindOnSupport_apply :
     (p.bindOnSupport f).toOuterMeasure s =
       ∑' a, p a * if h : p a = 0 then 0 else (f a h).toOuterMeasure s := by
   simp only [toOuterMeasure_apply, Set.indicator_apply, bindOnSupport_apply]
+  classical
   calc
     (∑' b, ite (b ∈ s) (∑' a, p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0) =
         ∑' (b) (a), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
diff --git a/Mathlib/Probability/Process/Adapted.lean b/Mathlib/Probability/Process/Adapted.lean
index 101965bb8f539..eb30f8b442411 100644
--- a/Mathlib/Probability/Process/Adapted.lean
+++ b/Mathlib/Probability/Process/Adapted.lean
@@ -35,7 +35,7 @@ adapted, progressively measurable
 
 open Filter Order TopologicalSpace
 
-open scoped Classical MeasureTheory NNReal ENNReal Topology
+open scoped MeasureTheory NNReal ENNReal Topology
 
 namespace MeasureTheory
 
diff --git a/Mathlib/Probability/Process/HittingTime.lean b/Mathlib/Probability/Process/HittingTime.lean
index b5a22e608a3fe..5ac75975d6483 100644
--- a/Mathlib/Probability/Process/HittingTime.lean
+++ b/Mathlib/Probability/Process/HittingTime.lean
@@ -36,21 +36,25 @@ hitting times indexed by the natural numbers or the reals. By taking the bounds
 
 open Filter Order TopologicalSpace
 
-open scoped Classical MeasureTheory NNReal ENNReal Topology
+open scoped MeasureTheory NNReal ENNReal Topology
 
 namespace MeasureTheory
 
 variable {Ω β ι : Type*} {m : MeasurableSpace Ω}
 
+open scoped Classical in
 /-- Hitting time: given a stochastic process `u` and a set `s`, `hitting u s n m` is the first time
 `u` is in `s` after time `n` and before time `m` (if `u` does not hit `s` after time `n` and
 before `m` then the hitting time is simply `m`).
 
 The hitting time is a stopping time if the process is adapted and discrete. -/
-noncomputable def hitting [Preorder ι] [InfSet ι] (u : ι → Ω → β) (s : Set β) (n m : ι) : Ω → ι :=
-  fun x => if ∃ j ∈ Set.Icc n m, u j x ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i x ∈ s}) else m
+noncomputable def hitting [Preorder ι] [InfSet ι] (u : ι → Ω → β)
+    (s : Set β) (n m : ι) : Ω → ι :=
+  fun x => if ∃ j ∈ Set.Icc n m, u j x ∈ s
+    then sInf (Set.Icc n m ∩ {i : ι | u i x ∈ s}) else m
 
 #adaptation_note /-- nightly-2024-03-16: added to replace simp [hitting] -/
+open scoped Classical in
 theorem hitting_def [Preorder ι] [InfSet ι] (u : ι → Ω → β) (s : Set β) (n m : ι) :
     hitting u s n m =
     fun x => if ∃ j ∈ Set.Icc n m, u j x ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i x ∈ s}) else m :=
@@ -90,11 +94,13 @@ theorem not_mem_of_lt_hitting {m k : ι} (hk₁ : k < hitting u s n m ω) (hk₂
 
 theorem hitting_eq_end_iff {m : ι} : hitting u s n m ω = m ↔
     (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m := by
+  classical
   rw [hitting, ite_eq_right_iff]
 
 theorem hitting_of_le {m : ι} (hmn : m ≤ n) : hitting u s n m ω = m := by
   obtain rfl | h := le_iff_eq_or_lt.1 hmn
-  · rw [hitting, ite_eq_right_iff, forall_exists_index]
+  · classical
+    rw [hitting, ite_eq_right_iff, forall_exists_index]
     conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
     intro i hi₁ hi₂ hi
     rw [Set.inter_eq_left.2, csInf_singleton]
diff --git a/Mathlib/Probability/Process/Stopping.lean b/Mathlib/Probability/Process/Stopping.lean
index a9b107e3d88e4..80f76791df248 100644
--- a/Mathlib/Probability/Process/Stopping.lean
+++ b/Mathlib/Probability/Process/Stopping.lean
@@ -33,7 +33,7 @@ stopping time, stochastic process
 
 open Filter Order TopologicalSpace
 
-open scoped Classical MeasureTheory NNReal ENNReal Topology
+open scoped MeasureTheory NNReal ENNReal Topology
 
 namespace MeasureTheory
 
@@ -96,6 +96,7 @@ protected theorem measurableSet_eq_of_countable_range (hτ : IsStoppingTime f τ
   rw [this]
   refine (hτ.measurableSet_le i).diff ?_
   refine MeasurableSet.biUnion h_countable fun j _ => ?_
+  classical
   rw [Set.iUnion_eq_if]
   split_ifs with hji
   · exact f.mono hji.le _ (hτ.measurableSet_le j)
@@ -803,6 +804,7 @@ variable {μ : Measure Ω} {τ : Ω → ι} {E : Type*} {p : ℝ≥0∞} {u : ι
 theorem stoppedValue_eq_of_mem_finset [AddCommMonoid E] {s : Finset ι} (hbdd : ∀ ω, τ ω ∈ s) :
     stoppedValue u τ = ∑ i ∈ s, Set.indicator {ω | τ ω = i} (u i) := by
   ext y
+  classical
   rw [stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]
   suffices Finset.filter (fun i => y ∈ {ω : Ω | τ ω = i}) s = ({τ y} : Finset ι) by
     rw [this, Finset.sum_singleton]
diff --git a/Mathlib/RepresentationTheory/Character.lean b/Mathlib/RepresentationTheory/Character.lean
index cb98ce35c607a..ada933887ae23 100644
--- a/Mathlib/RepresentationTheory/Character.lean
+++ b/Mathlib/RepresentationTheory/Character.lean
@@ -98,10 +98,9 @@ section Orthogonality
 
 variable {G : Grp.{u}} [IsAlgClosed k]
 
-open scoped Classical
-
 variable [Fintype G] [Invertible (Fintype.card G : k)]
 
+open scoped Classical in
 /-- Orthogonality of characters for irreducible representations of finite group over an
 algebraically closed field whose characteristic doesn't divide the order of the group. -/
 theorem char_orthonormal (V W : FDRep k G) [Simple V] [Simple W] :
diff --git a/Mathlib/RepresentationTheory/FDRep.lean b/Mathlib/RepresentationTheory/FDRep.lean
index 8eaedce3ed27a..dd5870c18de16 100644
--- a/Mathlib/RepresentationTheory/FDRep.lean
+++ b/Mathlib/RepresentationTheory/FDRep.lean
@@ -128,12 +128,11 @@ example : MonoidalLinear k (FDRep k G) := by infer_instance
 
 open Module
 
-open scoped Classical
-
 -- We need to provide this instance explicitly as otherwise `finrank_hom_simple_simple` gives a
 -- deterministic timeout.
 instance : HasKernels (FDRep k G) := by infer_instance
 
+open scoped Classical in
 /-- Schur's Lemma: the dimension of the `Hom`-space between two irreducible representation is `0` if
 they are not isomorphic, and `1` if they are. -/
 theorem finrank_hom_simple_simple [IsAlgClosed k] (V W : FDRep k G) [Simple V] [Simple W] :
diff --git a/Mathlib/RingTheory/Adjoin/FG.lean b/Mathlib/RingTheory/Adjoin/FG.lean
index b98e44e79d735..1ea80e3f8b9f8 100644
--- a/Mathlib/RingTheory/Adjoin/FG.lean
+++ b/Mathlib/RingTheory/Adjoin/FG.lean
@@ -129,11 +129,10 @@ theorem FG.prod {S : Subalgebra R A} {T : Subalgebra R B} (hS : S.FG) (hT : T.FG
 
 section
 
-open scoped Classical
-
-theorem FG.map {S : Subalgebra R A} (f : A →ₐ[R] B) (hs : S.FG) : (S.map f).FG :=
+theorem FG.map {S : Subalgebra R A} (f : A →ₐ[R] B) (hs : S.FG) : (S.map f).FG := by
   let ⟨s, hs⟩ := hs
-  ⟨s.image f, by rw [Finset.coe_image, Algebra.adjoin_image, hs]⟩
+  classical
+  exact ⟨s.image f, by rw [Finset.coe_image, Algebra.adjoin_image, hs]⟩
 
 end
 
diff --git a/Mathlib/RingTheory/Adjoin/Tower.lean b/Mathlib/RingTheory/Adjoin/Tower.lean
index c916d29572648..5e0b6870afb10 100644
--- a/Mathlib/RingTheory/Adjoin/Tower.lean
+++ b/Mathlib/RingTheory/Adjoin/Tower.lean
@@ -58,17 +58,19 @@ end Algebra
 
 section
 
-open scoped Classical
-
 theorem Algebra.fg_trans' {R S A : Type*} [CommSemiring R] [CommSemiring S] [Semiring A]
     [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (hRS : (⊤ : Subalgebra R S).FG)
-    (hSA : (⊤ : Subalgebra S A).FG) : (⊤ : Subalgebra R A).FG :=
-  let ⟨s, hs⟩ := hRS
-  let ⟨t, ht⟩ := hSA
-  ⟨s.image (algebraMap S A) ∪ t, by
-    rw [Finset.coe_union, Finset.coe_image, Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
-      hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top, Subalgebra.restrictScalars_top]⟩
-
+    (hSA : (⊤ : Subalgebra S A).FG) : (⊤ : Subalgebra R A).FG := by
+  classical
+  rcases hRS with ⟨s, hs⟩
+  rcases hSA with ⟨t, ht⟩
+  exact ⟨s.image (algebraMap S A) ∪ t, by
+    rw [Finset.coe_union, Finset.coe_image,
+        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
+        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
+        Subalgebra.restrictScalars_top
+       ]
+    ⟩
 end
 
 section ArtinTate
@@ -82,8 +84,6 @@ variable [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
 
 open Finset Submodule
 
-open scoped Classical
-
 theorem exists_subalgebra_of_fg (hAC : (⊤ : Subalgebra A C).FG) (hBC : (⊤ : Submodule B C).FG) :
     ∃ B₀ : Subalgebra A B, B₀.FG ∧ (⊤ : Submodule B₀ C).FG := by
   cases' hAC with x hx
@@ -91,6 +91,7 @@ theorem exists_subalgebra_of_fg (hAC : (⊤ : Subalgebra A C).FG) (hBC : (⊤ :
   have := hy
   simp_rw [eq_top_iff', mem_span_finset] at this
   choose f hf using this
+  classical
   let s : Finset B := Finset.image₂ f (x ∪ y * y) y
   have hxy :
     ∀ xi ∈ x, xi ∈ span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) :=
diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean
index 6d04333d192e0..b861c1ecbe216 100644
--- a/Mathlib/RingTheory/AdjoinRoot.lean
+++ b/Mathlib/RingTheory/AdjoinRoot.lean
@@ -48,8 +48,6 @@ The main definitions are in the `AdjoinRoot` namespace.
 
 noncomputable section
 
-open scoped Classical
-
 open Polynomial
 
 universe u v w
diff --git a/Mathlib/RingTheory/AlgebraTower.lean b/Mathlib/RingTheory/AlgebraTower.lean
index cd4e432e660f0..ef70b261a1645 100644
--- a/Mathlib/RingTheory/AlgebraTower.lean
+++ b/Mathlib/RingTheory/AlgebraTower.lean
@@ -85,8 +85,6 @@ section Semiring
 
 open Finsupp
 
-open scoped Classical
-
 variable {R S A}
 variable [Semiring R] [Semiring S] [AddCommMonoid A]
 variable [Module R S] [Module S A] [Module R A] [IsScalarTower R S A]
@@ -132,6 +130,7 @@ theorem Basis.smulTower_repr_mk (x i j) : (b.smulTower c).repr x (i, j) = b.repr
 
 @[simp]
 theorem Basis.smulTower_apply (ij) : (b.smulTower c) ij = b ij.1 • c ij.2 := by
+  classical
   obtain ⟨i, j⟩ := ij
   rw [Basis.apply_eq_iff]
   ext ⟨i', j'⟩
diff --git a/Mathlib/RingTheory/AlgebraicIndependent/Adjoin.lean b/Mathlib/RingTheory/AlgebraicIndependent/Adjoin.lean
index 46cb51be48adf..66a7c7a829c69 100644
--- a/Mathlib/RingTheory/AlgebraicIndependent/Adjoin.lean
+++ b/Mathlib/RingTheory/AlgebraicIndependent/Adjoin.lean
@@ -25,8 +25,6 @@ noncomputable section
 
 open Function Set Subalgebra MvPolynomial Algebra
 
-open scoped Classical
-
 namespace AlgebraicIndependent
 
 variable {ι : Type*}
diff --git a/Mathlib/RingTheory/AlgebraicIndependent/Basic.lean b/Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
index 0660623b33d9f..6f7f1983917b2 100644
--- a/Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
+++ b/Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
@@ -33,8 +33,6 @@ noncomputable section
 
 open Function Set Subalgebra MvPolynomial Algebra
 
-open scoped Classical
-
 variable {ι ι' R K A A' : Type*} {x : ι → A}
 variable [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A']
 
diff --git a/Mathlib/RingTheory/AlgebraicIndependent/Defs.lean b/Mathlib/RingTheory/AlgebraicIndependent/Defs.lean
index c3d9b6df75314..83bd22ac7b31c 100644
--- a/Mathlib/RingTheory/AlgebraicIndependent/Defs.lean
+++ b/Mathlib/RingTheory/AlgebraicIndependent/Defs.lean
@@ -41,8 +41,6 @@ noncomputable section
 
 open Function Set Subalgebra MvPolynomial Algebra
 
-open scoped Classical
-
 variable {ι ι' : Type*} (R : Type*) {K A A' : Type*} (x : ι → A)
 variable [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A']
 
diff --git a/Mathlib/RingTheory/FiniteType.lean b/Mathlib/RingTheory/FiniteType.lean
index 40f8bd11de976..c8b20cf8bab7c 100644
--- a/Mathlib/RingTheory/FiniteType.lean
+++ b/Mathlib/RingTheory/FiniteType.lean
@@ -75,10 +75,10 @@ protected theorem polynomial : FiniteType R R[X] :=
       rw [Finset.coe_singleton]
       exact Polynomial.adjoin_X⟩⟩
 
-open scoped Classical
 
 protected theorem freeAlgebra (ι : Type*) [Finite ι] : FiniteType R (FreeAlgebra R ι) := by
   cases nonempty_fintype ι
+  classical
   exact
     ⟨⟨Finset.univ.image (FreeAlgebra.ι R), by
         rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
@@ -86,6 +86,7 @@ protected theorem freeAlgebra (ι : Type*) [Finite ι] : FiniteType R (FreeAlgeb
 
 protected theorem mvPolynomial (ι : Type*) [Finite ι] : FiniteType R (MvPolynomial ι R) := by
   cases nonempty_fintype ι
+  classical
   exact
     ⟨⟨Finset.univ.image MvPolynomial.X, by
         rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
diff --git a/Mathlib/RingTheory/Fintype.lean b/Mathlib/RingTheory/Fintype.lean
index 9ee3bc2a315f2..e13486bc2013a 100644
--- a/Mathlib/RingTheory/Fintype.lean
+++ b/Mathlib/RingTheory/Fintype.lean
@@ -51,8 +51,7 @@ lemma Finset.univ_of_card_le_three (h : Fintype.card R ≤ 3) :
       · exact zero_ne_one h
       · exact zero_ne_one h.symm
 
-open scoped Classical
-
+open scoped Classical in
 theorem card_units_lt (M₀ : Type*) [MonoidWithZero M₀] [Nontrivial M₀] [Fintype M₀] :
     Fintype.card M₀ˣ < Fintype.card M₀ :=
   Fintype.card_lt_of_injective_of_not_mem Units.val Units.ext not_isUnit_zero
diff --git a/Mathlib/RingTheory/FreeCommRing.lean b/Mathlib/RingTheory/FreeCommRing.lean
index af33998c3ea6e..a09a60ff00f16 100644
--- a/Mathlib/RingTheory/FreeCommRing.lean
+++ b/Mathlib/RingTheory/FreeCommRing.lean
@@ -50,7 +50,6 @@ free commutative ring, free ring
 
 noncomputable section
 
-open scoped Classical
 open Polynomial
 
 universe u v
@@ -224,6 +223,7 @@ end Restriction
 theorem isSupported_of {p} {s : Set α} : IsSupported (of p) s ↔ p ∈ s :=
   suffices IsSupported (of p) s → p ∈ s from ⟨this, fun hps => Subring.subset_closure ⟨p, hps, rfl⟩⟩
   fun hps : IsSupported (of p) s => by
+  classical
   haveI := Classical.decPred s
   have : ∀ x, IsSupported x s →
         ∃ n : ℤ, lift (fun a => if a ∈ s then (0 : ℤ[X]) else Polynomial.X) x = n := by
diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean
index dbbef917b461d..fd5d7b6a7e4a6 100644
--- a/Mathlib/RingTheory/LaurentSeries.lean
+++ b/Mathlib/RingTheory/LaurentSeries.lean
@@ -89,7 +89,7 @@ structure on the `X`-adic completion of `K⸨X⸩`. Once this will be available,
 -/
 universe u
 
-open scoped Classical PowerSeries
+open scoped PowerSeries
 open HahnSeries Polynomial
 
 noncomputable section
@@ -541,6 +541,7 @@ theorem intValuation_eq_of_coe (P : K[X]) :
     (Ideal.span {↑P} : Ideal K⟦X⟧) ≠ 0 ∧ ((idealX K).asIdeal : Ideal K⟦X⟧) ≠ 0 := by
     simp only [Ideal.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot, coe_eq_zero_iff, hP,
       not_false_eq_true, true_and, (idealX K).3]
+  classical
   rw [count_associates_factors_eq  (span_ne_zero).1
     (Ideal.span_singleton_prime Polynomial.X_ne_zero|>.mpr prime_X) (span_ne_zero).2,
     count_associates_factors_eq]
diff --git a/Mathlib/RingTheory/Perfection.lean b/Mathlib/RingTheory/Perfection.lean
index 6dc12681fc5bd..210e3d6dbc519 100644
--- a/Mathlib/RingTheory/Perfection.lean
+++ b/Mathlib/RingTheory/Perfection.lean
@@ -454,10 +454,9 @@ instance : CharP (PreTilt K v O hv p) p :=
 
 section Classical
 
-open scoped Classical
-
 open Perfection
 
+open scoped Classical in
 /-- The valuation `Perfection(O/(p)) → ℝ≥0` as a function.
 Given `f ∈ Perfection(O/(p))`, if `f = 0` then output `0`;
 otherwise output `preVal(f(n))^(p^n)` for any `n` such that `f(n) ≠ 0`. -/
@@ -468,6 +467,7 @@ noncomputable def valAux (f : PreTilt K v O hv p) : ℝ≥0 :=
 
 variable {K v O hv p}
 
+open scoped Classical in
 theorem coeff_nat_find_add_ne_zero {f : PreTilt K v O hv p} {h : ∃ n, coeff _ _ n f ≠ 0} (k : ℕ) :
     coeff _ _ (Nat.find h + k) f ≠ 0 :=
   coeff_add_ne_zero (Nat.find_spec h) k
@@ -476,6 +476,7 @@ theorem valAux_eq {f : PreTilt K v O hv p} {n : ℕ} (hfn : coeff _ _ n f ≠ 0)
     valAux K v O hv p f = ModP.preVal K v O hv p (coeff _ _ n f) ^ p ^ n := by
   have h : ∃ n, coeff _ _ n f ≠ 0 := ⟨n, hfn⟩
   rw [valAux, dif_pos h]
+  classical
   obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.find_min' h hfn)
   induction' k with k ih
   · rfl
diff --git a/Mathlib/RingTheory/PrincipalIdealDomain.lean b/Mathlib/RingTheory/PrincipalIdealDomain.lean
index 77a6f3b5770e5..58ef2b97976b3 100644
--- a/Mathlib/RingTheory/PrincipalIdealDomain.lean
+++ b/Mathlib/RingTheory/PrincipalIdealDomain.lean
@@ -307,8 +307,7 @@ variable [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
 
 section
 
-open scoped Classical
-
+open scoped Classical in
 /-- `factors a` is a multiset of irreducible elements whose product is `a`, up to units -/
 noncomputable def factors (a : R) : Multiset R :=
   if h : a = 0 then ∅ else Classical.choose (WfDvdMonoid.exists_factors a h)
diff --git a/Mathlib/RingTheory/Radical.lean b/Mathlib/RingTheory/Radical.lean
index a213f7b39bfec..50e56b9aa02d5 100644
--- a/Mathlib/RingTheory/Radical.lean
+++ b/Mathlib/RingTheory/Radical.lean
@@ -47,14 +47,13 @@ This is different from the radical of an ideal.
 
 noncomputable section
 
-open scoped Classical
-
 namespace UniqueFactorizationMonoid
 
 -- `CancelCommMonoidWithZero` is required by `UniqueFactorizationMonoid`
 variable {M : Type*} [CancelCommMonoidWithZero M] [NormalizationMonoid M]
   [UniqueFactorizationMonoid M]
 
+open scoped Classical in
 /-- The finite set of prime factors of an element in a unique factorization monoid. -/
 def primeFactors (a : M) : Finset M :=
   (normalizedFactors a).toFinset
@@ -74,10 +73,12 @@ def radical (a : M) : M :=
 
 @[simp]
 theorem radical_zero_eq : radical (0 : M) = 1 := by
+  classical
   rw [radical, primeFactors, normalizedFactors_zero, Multiset.toFinset_zero, Finset.prod_empty]
 
 @[simp]
 theorem radical_one_eq : radical (1 : M) = 1 := by
+  classical
   rw [radical, primeFactors, normalizedFactors_one, Multiset.toFinset_zero, Finset.prod_empty]
 
 theorem radical_eq_of_associated {a b : M} (h : Associated a b) : radical a = radical b := by
@@ -100,6 +101,7 @@ theorem radical_pow (a : M) {n : Nat} (hn : 0 < n) : radical (a ^ n) = radical a
   simp_rw [radical, primeFactors_pow a hn]
 
 theorem radical_dvd_self (a : M) : radical a ∣ a := by
+  classical
   by_cases ha : a = 0
   · rw [ha]
     apply dvd_zero
@@ -147,13 +149,15 @@ theorem disjoint_normalizedFactors {a b : R} (hc : IsCoprime a b) :
 
 /-- Coprime elements have disjoint prime factors (as finsets). -/
 theorem disjoint_primeFactors {a b : R} (hc : IsCoprime a b) :
-    Disjoint (primeFactors a) (primeFactors b) :=
-  Multiset.disjoint_toFinset.mpr (disjoint_normalizedFactors hc)
+    Disjoint (primeFactors a) (primeFactors b) := by
+  classical
+  exact Multiset.disjoint_toFinset.mpr (disjoint_normalizedFactors hc)
 
 theorem mul_primeFactors_disjUnion {a b : R} (ha : a ≠ 0) (hb : b ≠ 0)
     (hc : IsCoprime a b) :
     primeFactors (a * b) =
     (primeFactors a).disjUnion (primeFactors b) (disjoint_primeFactors hc) := by
+  classical
   rw [Finset.disjUnion_eq_union]
   simp_rw [primeFactors]
   rw [normalizedFactors_mul ha hb, Multiset.toFinset_add]
diff --git a/Mathlib/RingTheory/Spectrum/Maximal/Basic.lean b/Mathlib/RingTheory/Spectrum/Maximal/Basic.lean
index 536e6f256c14d..e13efc0c60bcb 100644
--- a/Mathlib/RingTheory/Spectrum/Maximal/Basic.lean
+++ b/Mathlib/RingTheory/Spectrum/Maximal/Basic.lean
@@ -14,8 +14,6 @@ Basic properties the maximal spectrum of a ring.
 
 noncomputable section
 
-open scoped Classical
-
 variable (R S P : Type*) [CommSemiring R] [CommSemiring S] [CommSemiring P]
 
 namespace MaximalSpectrum
diff --git a/Mathlib/RingTheory/Spectrum/Prime/Basic.lean b/Mathlib/RingTheory/Spectrum/Prime/Basic.lean
index c789426f03c36..0f54c2ec83cac 100644
--- a/Mathlib/RingTheory/Spectrum/Prime/Basic.lean
+++ b/Mathlib/RingTheory/Spectrum/Prime/Basic.lean
@@ -42,7 +42,7 @@ assert_not_exists TopologicalSpace
 
 noncomputable section
 
-open scoped Classical Pointwise
+open scoped Pointwise
 
 universe u v
 
@@ -560,6 +560,7 @@ and is a homeomorphism when ι is finite. -/
   | ⟨i, p⟩ => (Pi.evalRingHom R i).specComap p
 
 theorem sigmaToPi_injective : (sigmaToPi R).Injective := fun ⟨i, p⟩ ⟨j, q⟩ eq ↦ by
+  classical
   obtain rfl | ne := eq_or_ne i j
   · congr; ext x
     simpa using congr_arg (Function.update (0 : ∀ i, R i) i x ∈ ·.asIdeal) eq
@@ -575,6 +576,7 @@ range of `sigmaToPi`, i.e. is not of the form `πᵢ⁻¹(𝔭)` for some prime
 see https://math.stackexchange.com/a/1563190. -/
 theorem exists_maximal_nmem_range_sigmaToPi_of_infinite :
     ∃ (I : Ideal (Π i, R i)) (_ : I.IsMaximal), ⟨I, inferInstance⟩ ∉ Set.range (sigmaToPi R) := by
+  classical
   let J : Ideal (Π i, R i) := -- `J := Π₀ i, R i` is an ideal in `Π i, R i`
   { __ := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom
     smul_mem' := by
diff --git a/Mathlib/RingTheory/Valuation/Basic.lean b/Mathlib/RingTheory/Valuation/Basic.lean
index 5ff8726949782..d188fcced5444 100644
--- a/Mathlib/RingTheory/Valuation/Basic.lean
+++ b/Mathlib/RingTheory/Valuation/Basic.lean
@@ -57,7 +57,6 @@ If ever someone extends `Valuation`, we should fully comply to the `DFunLike` by
 boilerplate lemmas to `ValuationClass`.
 -/
 
-open scoped Classical
 open Function Ideal
 
 noncomputable section
@@ -168,6 +167,7 @@ theorem map_add_lt {x y g} (hx : v x < g) (hy : v y < g) : v (x + y) < g :=
 
 theorem map_sum_le {ι : Type*} {s : Finset ι} {f : ι → R} {g : Γ₀} (hf : ∀ i ∈ s, v (f i) ≤ g) :
     v (∑ i ∈ s, f i) ≤ g := by
+  classical
   refine
     Finset.induction_on s (fun _ => v.map_zero ▸ zero_le')
       (fun a s has ih hf => ?_) hf
@@ -176,6 +176,7 @@ theorem map_sum_le {ι : Type*} {s : Finset ι} {f : ι → R} {g : Γ₀} (hf :
 
 theorem map_sum_lt {ι : Type*} {s : Finset ι} {f : ι → R} {g : Γ₀} (hg : g ≠ 0)
     (hf : ∀ i ∈ s, v (f i) < g) : v (∑ i ∈ s, f i) < g := by
+  classical
   refine
     Finset.induction_on s (fun _ => v.map_zero ▸ (zero_lt_iff.2 hg))
       (fun a s has ih hf => ?_) hf
@@ -305,6 +306,7 @@ theorem map_sub_eq_of_lt_right (h : v x < v y) : v (x - y) = v y := by
   rw [sub_eq_add_neg, map_add_eq_of_lt_right, map_neg]
   rwa [map_neg]
 
+open scoped Classical in
 theorem map_sum_eq_of_lt {ι : Type*} {s : Finset ι} {f : ι → R} {j : ι}
     (hj : j ∈ s) (h0 : v (f j) ≠ 0) (hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)) :
     v (∑ i ∈ s, f i) = v (f j) := by