Chore: Replace open scoped Classical with (open scoped Classical in) or (classical)

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,21 +83,25 @@ 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
 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,13 +121,15 @@ 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
   dsimp only [A, agreedContestants]; ext c; constructor <;> intro h
   · 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 _

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

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).
 
@@ -93,9 +91,11 @@ universe u
 variable {ι : Type u}
 
 /-- 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
+def indicatorSeries (α : Type*) [Semiring α] (s : Set ℕ) : PowerSeries α := by
+  classical
+  exact 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) :

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
 

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
 
@@ -94,12 +93,17 @@ section
 
 attribute [local simp] Hom.id Hom.comp
 
+
 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 +114,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 +161,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,
@@ -244,11 +251,13 @@ def mapMat_ (F : C ⥤ D) [Functor.Additive F] : Mat_ C ⥤ Mat_ D where
   obj M := ⟨M.ι, fun i => F.obj (M.X i)⟩
   map f i j := F.map (f i j)
 
+
 /-- The identity functor induces the identity functor on matrix categories.
 -/
 @[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 +268,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 +304,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 +376,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 +504,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 +523,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