[Merged by Bors] - chore: remove some uses of open Classical, part 2

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -34,8 +34,6 @@ noncomputable section
 
 open CategoryTheory ModuleCat.monoidalCategory
 
-open scoped Classical
-
 universe u
 
 section Ring

Mathlib/Algebra/Category/Grp/Adjunctions.lean

@@ -40,8 +40,6 @@ open CategoryTheory Limits
 
 namespace AddCommGrp
 
-open scoped Classical
-
 /-- The free functor `Type u ⥤ AddCommGroup` sending a type `X` to the
 free abelian group with generators `x : X`.
 -/

Mathlib/Algebra/Category/Grp/FilteredColimits.lean

@@ -26,11 +26,7 @@ universe v u
 
 noncomputable section
 
-open scoped Classical
-
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory CategoryTheory.Limits
 
 open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
 

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -24,8 +24,6 @@ namespace ModuleCat
 
 universe u
 
-open scoped Classical
-
 variable (R : Type u)
 
 section

Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

@@ -25,8 +25,6 @@ universe v u
 
 noncomputable section
 
-open scoped Classical
-
 open CategoryTheory CategoryTheory.Limits
 
 open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -26,11 +26,7 @@ universe v u
 
 noncomputable section
 
-open scoped Classical
-
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory CategoryTheory.Limits
 
 open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
 

Mathlib/Algebra/Category/Ring/Adjunctions.lean

@@ -22,8 +22,6 @@ open CategoryTheory
 
 namespace CommRingCat
 
-open scoped Classical
-
 /-- The free functor `Type u ⥤ CommRingCat` sending a type `X` to the multivariable (commutative)
 polynomials with variables `x : X`.
 -/

Mathlib/Algebra/Category/Ring/FilteredColimits.lean

@@ -26,11 +26,7 @@ universe v u
 
 noncomputable section
 
-open scoped Classical
-
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory CategoryTheory.Limits
 
 open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
 

Mathlib/Algebra/EuclideanDomain/Defs.lean

@@ -151,12 +151,11 @@ theorem div_zero (a : R) : a / 0 = 0 :=
 
 section
 
-open scoped Classical
-
 @[elab_as_elim]
 theorem GCD.induction {P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x)
-    (H1 : ∀ a b, a ≠ 0 → P (b % a) a → P a b) : P a b :=
-  if a0 : a = 0 then by
+    (H1 : ∀ a b, a ≠ 0 → P (b % a) a → P a b) : P a b := by
+  classical
+  exact if a0 : a = 0 then by
     -- Porting note: required for hygiene, the equation compiler introduces a dummy variable `x`
     -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unnecessarily.20tombstoned.20argument/near/314573315
     change P a b

Mathlib/Algebra/Field/IsField.lean

@@ -53,8 +53,7 @@ theorem not_isField_of_subsingleton (R : Type u) [Semiring R] [Subsingleton R] :
   let ⟨_, _, h⟩ := h.exists_pair_ne
   h (Subsingleton.elim _ _)
 
-open scoped Classical
-
+open Classical in
 /-- Transferring from `IsField` to `Semifield`. -/
 noncomputable def IsField.toSemifield {R : Type u} [Semiring R] (h : IsField R) : Semifield R where
   __ := ‹Semiring R›

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -1656,8 +1656,6 @@ theorem normalizer_eq_top : H.normalizer = ⊤ ↔ H.Normal :=
     ⟨fun h => ⟨fun a ha b => (h (mem_top b) a).mp ha⟩, fun h a _ha b =>
       ⟨fun hb => h.conj_mem b hb a, fun hb => by rwa [h.mem_comm_iff, inv_mul_cancel_left] at hb⟩⟩
 
-open scoped Classical
-
 @[to_additive]
 theorem le_normalizer_of_normal [hK : (H.subgroupOf K).Normal] (HK : H ≤ K) : K ≤ H.normalizer :=
   fun x hx y =>

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -35,8 +35,6 @@ and require `0⁻¹ = 0`.
 
 assert_not_exists DenselyOrdered
 
-open scoped Classical
-
 open Function
 
 variable {α M₀ G₀ M₀' G₀' F F' : Type*}
@@ -56,8 +54,9 @@ theorem right_ne_zero_of_mul : a * b ≠ 0 → b ≠ 0 :=
 theorem ne_zero_and_ne_zero_of_mul (h : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 :=
   ⟨left_ne_zero_of_mul h, right_ne_zero_of_mul h⟩
 
-theorem mul_eq_zero_of_ne_zero_imp_eq_zero {a b : M₀} (h : a ≠ 0 → b = 0) : a * b = 0 :=
-  if ha : a = 0 then by rw [ha, zero_mul] else by rw [h ha, mul_zero]
+theorem mul_eq_zero_of_ne_zero_imp_eq_zero {a b : M₀} (h : a ≠ 0 → b = 0) : a * b = 0 := by
+  have : Decidable (a = 0) := Classical.propDecidable (a = 0)
+  exact if ha : a = 0 then by rw [ha, zero_mul] else by rw [h ha, mul_zero]
 
 /-- To match `one_mul_eq_id`. -/
 theorem zero_mul_eq_const : ((0 : M₀) * ·) = Function.const _ 0 :=

Mathlib/Algebra/GroupWithZero/Commute.lean

@@ -19,8 +19,6 @@ variable [MonoidWithZero M₀]
 
 namespace Ring
 
-open scoped Classical
-
 theorem mul_inverse_rev' {a b : M₀} (h : Commute a b) :
     inverse (a * b) = inverse b * inverse a := by
   by_cases hab : IsUnit (a * b)

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

@@ -72,8 +72,7 @@ theorem not_isUnit_zero [Nontrivial M₀] : ¬IsUnit (0 : M₀) :=
 
 namespace Ring
 
-open scoped Classical
-
+open Classical in
 /-- 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
 than partially) defined inverse function for some purposes, including for calculus.
@@ -454,10 +453,9 @@ end CommGroupWithZero
 
 section NoncomputableDefs
 
-open scoped Classical
-
 variable {M : Type*} [Nontrivial M]
 
+open Classical in
 /-- Constructs a `GroupWithZero` structure on a `MonoidWithZero`
   consisting only of units and 0. -/
 noncomputable def groupWithZeroOfIsUnitOrEqZero [hM : MonoidWithZero M]

Mathlib/Algebra/Homology/ComplexShape.lean

@@ -41,8 +41,6 @@ so `d : X i ⟶ X j` is nonzero only when `i = j + 1`.
 
 noncomputable section
 
-open scoped Classical
-
 /-- A `c : ComplexShape ι` describes the shape of a chain complex,
 with chain groups indexed by `ι`.
 Typically `ι` will be `ℕ`, `ℤ`, or `Fin n`.
@@ -126,12 +124,14 @@ instance subsingleton_prev (c : ComplexShape ι) (j : ι) : Subsingleton { i //
   congr
   exact c.prev_eq rik rjk
 
+open Classical in
 /-- An arbitrary choice of index `j` such that `Rel i j`, if such exists.
 Returns `i` otherwise.
 -/
 def next (c : ComplexShape ι) (i : ι) : ι :=
   if h : ∃ j, c.Rel i j then h.choose else i
 
+open Classical in
 /-- An arbitrary choice of index `i` such that `Rel i j`, if such exists.
 Returns `j` otherwise.
 -/

Mathlib/Algebra/Homology/DifferentialObject.lean

@@ -18,8 +18,6 @@ it's here to check that definitions match up as expected.
 
 open CategoryTheory CategoryTheory.Limits
 
-open scoped Classical
-
 noncomputable section
 
 /-!
@@ -70,6 +68,7 @@ variable (V : Type*) [Category V] [HasZeroMorphisms V]
 theorem d_eqToHom (X : HomologicalComplex V (ComplexShape.up' b)) {x y z : β} (h : y = z) :
     X.d x y ≫ eqToHom (congr_arg X.X h) = X.d x z := by cases h; simp
 
+open Classical in
 set_option maxHeartbeats 400000 in
 /-- The functor from differential graded objects to homological complexes.
 -/

Mathlib/Algebra/Homology/Homotopy.lean

@@ -16,8 +16,6 @@ We define chain homotopies, and prove that homotopic chain maps induce the same
 
 universe v u
 
-open scoped Classical
-
 noncomputable section
 
 open CategoryTheory Category Limits HomologicalComplex
@@ -250,6 +248,7 @@ def nullHomotopicMap (hom : ∀ i j, C.X i ⟶ D.X j) : C ⟶ D where
     rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
       add_zero, zero_add, assoc]
 
+open Classical in
 /-- Variant of `nullHomotopicMap` where the input consists only of the
 relevant maps `C_i ⟶ D_j` such that `c.Rel j i`. -/
 def nullHomotopicMap' (h : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) : C ⟶ D :=
@@ -329,6 +328,7 @@ def nullHomotopy (hom : ∀ i j, C.X i ⟶ D.X j) (zero : ∀ i j, ¬c.Rel j i 
       rw [HomologicalComplex.zero_f_apply, add_zero]
       rfl }
 
+open Classical in
 /-- Homotopy to zero for maps constructed with `nullHomotopicMap'` -/
 @[simps!]
 def nullHomotopy' (h : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) : Homotopy (nullHomotopicMap' h) 0 := by

Mathlib/Algebra/Homology/HomotopyCategory.lean

@@ -18,8 +18,6 @@ with chain maps identified when they are homotopic.
 
 universe v u
 
-open scoped Classical
-
 noncomputable section
 
 open CategoryTheory CategoryTheory.Limits HomologicalComplex
@@ -175,6 +173,7 @@ section
 
 variable [CategoryWithHomology V]
 
+open Classical in
 /-- The `i`-th homology, as a functor from the homotopy category. -/
 noncomputable def homologyFunctor (i : ι) : HomotopyCategory V c ⥤ V :=
   CategoryTheory.Quotient.lift _ (HomologicalComplex.homologyFunctor V c i) (by

Mathlib/Algebra/Homology/ImageToKernel.lean

@@ -23,8 +23,6 @@ open CategoryTheory CategoryTheory.Limits
 variable {ι : Type*}
 variable {V : Type u} [Category.{v} V] [HasZeroMorphisms V]
 
-open scoped Classical
-
 noncomputable section
 
 section

Mathlib/Algebra/Module/DedekindDomain.lean

@@ -28,12 +28,10 @@ variable [IsDedekindDomain R]
 
 open UniqueFactorizationMonoid
 
-open scoped Classical
-
 /-- Over a Dedekind domain, an `I`-torsion module is the internal direct sum of its `p i ^ e i`-
 torsion submodules, where `I = ∏ i, p i ^ e i` is its unique decomposition in prime ideals. -/
-theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal {I : Ideal R} (hI : I ≠ ⊥)
-    (hM : Module.IsTorsionBySet R M I) :
+theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal [DecidableEq (Ideal R)]
+    {I : Ideal R} (hI : I ≠ ⊥) (hM : Module.IsTorsionBySet R M I) :
     DirectSum.IsInternal fun p : (factors I).toFinset =>
       torsionBySet R M (p ^ (factors I).count ↑p : Ideal R) := by
   let P := factors I
@@ -59,7 +57,8 @@ theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal {I : Ideal R} (hI
 /-- A finitely generated torsion module over a Dedekind domain is an internal direct sum of its
 `p i ^ e i`-torsion submodules where `p i` are factors of `(⊤ : Submodule R M).annihilator` and
 `e i` are their multiplicities. -/
-theorem isInternal_prime_power_torsion [Module.Finite R M] (hM : Module.IsTorsion R M) :
+theorem isInternal_prime_power_torsion [DecidableEq (Ideal R)] [Module.Finite R M]
+    (hM : Module.IsTorsion R M) :
     DirectSum.IsInternal fun p : (factors (⊤ : Submodule R M).annihilator).toFinset =>
       torsionBySet R M (p ^ (factors (⊤ : Submodule R M).annihilator).count ↑p : Ideal R) := by
   have hM' := Module.isTorsionBySet_annihilator_top R M
@@ -72,8 +71,9 @@ theorem isInternal_prime_power_torsion [Module.Finite R M] (hM : Module.IsTorsio
 `p i ^ e i`-torsion submodules for some prime ideals `p i` and numbers `e i`. -/
 theorem exists_isInternal_prime_power_torsion [Module.Finite R M] (hM : Module.IsTorsion R M) :
     ∃ (P : Finset <| Ideal R) (_ : DecidableEq P) (_ : ∀ p ∈ P, Prime p) (e : P → ℕ),
-      DirectSum.IsInternal fun p : P => torsionBySet R M (p ^ e p : Ideal R) :=
-  ⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _,
+      DirectSum.IsInternal fun p : P => torsionBySet R M (p ^ e p : Ideal R) := by
+  classical
+  exact ⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _,
     isInternal_prime_power_torsion hM⟩
 
 end Submodule

Mathlib/Algebra/Module/PID.lean

@@ -53,8 +53,6 @@ assert_not_exists TopologicalSpace
 
 universe u v
 
-open scoped Classical
-
 variable {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
 variable {M : Type v} [AddCommGroup M] [Module R M]
 variable {N : Type max u v} [AddCommGroup N] [Module R N]
@@ -73,7 +71,7 @@ theorem Submodule.isSemisimple_torsionBy_of_irreducible {a : R} (h : Irreducible
 
 /-- A finitely generated torsion module over a PID is an internal direct sum of its
 `p i ^ e i`-torsion submodules for some primes `p i` and numbers `e i`. -/
-theorem Submodule.isInternal_prime_power_torsion_of_pid [Module.Finite R M]
+theorem Submodule.isInternal_prime_power_torsion_of_pid [DecidableEq (Ideal R)] [Module.Finite R M]
     (hM : Module.IsTorsion R M) :
     DirectSum.IsInternal fun p : (factors (⊤ : Submodule R M).annihilator).toFinset =>
       torsionBy R M
@@ -90,6 +88,7 @@ theorem Submodule.exists_isInternal_prime_power_torsion_of_pid [Module.Finite R
     (hM : Module.IsTorsion R M) :
     ∃ (ι : Type u) (_ : Fintype ι) (_ : DecidableEq ι) (p : ι → R) (_ : ∀ i, Irreducible <| p i)
         (e : ι → ℕ), DirectSum.IsInternal fun i => torsionBy R M <| p i ^ e i := by
+  classical
   refine ⟨_, ?_, _, _, ?_, _, Submodule.isInternal_prime_power_torsion_of_pid hM⟩
   · exact Finset.fintypeCoeSort _
   · rintro ⟨p, hp⟩
@@ -108,6 +107,7 @@ open Ideal Submodule.IsPrincipal
 
 theorem _root_.Ideal.torsionOf_eq_span_pow_pOrder (x : M) :
     torsionOf R M x = span {p ^ pOrder hM x} := by
+  classical
   dsimp only [pOrder]
   rw [← (torsionOf R M x).span_singleton_generator, Ideal.span_singleton_eq_span_singleton, ←
     Associates.mk_eq_mk_iff_associated, Associates.mk_pow]