diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean
index 1941b813..71b3e35e 100644
--- a/SphereEversion/Local/HPrinciple.lean
+++ b/SphereEversion/Local/HPrinciple.lean
@@ -53,7 +53,7 @@ need to access its components only once.
 
 noncomputable section
 
-open scoped unitInterval Classical Filter Topology
+open scoped unitInterval Filter Topology
 
 open Filter Set RelLoc
 
@@ -94,8 +94,6 @@ structure StepLandscape extends Landscape E where
 
 variable {E}
 
-open scoped Classical
-
 variable (R : RelLoc E F)
 
 namespace StepLandscape
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean
index f17c0f0c..22163248 100644
--- a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean
+++ b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean
@@ -12,12 +12,9 @@ import Mathlib.Topology.VectorBundle.Hom
 # Various operations on and properties of smooth vector bundles
 -/
 
-
 noncomputable section
 
-open Bundle Set TopologicalSpace PartialHomeomorph
-
-open scoped Classical Manifold Bundle
+open Bundle Set
 
 namespace FiberBundle
 
diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean
index e30177c2..8d83dcf1 100644
--- a/SphereEversion/ToMathlib/Topology/Misc.lean
+++ b/SphereEversion/ToMathlib/Topology/Misc.lean
@@ -6,13 +6,10 @@ import Mathlib.Topology.Algebra.Order.Floor
 noncomputable section
 
 open Set Function Filter TopologicalSpace
-
-open scoped unitInterval Topology uniformity Filter Classical
+open scoped unitInterval Topology uniformity
 
 section Maps
 
-open Function Set
-
 variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : β → α}
 
 -- TODO: move to Data.Set.Defs
@@ -205,7 +202,7 @@ section
 -- TODO: move to Mathlib.Topology.Constructions
 -- needs classical
 variable {α β γ δ ι : Type*} [TopologicalSpace α] [TopologicalSpace β] {x : α}
-
+open scoped Classical in
 theorem isOpen_slice_of_isOpen_over {Ω : Set (α × β)} {x₀ : α}
     (hΩ_op : ∃ U ∈ 𝓝 x₀, IsOpen (Ω ∩ Prod.fst ⁻¹' U)) : IsOpen (Prod.mk x₀ ⁻¹' Ω) := by
   rcases hΩ_op with ⟨U, hU, hU_op⟩; convert hU_op.preimage (Continuous.Prod.mk x₀) using 1
@@ -333,8 +330,6 @@ theorem decode₂_locallyFinite {ι} [Encodable ι] {s : ι → Set α} (hs : Lo
   simp_rw [mem_setOf_eq, h, map_none, getD_none, empty_inter] at hn
   exact (not_nonempty_empty hn).elim
 
-open TopologicalSpace
-
 variable {X : Type*} [EMetricSpace X] [LocallyCompactSpace X] [SecondCountableTopology X]
 
 theorem exists_locallyFinite_subcover_of_locally {C : Set X} (hC : IsClosed C) {P : Set X → Prop}
@@ -428,6 +423,7 @@ theorem cover_nat_nhdsWithin {α} [TopologicalSpace α] [SecondCountableTopology
   rw [biUnion_range] at hsf
   exact ⟨x, hts, hsf⟩
 
+open scoped Classical in
 /-- A version of `TopologicalSpace.cover_nat_nhdsWithin` where `f` is only defined on `s`. -/
 theorem cover_nat_nhdsWithin' {α} [TopologicalSpace α] [SecondCountableTopology α] {s : Set α}
     {f : ∀ x ∈ s, Set α} (hf : ∀ (x) (hx : x ∈ s), f x hx ∈ 𝓝[s] x) (hs : s.Nonempty) :
@@ -523,8 +519,6 @@ theorem exists_subset_iUnion_interior_of_isOpen (hs : IsOpen s) (uo : ∀ i, IsO
 
 end ShrinkingLemma
 
-open scoped Filter
-
 theorem Filter.EventuallyEq.slice {α β γ : Type*} [TopologicalSpace α] [TopologicalSpace β]
     {f g : α × β → γ} {a : α} {b : β} (h : f =ᶠ[𝓝 (a, b)] g) :
     (fun y ↦ f (a, y)) =ᶠ[𝓝 b] fun y ↦ g (a, y) :=