chore: scope open Classical (#11199)

We remove all but one `open Classical`s, instead preferring to use `open scoped Classical`. The only real side-effect this led to is moving a couple declarations to use `Exists.choose` instead of `Classical.choose`. The first few commits are explicitly labelled regex replaces for ease of review.
leanprover-community · Mar 22, 2024 · e88540e · e88540e
1 parent 0be0dbb
commit e88540e
Show file tree

Hide file tree

Showing 301 changed files with 561 additions and 384 deletions.
diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean
@@ -346,7 +346,7 @@ end
 
 section DecidableEq
 
-open Classical
+open scoped Classical
 
 theorem mem_span_mul_finite_of_mem_span_mul {R A} [Semiring R] [AddCommMonoid A] [Mul A]
     [Module R A] {S : Set A} {S' : Set A} {x : A} (hx : x ∈ span R (S * S')) :

diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean
@@ -89,7 +89,7 @@ section
 
 /- Note: we use classical logic only for these definitions, to ensure that we do not write lemmas
 with `Classical.dec` in their statement. -/
-open Classical
+open scoped Classical
 
 /-- Sum of `f x` as `x` ranges over the elements of the support of `f`, if it's finite. Zero
 otherwise. -/

diff --git a/Mathlib/Algebra/BigOperators/Finsupp.lean b/Mathlib/Algebra/BigOperators/Finsupp.lean
@@ -688,7 +688,7 @@ theorem Finsupp.sum_apply' : g.sum k x = g.sum fun i b => k i b x :=
 
 section
 
-open Classical
+open scoped Classical
 
 theorem Finsupp.sum_sum_index' : (∑ x in s, f x).sum t = ∑ x in s, (f x).sum t :=
   Finset.induction_on s rfl fun a s has ih => by

diff --git a/Mathlib/Algebra/Category/GroupCat/FilteredColimits.lean b/Mathlib/Algebra/Category/GroupCat/FilteredColimits.lean
@@ -29,7 +29,7 @@ universe v u
 
 noncomputable section
 
-open Classical
+open scoped Classical
 
 open CategoryTheory
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@@ -27,7 +27,7 @@ namespace ModuleCat
 
 universe u
 
-open Classical
+open scoped Classical
 
 variable (R : Type u)
 

diff --git a/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean b/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean
@@ -29,7 +29,7 @@ universe v u
 
 noncomputable section
 
-open Classical
+open scoped Classical
 
 open CategoryTheory
 

diff --git a/Mathlib/Algebra/Category/Ring/Adjunctions.lean b/Mathlib/Algebra/Category/Ring/Adjunctions.lean
@@ -25,7 +25,7 @@ open CategoryTheory
 namespace CommRingCat
 set_option linter.uppercaseLean3 false -- `CommRing`
 
-open Classical
+open scoped Classical
 
 /-- The free functor `Type u ⥤ CommRingCat` sending a type `X` to the multivariable (commutative)
 polynomials with variables `x : X`.

diff --git a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean
@@ -27,7 +27,7 @@ universe v u
 
 noncomputable section
 
-open Classical
+open scoped Classical
 
 open CategoryTheory
 

diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean
@@ -264,7 +264,7 @@ end functorial
 
 section Totalize
 
-open Classical
+open scoped Classical
 
 variable (G f)
 
@@ -289,7 +289,7 @@ end Totalize
 
 variable [DirectedSystem G fun i j h => f i j h]
 
-open Classical
+open scoped Classical
 
 theorem toModule_totalize_of_le {x : DirectSum ι G} {i j : ι} (hij : i ≤ j)
     (hx : ∀ k ∈ x.support, k ≤ i) :
@@ -633,7 +633,7 @@ theorem exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)] (z : DirectLimit G f
 
 section
 
-open Classical
+open scoped Classical
 
 open Polynomial
 
@@ -667,7 +667,7 @@ theorem induction_on [Nonempty ι] [IsDirected ι (· ≤ ·)] {C : DirectLimit
 
 section OfZeroExact
 
-open Classical
+open scoped Classical
 
 variable (f' : ∀ i j, i ≤ j → G i →+* G j)
 
@@ -1003,7 +1003,7 @@ theorem exists_inv {p : Ring.DirectLimit G f} : p ≠ 0 → ∃ y, p * y = 1 :=
 
 section
 
-open Classical
+open scoped Classical
 
 /-- Noncomputable multiplicative inverse in a direct limit of fields. -/
 noncomputable def inv (p : Ring.DirectLimit G f) : Ring.DirectLimit G f :=

diff --git a/Mathlib/Algebra/EuclideanDomain/Defs.lean b/Mathlib/Algebra/EuclideanDomain/Defs.lean
@@ -173,7 +173,7 @@ theorem div_zero (a : R) : a / 0 = 0 :=
 
 section
 
-open Classical
+open scoped Classical
 
 @[elab_as_elim]
 theorem GCD.induction {P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x)

diff --git a/Mathlib/Algebra/Field/IsField.lean b/Mathlib/Algebra/Field/IsField.lean
@@ -60,7 +60,7 @@ theorem not_isField_of_subsingleton (R : Type u) [Semiring R] [Subsingleton R] :
   h (Subsingleton.elim _ _)
 #align not_is_field_of_subsingleton not_isField_of_subsingleton
 
-open Classical
+open scoped Classical
 
 /-- Transferring from `IsField` to `Semifield`. -/
 noncomputable def IsField.toSemifield {R : Type u} [Semiring R] (h : IsField R) : Semifield R :=

diff --git a/Mathlib/Algebra/GCDMonoid/Div.lean b/Mathlib/Algebra/GCDMonoid/Div.lean
@@ -70,7 +70,8 @@ end Int
 
 namespace Polynomial
 
-open Polynomial Classical
+open scoped Classical
+open Polynomial
 
 noncomputable section
 

diff --git a/Mathlib/Algebra/GroupWithZero/Basic.lean b/Mathlib/Algebra/GroupWithZero/Basic.lean
@@ -36,7 +36,7 @@ and require `0⁻¹ = 0`.
 -/
 
 
-open Classical
+open scoped Classical
 
 open Function
 

diff --git a/Mathlib/Algebra/GroupWithZero/Commute.lean b/Mathlib/Algebra/GroupWithZero/Commute.lean
@@ -21,7 +21,7 @@ variable [MonoidWithZero M₀]
 
 namespace Ring
 
-open Classical
+open scoped Classical
 
 theorem mul_inverse_rev' {a b : M₀} (h : Commute a b) :
     inverse (a * b) = inverse b * inverse a := by

diff --git a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean
@@ -78,7 +78,7 @@ theorem not_isUnit_zero [Nontrivial M₀] : ¬IsUnit (0 : M₀) :=
 
 namespace Ring
 
-open Classical
+open scoped Classical
 
 /-- Introduce a function `inverse` on a monoid with zero `M₀`, which sends `x` to `x⁻¹` if `x` is
 invertible and to `0` otherwise.  This definition is somewhat ad hoc, but one needs a fully (rather
@@ -328,7 +328,7 @@ end CommGroupWithZero
 
 section NoncomputableDefs
 
-open Classical
+open scoped Classical
 
 variable {M : Type*} [Nontrivial M]
 

diff --git a/Mathlib/Algebra/Homology/ComplexShape.lean b/Mathlib/Algebra/Homology/ComplexShape.lean
@@ -43,7 +43,7 @@ so `d : X i ⟶ X j` is nonzero only when `i = j + 1`.
 
 noncomputable section
 
-open Classical
+open scoped Classical
 
 /-- A `c : ComplexShape ι` describes the shape of a chain complex,
 with chain groups indexed by `ι`.

diff --git a/Mathlib/Algebra/Homology/Homology.lean b/Mathlib/Algebra/Homology/Homology.lean
@@ -40,7 +40,8 @@ variable {V : Type u} [Category.{v} V] [HasZeroMorphisms V]
 
 variable {c : ComplexShape ι} (C : HomologicalComplex V c)
 
-open Classical ZeroObject
+open scoped Classical
+open ZeroObject
 
 noncomputable section
 

diff --git a/Mathlib/Algebra/Homology/Homotopy.lean b/Mathlib/Algebra/Homology/Homotopy.lean
@@ -18,7 +18,7 @@ We define chain homotopies, and prove that homotopic chain maps induce the same
 
 universe v u
 
-open Classical
+open scoped Classical
 
 noncomputable section
 

diff --git a/Mathlib/Algebra/Homology/HomotopyCategory.lean b/Mathlib/Algebra/Homology/HomotopyCategory.lean
@@ -22,7 +22,7 @@ set_option autoImplicit true
 
 universe v u
 
-open Classical
+open scoped Classical
 
 noncomputable section
 

diff --git a/Mathlib/Algebra/Homology/ImageToKernel.lean b/Mathlib/Algebra/Homology/ImageToKernel.lean
@@ -35,7 +35,7 @@ variable {ι : Type*}
 
 variable {V : Type u} [Category.{v} V] [HasZeroMorphisms V]
 
-open Classical
+open scoped Classical
 
 noncomputable section
 

diff --git a/Mathlib/Algebra/MonoidAlgebra/Degree.lean b/Mathlib/Algebra/MonoidAlgebra/Degree.lean
@@ -22,7 +22,8 @@ variable {R R' A T B ι : Type*}
 
 namespace AddMonoidAlgebra
 
-open Classical BigOperators
+open scoped Classical
+open BigOperators
 
 /-!
 

diff --git a/Mathlib/Algebra/Order/CauSeq/Completion.lean b/Mathlib/Algebra/Order/CauSeq/Completion.lean
@@ -198,7 +198,7 @@ instance Cauchy.commRing : CommRing (Cauchy abv) :=
 
 end
 
-open Classical
+open scoped Classical
 
 section
 

diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@@ -480,7 +480,7 @@ section Field
 
 /-! ### Group operation polynomials over a field -/
 
-open Classical
+open scoped Classical
 
 /-- The slope of the line through two affine points $(x_1, y_1)$ and $(x_2, y_2)$ in `W`.
 If $x_1 \ne x_2$, then this line is the secant of `W` through $(x_1, y_1)$ and $(x_2, y_2)$,
@@ -691,7 +691,7 @@ lemma neg_some {x y : R} (h : W.nonsingular x y) : -some h = some (nonsingular_n
 instance : InvolutiveNeg W.Point :=
   ⟨by rintro (_ | _) <;> simp [zero_def]; ring1⟩
 
-open Classical
+open scoped Classical
 
 variable {F : Type u} [Field F] {W : Affine F}
 

diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
@@ -47,7 +47,7 @@ and Chris Hughes (on an earlier repository).
 
 noncomputable section
 
-open Classical
+open scoped Classical
 
 universe u v
 

diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Maximal.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Maximal.lean
@@ -28,7 +28,7 @@ natural inclusion into the prime spectrum to avoid API duplication for zero loci
 
 noncomputable section
 
-open Classical
+open scoped Classical
 
 universe u v
 

diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean
@@ -74,7 +74,8 @@ noncomputable section
 
 variable {𝕜 E F G : Type*}
 
-open Topology Classical BigOperators NNReal Filter ENNReal
+open scoped Classical
+open Topology BigOperators NNReal Filter ENNReal
 
 open Set Filter Asymptotics
 

diff --git a/Mathlib/Analysis/Analytic/CPolynomial.lean b/Mathlib/Analysis/Analytic/CPolynomial.lean
@@ -42,7 +42,8 @@ We develop the basic properties of these notions, notably:
 variable {𝕜 E F G : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
   [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G]
 
-open Topology Classical BigOperators NNReal Filter ENNReal
+open scoped Classical
+open Topology BigOperators NNReal Filter ENNReal
 
 open Set Filter Asymptotics
 

diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean
@@ -19,7 +19,8 @@ We show that the following are analytic:
 
 noncomputable section
 
-open Topology Classical BigOperators NNReal Filter ENNReal
+open scoped Classical
+open Topology BigOperators NNReal Filter ENNReal
 
 open Set Filter Asymptotics
 

diff --git a/Mathlib/Analysis/Asymptotics/Asymptotics.lean b/Mathlib/Analysis/Asymptotics/Asymptotics.lean
@@ -49,7 +49,8 @@ the Fréchet derivative.)
 
 open Filter Set
 
-open Topology BigOperators Classical Filter NNReal
+open scoped Classical
+open Topology BigOperators Filter NNReal
 
 namespace Asymptotics
 

diff --git a/Mathlib/Analysis/BoxIntegral/Box/Basic.lean b/Mathlib/Analysis/BoxIntegral/Box/Basic.lean
@@ -56,7 +56,8 @@ open Set Function Metric Filter
 
 noncomputable section
 
-open NNReal Classical Topology
+open scoped Classical
+open NNReal Topology
 
 namespace BoxIntegral
 

diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean b/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean
@@ -31,7 +31,8 @@ rectangular box, additive function
 
 noncomputable section
 
-open Classical BigOperators Function Set
+open scoped Classical
+open BigOperators Function Set
 
 namespace BoxIntegral
 

diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
@@ -41,7 +41,8 @@ rectangular box, partition
 
 open Set Finset Function
 
-open Classical NNReal BigOperators
+open scoped Classical
+open NNReal BigOperators
 
 noncomputable section
 

diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Filter.lean b/Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
@@ -168,7 +168,8 @@ integral, rectangular box, partition, filter
 
 open Set Function Filter Metric Finset Bool
 
-open Classical Topology Filter NNReal
+open scoped Classical
+open Topology Filter NNReal
 
 noncomputable section
 

diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean
@@ -40,7 +40,8 @@ rectangular box, partition, hyperplane
 
 noncomputable section
 
-open Classical BigOperators Filter
+open scoped Classical
+open BigOperators Filter
 
 open Function Set Filter
 

diff --git a/Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.lean b/Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.lean
@@ -33,7 +33,8 @@ namespace BoxIntegral
 
 open Set Metric
 
-open Classical Topology
+open scoped Classical
+open Topology
 
 noncomputable section
 

diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean b/Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
@@ -27,7 +27,8 @@ rectangular box, box partition
 
 noncomputable section
 
-open Classical ENNReal NNReal
+open scoped Classical
+open ENNReal NNReal
 
 open Set Function