chore(Logic): remove bare open Classical (#15836)

Author: grunweg

Mathlib/Logic/Denumerable.lean

@@ -184,22 +184,19 @@ open Function Encodable
 
 /-! ### Subsets of `ℕ` -/
 
-
 variable {s : Set ℕ} [Infinite s]
 
 section Classical
 
-open scoped Classical
-
-theorem exists_succ (x : s) : ∃ n, (x : ℕ) + n + 1 ∈ s :=
-  _root_.by_contradiction fun h =>
-    have : ∀ (a : ℕ) (_ : a ∈ s), a < x + 1 := fun a ha =>
-      lt_of_not_ge fun hax => h ⟨a - (x + 1), by rwa [add_right_comm, Nat.add_sub_cancel' hax]⟩
-    Fintype.false
-      ⟨(((Multiset.range (succ x)).filter (· ∈ s)).pmap
-            (fun (y : ℕ) (hy : y ∈ s) => Subtype.mk y hy)
-            (by simp [-Multiset.range_succ])).toFinset,
-        by simpa [Subtype.ext_iff_val, Multiset.mem_filter, -Multiset.range_succ] ⟩
+theorem exists_succ (x : s) : ∃ n, (x : ℕ) + n + 1 ∈ s := by
+  by_contra h
+  have : ∀ (a : ℕ) (_ : a ∈ s), a < x + 1 := fun a ha =>
+    lt_of_not_ge fun hax => h ⟨a - (x + 1), by rwa [add_right_comm, Nat.add_sub_cancel' hax]⟩
+  classical
+  exact Fintype.false
+    ⟨(((Multiset.range (succ x)).filter (· ∈ s)).pmap
+      (fun (y : ℕ) (hy : y ∈ s) => Subtype.mk y hy) (by simp [-Multiset.range_succ])).toFinset,
+      by simpa [Subtype.ext_iff_val, Multiset.mem_filter, -Multiset.range_succ] ⟩
 
 end Classical
 

Mathlib/Logic/Nontrivial/Basic.lean

@@ -16,11 +16,8 @@ import Mathlib.Tactic.Attr.Register
 Results about `Nontrivial`.
 -/
 
-
 variable {α : Type*} {β : Type*}
 
-open scoped Classical
-
 -- `x` and `y` are explicit here, as they are often needed to guide typechecking of `h`.
 theorem nontrivial_of_lt [Preorder α] (x y : α) (h : x < y) : Nontrivial α :=
   ⟨⟨x, y, ne_of_lt h⟩⟩
@@ -36,6 +33,7 @@ theorem Subtype.nontrivial_iff_exists_ne (p : α → Prop) (x : Subtype p) :
     Nontrivial (Subtype p) ↔ ∃ (y : α) (_ : p y), y ≠ x := by
   simp only [_root_.nontrivial_iff_exists_ne x, Subtype.exists, Ne, Subtype.ext_iff]
 
+open Classical in
 /-- An inhabited type is either nontrivial, or has a unique element. -/
 noncomputable def nontrivialPSumUnique (α : Type*) [Inhabited α] :
     Nontrivial α ⊕' Unique α :=
@@ -76,6 +74,7 @@ namespace Pi
 
 variable {I : Type*} {f : I → Type*}
 
+open Classical in
 /-- A pi type is nontrivial if it's nonempty everywhere and nontrivial somewhere. -/
 theorem nontrivial_at (i' : I) [inst : ∀ i, Nonempty (f i)] [Nontrivial (f i')] :
     Nontrivial (∀ i : I, f i) := by

Mathlib/Logic/Nontrivial/Defs.lean

@@ -19,11 +19,8 @@ We introduce a typeclass `Nontrivial` formalizing this property.
 Basic results about nontrivial types are in `Mathlib.Logic.Nontrivial.Basic`.
 -/
 
-
 variable {α : Type*} {β : Type*}
 
-open scoped Classical
-
 /-- Predicate typeclass for expressing that a type is not reduced to a single element. In rings,
 this is equivalent to `0 ≠ 1`. In vector spaces, this is equivalent to positive dimension. -/
 class Nontrivial (α : Type*) : Prop where
@@ -44,6 +41,7 @@ protected theorem Decidable.exists_ne [Nontrivial α] [DecidableEq α] (x : α)
     exact ⟨y', h.symm⟩
   · exact ⟨y, Ne.symm hx⟩
 
+open Classical in
 theorem exists_ne [Nontrivial α] (x : α) : ∃ y, y ≠ x := Decidable.exists_ne x
 
 -- `x` and `y` are explicit here, as they are often needed to guide typechecking of `h`.

Mathlib/Logic/Small/Basic.lean

@@ -16,8 +16,6 @@ universe u w v v'
 
 section
 
-open scoped Classical
-
 instance small_subtype (α : Type v) [Small.{w} α] (P : α → Prop) : Small.{w} { x // P x } :=
   small_map (equivShrink α).subtypeEquivOfSubtype'
 

Mathlib/Logic/Small/Defs.lean

@@ -88,8 +88,6 @@ theorem small_type : Small.{max (u + 1) v} (Type u) :=
 
 section
 
-open scoped Classical
-
 theorem small_congr {α : Type*} {β : Type*} (e : α ≃ β) : Small.{w} α ↔ Small.{w} β :=
   ⟨fun h => @small_map _ _ h e.symm, fun h => @small_map _ _ h e⟩