chore: remove redundant open scoped Classical (#41423)

felixpernegger · felixpernegger · commit ed0d70fdcde7 · 2026-07-08T09:06:14.000Z
This PR removes all redundant/unused `open scoped Classical in`. Furthermore, if the `open scoped Classical` is only needed for the proof of a declaration, it moves it there (and convert it to `classical` when in tactic mode). Excludes MathlibTest.

This was done with a script bruteforcing everything, made by Claude code.

Only thing remaining would be to check if all `classical` are really needed, but there are quite a lot of them (&gt;3k).

Co-authored-by: Batixx &lt;s59fpern@uni-bonn.de&gt;
diff --git a/Archive/Imo/Imo1998Q2.lean b/Archive/Imo/Imo1998Q2.lean
@@ -98,7 +98,6 @@ 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]
 
diff --git a/Mathlib/Analysis/Normed/Lp/ProdLp.lean b/Mathlib/Analysis/Normed/Lp/ProdLp.lean
@@ -162,7 +162,6 @@ section EDist
 
 variable [EDist α] [EDist β]
 
-open scoped Classical in
 /-- Endowing the space `WithLp p (α × β)` with the `L^p` edistance. We register this instance
 separate from `WithLp.instProdPseudoEMetric` since the latter requires the type class hypothesis
 `[Fact (1 ≤ p)]` in order to prove the triangle inequality.
@@ -231,7 +230,6 @@ section Dist
 
 variable [Dist α] [Dist β]
 
-open scoped Classical in
 /-- Endowing the space `WithLp p (α × β)` with the `L^p` distance. We register this instance
 separate from `WithLp.instProdPseudoMetricSpace` since the latter requires the type class hypothesis
 `[Fact (1 ≤ p)]` in order to prove the triangle inequality.
@@ -268,7 +266,6 @@ section Norm
 
 variable [Norm α] [Norm β]
 
-open scoped Classical in
 /-- Endowing the space `WithLp p (α × β)` with the `L^p` norm. We register this instance
 separate from `WithLp.instProdSeminormedAddCommGroup` since the latter requires the type class
 hypothesis `[Fact (1 ≤ p)]` in order to prove the triangle inequality.
diff --git a/Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean b/Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
@@ -52,8 +52,9 @@ noncomputable def ruzsaSzemerediNumber : ℕ := by
   exact Nat.findGreatest (fun m ↦ ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj),
     #(G.cliqueFinset 3) = m ∧ G.LocallyLinear) ((card α).choose 3)
 
-open scoped Classical in
-lemma ruzsaSzemerediNumber_le : ruzsaSzemerediNumber α ≤ (card α).choose 3 := Nat.findGreatest_le _
+lemma ruzsaSzemerediNumber_le : ruzsaSzemerediNumber α ≤ (card α).choose 3 := by
+  classical
+  exact Nat.findGreatest_le _
 
 lemma ruzsaSzemerediNumber_spec :
     ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj),
diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
@@ -549,8 +549,9 @@ lemma CliqueFree.mem_of_sup_edge_isNClique {x y : α} {t : Finset α} {n : ℕ}
 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) :=
-  fun _ hs ↦ (hs.erase_of_sup_edge_of_mem <|
+    (G ⊔ edge v w).CliqueFree (n + 1) := by
+  classical
+  exact fun _ hs ↦ (hs.erase_of_sup_edge_of_mem <|
     (h.mono n.le_succ).mem_of_sup_edge_isNClique hs).not_cliqueFree h
 
 lemma IsNClique.exists_not_adj_of_cliqueFree_succ (hc : G.IsNClique n s)
diff --git a/Mathlib/FieldTheory/Perfect.lean b/Mathlib/FieldTheory/Perfect.lean
@@ -455,7 +455,6 @@ noncomputable def rootsExpandToRoots : (expand R p f).roots.toFinset ↪ f.roots
 @[simp]
 theorem rootsExpandToRoots_apply (x) : (rootsExpandToRoots p f x : R) = x ^ p := rfl
 
-open scoped Classical in
 /-- If `f` is a polynomial over an integral domain `R` of characteristic `p`, then there is
 a map from the set of roots of `Polynomial.expand R (p ^ n) f` to the set of roots of `f`.
 It's given by `x ↦ x ^ (p ^ n)`, see `rootsExpandPowToRoots_apply`. -/
diff --git a/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean b/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean
@@ -118,6 +118,7 @@ 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
+  classical
   apply (Nat.find_eq_zero _).mpr
   rw [pow_zero, pow_one]
   obtain ⟨y, hy⟩ := h
diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean
@@ -523,7 +523,6 @@ def ChartedSpace.sum_of_nonempty [Nonempty H] : ChartedSpace H (M ⊕ M') where
       right
       use ChartedSpace.chartAt x, cm'.chart_mem_atlas x
 
-open scoped Classical in
 instance ChartedSpace.sum : ChartedSpace H (M ⊕ M') := by
   by_cases! h : Nonempty H
   · exact ChartedSpace.sum_of_nonempty
diff --git a/Mathlib/GroupTheory/Coxeter/Length.lean b/Mathlib/GroupTheory/Coxeter/Length.lean
@@ -90,9 +90,9 @@ theorem exists_isReduced (w : W) : ∃ ω : List B, cs.IsReduced ω ∧ w = π 
 @[deprecated (since := "2026-03-25")] alias exists_reduced_word := exists_isReduced
 @[deprecated (since := "2026-03-25")] alias exists_reduced_word' := exists_isReduced
 
-open scoped Classical in
-theorem length_wordProd_le (ω : List B) : ℓ (π ω) ≤ ω.length :=
-  Nat.find_min' (cs.exists_word_with_prod (π ω)) ⟨ω, rfl, rfl⟩
+theorem length_wordProd_le (ω : List B) : ℓ (π ω) ≤ ω.length := by
+  classical
+  exact Nat.find_min' (cs.exists_word_with_prod (π ω)) ⟨ω, rfl, rfl⟩
 
 @[simp] theorem length_one : ℓ (1 : W) = 0 := Nat.eq_zero_of_le_zero (cs.length_wordProd_le [])
 
diff --git a/Mathlib/GroupTheory/FreeAbelianGroup.lean b/Mathlib/GroupTheory/FreeAbelianGroup.lean
@@ -146,9 +146,9 @@ end lift
 
 section
 
-open scoped Classical in
-theorem of_injective : Function.Injective (of : α → FreeAbelianGroup α) :=
-  fun x y hoxy ↦ Classical.by_contradiction fun hxy : x ≠ y ↦
+theorem of_injective : Function.Injective (of : α → FreeAbelianGroup α) := by
+  classical
+  exact fun x y hoxy ↦ Classical.by_contradiction fun hxy : x ≠ y ↦
     let f : FreeAbelianGroup α →+ ℤ := lift fun z ↦ if x = z then (1 : ℤ) else 0
     have hfx1 : f (of x) = 1 := (lift_apply_of _ _).trans <| if_pos rfl
     have hfy1 : f (of y) = 1 := hoxy ▸ hfx1
diff --git a/Mathlib/GroupTheory/Perm/ViaEmbedding.lean b/Mathlib/GroupTheory/Perm/ViaEmbedding.lean
@@ -29,13 +29,13 @@ open scoped Classical in
 noncomputable def viaEmbedding : Perm β :=
   extendDomain e (ofInjective ι.1 ι.2)
 
-open scoped Classical in
-theorem viaEmbedding_apply (x : α) : e.viaEmbedding ι (ι x) = ι (e x) :=
-  extendDomain_apply_image e (ofInjective ι.1 ι.2) x
+theorem viaEmbedding_apply (x : α) : e.viaEmbedding ι (ι x) = ι (e x) := by
+  classical
+  exact extendDomain_apply_image e (ofInjective ι.1 ι.2) x
 
-open scoped Classical in
-theorem viaEmbedding_apply_of_notMem (x : β) (hx : x ∉ Set.range ι) : e.viaEmbedding ι x = x :=
-  extendDomain_apply_not_subtype e (ofInjective ι.1 ι.2) hx
+theorem viaEmbedding_apply_of_notMem (x : β) (hx : x ∉ Set.range ι) : e.viaEmbedding ι x = x := by
+  classical
+  exact extendDomain_apply_not_subtype e (ofInjective ι.1 ι.2) hx
 
 open scoped Classical in
 /-- `viaEmbedding` as a group homomorphism -/
@@ -45,9 +45,9 @@ noncomputable def viaEmbeddingHom : Perm α →* Perm β :=
 theorem viaEmbeddingHom_apply : viaEmbeddingHom ι e = viaEmbedding e ι :=
   rfl
 
-open scoped Classical in
-theorem viaEmbeddingHom_injective : Function.Injective (viaEmbeddingHom ι) :=
-  extendDomainHom_injective (ofInjective ι.1 ι.2)
+theorem viaEmbeddingHom_injective : Function.Injective (viaEmbeddingHom ι) := by
+  classical
+  exact extendDomainHom_injective (ofInjective ι.1 ι.2)
 
 end Perm
 
diff --git a/Mathlib/LinearAlgebra/Basis/VectorSpace.lean b/Mathlib/LinearAlgebra/Basis/VectorSpace.lean
@@ -257,7 +257,6 @@ theorem LinearMap.exists_leftInverse_of_injective (f : V →ₗ[K] V') (hf_inj :
   rw [Basis.ofVectorSpace_apply_self, fb_eq, hC.constr_basis]
   exact leftInverse_invFun (LinearMap.ker_eq_bot.1 hf_inj) _
 
-open scoped Classical in
 /-- The left inverse of `f : E →ₗ[𝕜] F`.
 
 If `f` is not injective, then we use the junk value `0`. -/
diff --git a/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean b/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
@@ -339,10 +339,10 @@ theorem Integrable.to_average {f : α → ε} (h : Integrable f μ) : Integrable
   · apply h.smul_measure
     simpa
 
-open scoped Classical in
 theorem integrable_average [IsFiniteMeasure μ] {f : α → ε} :
-    Integrable f ((μ univ)⁻¹ • μ) ↔ Integrable f μ :=
-  (eq_or_ne μ 0).by_cases (fun h => by simp [h]) fun h =>
+    Integrable f ((μ univ)⁻¹ • μ) ↔ Integrable f μ := by
+  classical
+  exact (eq_or_ne μ 0).by_cases (fun h => by simp [h]) fun h =>
     integrable_smul_measure (ENNReal.inv_ne_zero.2 <| by finiteness)
       (ENNReal.inv_ne_top.2 <| mt Measure.measure_univ_eq_zero.1 h)
 
diff --git a/Mathlib/MeasureTheory/Function/SimpleFunc.lean b/Mathlib/MeasureTheory/Function/SimpleFunc.lean
@@ -215,11 +215,11 @@ theorem piecewise_univ (f g : α →ₛ β) : piecewise univ MeasurableSet.univ
 theorem piecewise_empty (f g : α →ₛ β) : piecewise ∅ MeasurableSet.empty f g = g :=
   coe_injective <| by simp
 
-open scoped Classical in
 @[simp]
 theorem piecewise_same (f : α →ₛ β) {s : Set α} (hs : MeasurableSet s) :
-    piecewise s hs f f = f :=
-  coe_injective <| Set.piecewise_same _ _
+    piecewise s hs f f = f := by
+  classical
+  exact coe_injective <| Set.piecewise_same _ _
 
 theorem support_indicator [Zero β] {s : Set α} (hs : MeasurableSet s) (f : α →ₛ β) :
     Function.support (f.piecewise s hs (SimpleFunc.const α 0)) = s ∩ Function.support f :=
@@ -674,10 +674,11 @@ lemma mk_le_mk {f g : α → β} {hf hg hf' hg'} : mk f hf hf' ≤ mk g hg hg' 
 @[simp, gcongr]
 lemma mk_lt_mk {f g : α → β} {hf hg hf' hg'} : mk f hf hf' < mk g hg hg' ↔ f < g := Iff.rfl
 
-open scoped Classical in
 @[gcongr only]
 lemma piecewise_mono (hf : ∀ a ∈ s, f₁ a ≤ f₂ a) (hg : ∀ a ∉ s, g₁ a ≤ g₂ a) :
-    piecewise s hs f₁ g₁ ≤ piecewise s hs f₂ g₂ := Set.piecewise_mono hf hg
+    piecewise s hs f₁ g₁ ≤ piecewise s hs f₂ g₂ := by
+  classical
+  exact Set.piecewise_mono hf hg
 
 end Preorder
 
@@ -751,10 +752,10 @@ theorem restrict_univ (f : α →ₛ β) : restrict f univ = f := by simp [restr
 @[simp]
 theorem restrict_empty (f : α →ₛ β) : restrict f ∅ = 0 := by simp [restrict]
 
-open scoped Classical in
 theorem map_restrict_of_zero [Zero γ] {g : β → γ} (hg : g 0 = 0) (f : α →ₛ β) (s : Set α) :
-    (f.restrict s).map g = (f.map g).restrict s :=
-  ext fun x =>
+    (f.restrict s).map g = (f.map g).restrict s := by
+  classical
+  exact ext fun x =>
     if hs : MeasurableSet s then by simp [hs, Set.indicator_comp_of_zero hg]
     else by simp [restrict_of_not_measurable hs, hg]
 
@@ -781,19 +782,19 @@ theorem mem_restrict_range {r : β} {s : Set α} {f : α →ₛ β} (hs : Measur
     r ∈ (restrict f s).range ↔ r = 0 ∧ s ≠ univ ∨ r ∈ f '' s := by
   rw [← Finset.mem_coe, coe_range, coe_restrict _ hs, mem_range_indicator]
 
-open scoped Classical in
 theorem mem_image_of_mem_range_restrict {r : β} {s : Set α} {f : α →ₛ β}
-    (hr : r ∈ (restrict f s).range) (h0 : r ≠ 0) : r ∈ f '' s :=
-  if hs : MeasurableSet s then by simpa [mem_restrict_range hs, h0, -mem_range] using hr
+    (hr : r ∈ (restrict f s).range) (h0 : r ≠ 0) : r ∈ f '' s := by
+  classical
+  exact if hs : MeasurableSet s then by simpa [mem_restrict_range hs, h0, -mem_range] using hr
   else by
     rw [restrict_of_not_measurable hs] at hr
     exact (h0 <| eq_zero_of_mem_range_zero hr).elim
 
-open scoped Classical in
 @[gcongr, mono]
 theorem restrict_mono [Preorder β] (s : Set α) {f g : α →ₛ β} (H : f ≤ g) :
-    f.restrict s ≤ g.restrict s :=
-  if hs : MeasurableSet s then fun x => by
+    f.restrict s ≤ g.restrict s := by
+  classical
+  exact if hs : MeasurableSet s then fun x => by
     simp only [coe_restrict _ hs, indicator_le_indicator (H x)]
   else by simp only [restrict_of_not_measurable hs, le_refl]
 
@@ -1030,10 +1031,10 @@ theorem lintegral_sum {m : MeasurableSpace α} {ι} (f : α →ₛ ℝ≥0∞) (
     ENNReal.tsum_mul_left]
   apply ENNReal.tsum_comm
 
-open scoped Classical in
 theorem restrict_lintegral (f : α →ₛ ℝ≥0∞) {s : Set α} (hs : MeasurableSet s) :
-    (restrict f s).lintegral μ = ∑ r ∈ f.range, r * μ (f ⁻¹' {r} ∩ s) :=
-  calc
+    (restrict f s).lintegral μ = ∑ r ∈ f.range, r * μ (f ⁻¹' {r} ∩ s) := by
+  classical
+  exact calc
     (restrict f s).lintegral μ = ∑ r ∈ f.range, r * μ (restrict f s ⁻¹' {r}) :=
       lintegral_eq_of_subset _ fun x hx =>
         if hxs : x ∈ s then fun _ => by
diff --git a/Mathlib/MeasureTheory/Measure/Stieltjes.lean b/Mathlib/MeasureTheory/Measure/Stieltjes.lean
@@ -76,7 +76,6 @@ lemma isOpen_Iotop [TopologicalSpace R] [OrderTopology R] (a b : R) : IsOpen (Io
     simp [this, isOpen_Ioi]
   · simp [isOpen_Ioo]
 
-open scoped Classical in
 /-- `botSet` is the set of all bottom elements. -/
 def botSet : Set R := {x | IsBot x}
 
diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean b/Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean
@@ -148,15 +148,15 @@ open scoped Classical in
 noncomputable def spanningSetsIndex (μ : Measure α) [SigmaFinite μ] (x : α) : ℕ :=
   Nat.find <| iUnion_eq_univ_iff.1 (iUnion_spanningSets μ) x
 
-open scoped Classical in
 theorem measurableSet_spanningSetsIndex (μ : Measure α) [SigmaFinite μ] :
-    Measurable (spanningSetsIndex μ) :=
-  measurable_find _ <| measurableSet_spanningSets μ
+    Measurable (spanningSetsIndex μ) := by
+  classical
+  exact measurable_find _ <| measurableSet_spanningSets μ
 
-open scoped Classical in
 theorem preimage_spanningSetsIndex_singleton (μ : Measure α) [SigmaFinite μ] (n : ℕ) :
-    spanningSetsIndex μ ⁻¹' {n} = disjointed (spanningSets μ) n :=
-  preimage_find_eq_disjointed _ _ _
+    spanningSetsIndex μ ⁻¹' {n} = disjointed (spanningSets μ) n := by
+  classical
+  exact preimage_find_eq_disjointed _ _ _
 
 theorem spanningSetsIndex_eq_iff (μ : Measure α) [SigmaFinite μ] {x : α} {n : ℕ} :
     spanningSetsIndex μ x = n ↔ x ∈ disjointed (spanningSets μ) n := by
diff --git a/Mathlib/MeasureTheory/SetSemiring.lean b/Mathlib/MeasureTheory/SetSemiring.lean
@@ -148,7 +148,6 @@ theorem isSetRing_supClosure (hC : IsSetSemiring C) : IsSetRing (supClosure C) w
 
 section disjointOfDiff
 
-open scoped Classical in
 /-- In a semi-ring of sets `C`, for all sets `s, t ∈ C`, `s \ t` is equal to a disjoint union of
 finitely many sets in `C`. The finite set of sets in the union is not unique, but this definition
 gives an arbitrary `Finset (Set α)` that satisfies the equality.
@@ -291,7 +290,6 @@ lemma exists_disjoint_finset_sdiff_eq (hC : IsSetSemiring C) (hs : s ∈ C) (hI
 @[deprecated (since := "2026-06-03")]
 alias exists_disjoint_finset_diff_eq := exists_disjoint_finset_sdiff_eq
 
-open scoped Classical in
 /-- In a semiring of sets `C`, for all set `s ∈ C` and finite set of sets `I ⊆ C`,
 `disjointOfDiffUnion` is a finite set of sets in `C` such that
 `s \ ⋃₀ I = ⋃₀ (hC.disjointOfDiffUnion hs I hI)`.
diff --git a/Mathlib/NumberTheory/RamificationInertia/Basic.lean b/Mathlib/NumberTheory/RamificationInertia/Basic.lean
@@ -491,47 +491,39 @@ section FactorsMap
 
 variable [IsDedekindDomain S]
 
-open scoped Classical in
 theorem Factors.ne_bot (P : (factors (map (algebraMap R S) p)).toFinset) : (P : Ideal S) ≠ ⊥ :=
   (prime_of_factor _ (Multiset.mem_toFinset.mp P.2)).ne_zero
 
-open scoped Classical in
 instance Factors.isPrime (P : (factors (map (algebraMap R S) p)).toFinset) :
     IsPrime (P : Ideal S) :=
   Ideal.isPrime_of_prime (prime_of_factor _ (Multiset.mem_toFinset.mp P.2))
 
-open scoped Classical in
 theorem Factors.ramificationIdx_ne_zero (P : (factors (map (algebraMap R S) p)).toFinset) :
     ramificationIdx' p P.1 ≠ 0 :=
   IsDedekindDomain.ramificationIdx'_ne_zero (ne_zero_of_mem_factors (Multiset.mem_toFinset.mp P.2))
     (Factors.isPrime p P) (Ideal.le_of_dvd (dvd_of_mem_factors (Multiset.mem_toFinset.mp P.2)))
 
-open scoped Classical in
 instance Factors.fact_ramificationIdx_neZero (P : (factors (map (algebraMap R S) p)).toFinset) :
     NeZero (ramificationIdx' p P.1) :=
   ⟨Factors.ramificationIdx_ne_zero p P⟩
 
 attribute [local instance] Quotient.algebraQuotientOfRamificationIdxNeZero
 
-open scoped Classical in
 instance Factors.isScalarTower (P : (factors (map (algebraMap R S) p)).toFinset) :
     IsScalarTower R (R ⧸ p) (S ⧸ (P : Ideal S)) :=
   IsScalarTower.of_algebraMap_eq' rfl
 
-open scoped Classical in
 instance Factors.liesOver [p.IsMaximal] (P : (factors (map (algebraMap R S) p)).toFinset) :
     P.1.LiesOver p :=
   ⟨(comap_eq_of_scalar_tower_quotient (algebraMap (R ⧸ p) (S ⧸ P.1)).injective).symm⟩
 
-open scoped Classical in
 theorem Factors.finrank_pow_ramificationIdx [p.IsMaximal]
     (P : (factors (map (algebraMap R S) p)).toFinset) :
     finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ ramificationIdx' p P.1) =
       ramificationIdx' p P.1 * inertiaDeg' p (P : Ideal S) := by
   rw [finrank_prime_pow_ramificationIdx, inertiaDeg'_algebraMap]
   exacts [Factors.ne_bot p P, NeZero.ne _]
 
-open scoped Classical in
 instance Factors.finiteDimensional_quotient_pow [Module.Finite R S] [p.IsMaximal]
     (P : (factors (map (algebraMap R S) p)).toFinset) :
     FiniteDimensional (R ⧸ p) (S ⧸ (P : Ideal S) ^ ramificationIdx' p P.1) := by
@@ -541,7 +533,6 @@ instance Factors.finiteDimensional_quotient_pow [Module.Finite R S] [p.IsMaximal
 
 universe w
 
-open scoped Classical in
 /-- **Chinese remainder theorem** for a ring of integers: if the prime ideal `p : Ideal R`
 factors in `S` as `∏ i, P i ^ e i`, then `S ⧸ I` factors as `Π i, R ⧸ (P i ^ e i)`. -/
 noncomputable def Factors.piQuotientEquiv (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) :
@@ -568,7 +559,6 @@ theorem Factors.piQuotientEquiv_map (p : Ideal R) (hp : map (algebraMap R S) p 
 
 variable (S)
 
-open scoped Classical in
 /-- **Chinese remainder theorem** for a ring of integers: if the prime ideal `p : Ideal R`
 factors in `S` as `∏ i, P i ^ e i`,
 then `S ⧸ I` factors `R ⧸ I`-linearly as `Π i, R ⧸ (P i ^ e i)`. -/
@@ -588,7 +578,6 @@ variable (K L : Type*) [Field K] [Field L] [IsDedekindDomain R] [Algebra R K] [I
   [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L]
   [IsScalarTower R K L] [Module.Finite R S]
 
-open scoped Classical in
 /-- The **fundamental identity** of ramification index `e` and inertia degree `f`:
 for `P` ranging over the primes lying over `p`, `∑ P, e P * f P = [Frac(S) : Frac(R)]`;
 here `S` is a finite `R`-module (and thus `Frac(S) : Frac(R)` is a finite extension) and `p`
diff --git a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
@@ -91,7 +91,6 @@ theorem intValuationDef_if_pos {r : R} (hr : r = 0) : v.intValuationDef r = 0 :=
 theorem intValuationDef_zero : v.intValuationDef 0 = 0 :=
   if_pos rfl
 
-open scoped Classical in
 theorem intValuationDef_if_neg {r : R} (hr : r ≠ 0) :
     v.intValuationDef r = exp
         (-(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r} : Ideal R)).factors : ℤ) :=
diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
diff --git a/Mathlib/RingTheory/Spectrum/Maximal/Localization.lean b/Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
diff --git a/Mathlib/Topology/Category/Profinite/Nobeling/Induction.lean b/Mathlib/Topology/Category/Profinite/Nobeling/Induction.lean
diff --git a/Mathlib/Topology/Category/Profinite/Nobeling/Span.lean b/Mathlib/Topology/Category/Profinite/Nobeling/Span.lean
diff --git a/Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean b/Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean
