Skip to content

Commit 425a516

Browse files
sgouezelgrunweg
sgouezel
authored and
grunweg
committed
chore: remove some uses of open Classical, part 2 (#15413)
See #15371.
1 parent 3f895b3 commit 425a516

File tree

82 files changed

+173
-224
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

82 files changed

+173
-224
lines changed

‎Mathlib/Algebra/Category/AlgebraCat/Basic.lean

+1-3
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,7 @@ associating to a type the free `R`-algebra on that type is left adjoint to the f
1717
-/
1818

1919

20-
open CategoryTheory
21-
22-
open CategoryTheory.Limits
20+
open CategoryTheory Limits
2321

2422
universe v u
2523

‎Mathlib/Algebra/Category/AlgebraCat/Limits.lean

+1-3
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,7 @@ the underlying types are just the limits in the category of types.
1616
-/
1717

1818

19-
open CategoryTheory
20-
21-
open CategoryTheory.Limits
19+
open CategoryTheory Limits
2220

2321
universe v w u t
2422

‎Mathlib/Algebra/Category/FGModuleCat/Basic.lean

-2
Original file line numberDiff line numberDiff line change
@@ -34,8 +34,6 @@ noncomputable section
3434

3535
open CategoryTheory ModuleCat.monoidalCategory
3636

37-
open scoped Classical
38-
3937
universe u
4038

4139
section Ring

‎Mathlib/Algebra/Category/FGModuleCat/Limits.lean

+1-3
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,7 @@ noncomputable section
2828

2929
universe v u
3030

31-
open CategoryTheory
32-
33-
open CategoryTheory.Limits
31+
open CategoryTheory Limits
3432

3533
namespace FGModuleCat
3634

‎Mathlib/Algebra/Category/Grp/Adjunctions.lean

-2
Original file line numberDiff line numberDiff line change
@@ -40,8 +40,6 @@ open CategoryTheory Limits
4040

4141
namespace AddCommGrp
4242

43-
open scoped Classical
44-
4543
/-- The free functor `Type u ⥤ AddCommGroup` sending a type `X` to the
4644
free abelian group with generators `x : X`.
4745
-/

‎Mathlib/Algebra/Category/Grp/FilteredColimits.lean

+2-6
Original file line numberDiff line numberDiff line change
@@ -26,13 +26,9 @@ universe v u
2626

2727
noncomputable section
2828

29-
open scoped Classical
29+
open CategoryTheory Limits
3030

31-
open CategoryTheory
32-
33-
open CategoryTheory.Limits
34-
35-
open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
31+
open IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
3632

3733
namespace Grp.FilteredColimits
3834

‎Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

-2
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,6 @@ namespace ModuleCat
2424

2525
universe u
2626

27-
open scoped Classical
28-
2927
variable (R : Type u)
3028

3129
section

‎Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

-2
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,6 @@ universe v u
2525

2626
noncomputable section
2727

28-
open scoped Classical
29-
3028
open CategoryTheory CategoryTheory.Limits
3129

3230
open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.

‎Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

+2-6
Original file line numberDiff line numberDiff line change
@@ -26,13 +26,9 @@ universe v u
2626

2727
noncomputable section
2828

29-
open scoped Classical
29+
open CategoryTheory Limits
3030

31-
open CategoryTheory
32-
33-
open CategoryTheory.Limits
34-
35-
open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
31+
open IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
3632

3733
namespace MonCat.FilteredColimits
3834

‎Mathlib/Algebra/Category/Ring/Adjunctions.lean

-2
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,6 @@ open CategoryTheory
2222

2323
namespace CommRingCat
2424

25-
open scoped Classical
26-
2725
/-- The free functor `Type u ⥤ CommRingCat` sending a type `X` to the multivariable (commutative)
2826
polynomials with variables `x : X`.
2927
-/

‎Mathlib/Algebra/Category/Ring/Colimits.lean

+1-3
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,7 @@ by a tactic that analyses the shape of `CommRing` and `RingHom`.
1818

1919
universe u v
2020

21-
open CategoryTheory
22-
23-
open CategoryTheory.Limits
21+
open CategoryTheory Limits
2422

2523

2624
namespace RingCat.Colimits

‎Mathlib/Algebra/Category/Ring/Constructions.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ suppress_compilation
2626

2727
universe u u'
2828

29-
open CategoryTheory CategoryTheory.Limits TensorProduct
29+
open CategoryTheory Limits TensorProduct
3030

3131
namespace CommRingCat
3232

‎Mathlib/Algebra/Category/Ring/FilteredColimits.lean

+2-6
Original file line numberDiff line numberDiff line change
@@ -26,13 +26,9 @@ universe v u
2626

2727
noncomputable section
2828

29-
open scoped Classical
29+
open CategoryTheory Limits
3030

31-
open CategoryTheory
32-
33-
open CategoryTheory.Limits
34-
35-
open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
31+
open IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
3632

3733
open AddMonCat.FilteredColimits (colimit_zero_eq colimit_add_mk_eq)
3834

‎Mathlib/Algebra/EuclideanDomain/Defs.lean

+3-4
Original file line numberDiff line numberDiff line change
@@ -151,12 +151,11 @@ theorem div_zero (a : R) : a / 0 = 0 :=
151151

152152
section
153153

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

‎Mathlib/Algebra/Field/IsField.lean

+1-2
Original file line numberDiff line numberDiff line change
@@ -53,8 +53,7 @@ theorem not_isField_of_subsingleton (R : Type u) [Semiring R] [Subsingleton R] :
5353
let ⟨_, _, h⟩ := h.exists_pair_ne
5454
h (Subsingleton.elim _ _)
5555

56-
open scoped Classical
57-
56+
open Classical in
5857
/-- Transferring from `IsField` to `Semifield`. -/
5958
noncomputable def IsField.toSemifield {R : Type u} [Semiring R] (h : IsField R) : Semifield R where
6059
__ := ‹Semiring R›

‎Mathlib/Algebra/Group/Subgroup/Basic.lean

-2
Original file line numberDiff line numberDiff line change
@@ -1656,8 +1656,6 @@ theorem normalizer_eq_top : H.normalizer = ⊤ ↔ H.Normal :=
16561656
⟨fun h => ⟨fun a ha b => (h (mem_top b) a).mp ha⟩, fun h a _ha b =>
16571657
⟨fun hb => h.conj_mem b hb a, fun hb => by rwa [h.mem_comm_iff, inv_mul_cancel_left] at hb⟩⟩
16581658

1659-
open scoped Classical
1660-
16611659
@[to_additive]
16621660
theorem le_normalizer_of_normal [hK : (H.subgroupOf K).Normal] (HK : H ≤ K) : K ≤ H.normalizer :=
16631661
fun x hx y =>

‎Mathlib/Algebra/GroupWithZero/Basic.lean

+3-4
Original file line numberDiff line numberDiff line change
@@ -35,8 +35,6 @@ and require `0⁻¹ = 0`.
3535

3636
assert_not_exists DenselyOrdered
3737

38-
open scoped Classical
39-
4038
open Function
4139

4240
variable {α M₀ G₀ M₀' G₀' F F' : Type*}
@@ -56,8 +54,9 @@ theorem right_ne_zero_of_mul : a * b ≠ 0 → b ≠ 0 :=
5654
theorem ne_zero_and_ne_zero_of_mul (h : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 :=
5755
⟨left_ne_zero_of_mul h, right_ne_zero_of_mul h⟩
5856

59-
theorem mul_eq_zero_of_ne_zero_imp_eq_zero {a b : M₀} (h : a ≠ 0 → b = 0) : a * b = 0 :=
60-
if ha : a = 0 then by rw [ha, zero_mul] else by rw [h ha, mul_zero]
57+
theorem mul_eq_zero_of_ne_zero_imp_eq_zero {a b : M₀} (h : a ≠ 0 → b = 0) : a * b = 0 := by
58+
have : Decidable (a = 0) := Classical.propDecidable (a = 0)
59+
exact if ha : a = 0 then by rw [ha, zero_mul] else by rw [h ha, mul_zero]
6160

6261
/-- To match `one_mul_eq_id`. -/
6362
theorem zero_mul_eq_const : ((0 : M₀) * ·) = Function.const _ 0 :=

‎Mathlib/Algebra/GroupWithZero/Commute.lean

-2
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,6 @@ variable [MonoidWithZero M₀]
1919

2020
namespace Ring
2121

22-
open scoped Classical
23-
2422
theorem mul_inverse_rev' {a b : M₀} (h : Commute a b) :
2523
inverse (a * b) = inverse b * inverse a := by
2624
by_cases hab : IsUnit (a * b)

‎Mathlib/Algebra/GroupWithZero/Units/Basic.lean

+2-4
Original file line numberDiff line numberDiff line change
@@ -72,8 +72,7 @@ theorem not_isUnit_zero [Nontrivial M₀] : ¬IsUnit (0 : M₀) :=
7272

7373
namespace Ring
7474

75-
open scoped Classical
76-
75+
open Classical in
7776
/-- Introduce a function `inverse` on a monoid with zero `M₀`, which sends `x` to `x⁻¹` if `x` is
7877
invertible and to `0` otherwise. This definition is somewhat ad hoc, but one needs a fully (rather
7978
than partially) defined inverse function for some purposes, including for calculus.
@@ -454,10 +453,9 @@ end CommGroupWithZero
454453

455454
section NoncomputableDefs
456455

457-
open scoped Classical
458-
459456
variable {M : Type*} [Nontrivial M]
460457

458+
open Classical in
461459
/-- Constructs a `GroupWithZero` structure on a `MonoidWithZero`
462460
consisting only of units and 0. -/
463461
noncomputable def groupWithZeroOfIsUnitOrEqZero [hM : MonoidWithZero M]

‎Mathlib/Algebra/Homology/ComplexShape.lean

+2-2
Original file line numberDiff line numberDiff line change
@@ -41,8 +41,6 @@ so `d : X i ⟶ X j` is nonzero only when `i = j + 1`.
4141

4242
noncomputable section
4343

44-
open scoped Classical
45-
4644
/-- A `c : ComplexShape ι` describes the shape of a chain complex,
4745
with chain groups indexed by `ι`.
4846
Typically `ι` will be `ℕ`, `ℤ`, or `Fin n`.
@@ -126,12 +124,14 @@ instance subsingleton_prev (c : ComplexShape ι) (j : ι) : Subsingleton { i //
126124
congr
127125
exact c.prev_eq rik rjk
128126

127+
open Classical in
129128
/-- An arbitrary choice of index `j` such that `Rel i j`, if such exists.
130129
Returns `i` otherwise.
131130
-/
132131
def next (c : ComplexShape ι) (i : ι) : ι :=
133132
if h : ∃ j, c.Rel i j then h.choose else i
134133

134+
open Classical in
135135
/-- An arbitrary choice of index `i` such that `Rel i j`, if such exists.
136136
Returns `j` otherwise.
137137
-/

‎Mathlib/Algebra/Homology/DifferentialObject.lean

+1-2
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,6 @@ it's here to check that definitions match up as expected.
1818

1919
open CategoryTheory CategoryTheory.Limits
2020

21-
open scoped Classical
22-
2321
noncomputable section
2422

2523
/-!
@@ -70,6 +68,7 @@ variable (V : Type*) [Category V] [HasZeroMorphisms V]
7068
theorem d_eqToHom (X : HomologicalComplex V (ComplexShape.up' b)) {x y z : β} (h : y = z) :
7169
X.d x y ≫ eqToHom (congr_arg X.X h) = X.d x z := by cases h; simp
7270

71+
open Classical in
7372
set_option maxHeartbeats 400000 in
7473
/-- The functor from differential graded objects to homological complexes.
7574
-/

‎Mathlib/Algebra/Homology/Homotopy.lean

+2-2
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,6 @@ We define chain homotopies, and prove that homotopic chain maps induce the same
1616

1717
universe v u
1818

19-
open scoped Classical
20-
2119
noncomputable section
2220

2321
open CategoryTheory Category Limits HomologicalComplex
@@ -250,6 +248,7 @@ def nullHomotopicMap (hom : ∀ i j, C.X i ⟶ D.X j) : C ⟶ D where
250248
rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
251249
add_zero, zero_add, assoc]
252250

251+
open Classical in
253252
/-- Variant of `nullHomotopicMap` where the input consists only of the
254253
relevant maps `C_i ⟶ D_j` such that `c.Rel j i`. -/
255254
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
329328
rw [HomologicalComplex.zero_f_apply, add_zero]
330329
rfl }
331330

331+
open Classical in
332332
/-- Homotopy to zero for maps constructed with `nullHomotopicMap'` -/
333333
@[simps!]
334334
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

+1-2
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,6 @@ with chain maps identified when they are homotopic.
1818

1919
universe v u
2020

21-
open scoped Classical
22-
2321
noncomputable section
2422

2523
open CategoryTheory CategoryTheory.Limits HomologicalComplex
@@ -175,6 +173,7 @@ section
175173

176174
variable [CategoryWithHomology V]
177175

176+
open Classical in
178177
/-- The `i`-th homology, as a functor from the homotopy category. -/
179178
noncomputable def homologyFunctor (i : ι) : HomotopyCategory V c ⥤ V :=
180179
CategoryTheory.Quotient.lift _ (HomologicalComplex.homologyFunctor V c i) (by

‎Mathlib/Algebra/Homology/ImageToKernel.lean

-2
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,6 @@ open CategoryTheory CategoryTheory.Limits
2323
variable {ι : Type*}
2424
variable {V : Type u} [Category.{v} V] [HasZeroMorphisms V]
2525

26-
open scoped Classical
27-
2826
noncomputable section
2927

3028
section

‎Mathlib/Algebra/Module/DedekindDomain.lean

+7-7
Original file line numberDiff line numberDiff line change
@@ -28,12 +28,10 @@ variable [IsDedekindDomain R]
2828

2929
open UniqueFactorizationMonoid
3030

31-
open scoped Classical
32-
3331
/-- Over a Dedekind domain, an `I`-torsion module is the internal direct sum of its `p i ^ e i`-
3432
torsion submodules, where `I = ∏ i, p i ^ e i` is its unique decomposition in prime ideals. -/
35-
theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal {I : Ideal R} (hI : I ≠ ⊥)
36-
(hM : Module.IsTorsionBySet R M I) :
33+
theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal [DecidableEq (Ideal R)]
34+
{I : Ideal R} (hI : I ≠ ⊥) (hM : Module.IsTorsionBySet R M I) :
3735
DirectSum.IsInternal fun p : (factors I).toFinset =>
3836
torsionBySet R M (p ^ (factors I).count ↑p : Ideal R) := by
3937
let P := factors I
@@ -59,7 +57,8 @@ theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal {I : Ideal R} (hI
5957
/-- A finitely generated torsion module over a Dedekind domain is an internal direct sum of its
6058
`p i ^ e i`-torsion submodules where `p i` are factors of `(⊤ : Submodule R M).annihilator` and
6159
`e i` are their multiplicities. -/
62-
theorem isInternal_prime_power_torsion [Module.Finite R M] (hM : Module.IsTorsion R M) :
60+
theorem isInternal_prime_power_torsion [DecidableEq (Ideal R)] [Module.Finite R M]
61+
(hM : Module.IsTorsion R M) :
6362
DirectSum.IsInternal fun p : (factors (⊤ : Submodule R M).annihilator).toFinset =>
6463
torsionBySet R M (p ^ (factors (⊤ : Submodule R M).annihilator).count ↑p : Ideal R) := by
6564
have hM' := Module.isTorsionBySet_annihilator_top R M
@@ -72,8 +71,9 @@ theorem isInternal_prime_power_torsion [Module.Finite R M] (hM : Module.IsTorsio
7271
`p i ^ e i`-torsion submodules for some prime ideals `p i` and numbers `e i`. -/
7372
theorem exists_isInternal_prime_power_torsion [Module.Finite R M] (hM : Module.IsTorsion R M) :
7473
∃ (P : Finset <| Ideal R) (_ : DecidableEq P) (_ : ∀ p ∈ P, Prime p) (e : P → ℕ),
75-
DirectSum.IsInternal fun p : P => torsionBySet R M (p ^ e p : Ideal R) :=
76-
⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _,
74+
DirectSum.IsInternal fun p : P => torsionBySet R M (p ^ e p : Ideal R) := by
75+
classical
76+
exact ⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _,
7777
isInternal_prime_power_torsion hM⟩
7878

7979
end Submodule

‎Mathlib/Algebra/Module/PID.lean

+3-3
Original file line numberDiff line numberDiff line change
@@ -53,8 +53,6 @@ assert_not_exists TopologicalSpace
5353

5454
universe u v
5555

56-
open scoped Classical
57-
5856
variable {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
5957
variable {M : Type v} [AddCommGroup M] [Module R M]
6058
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
7371

7472
/-- A finitely generated torsion module over a PID is an internal direct sum of its
7573
`p i ^ e i`-torsion submodules for some primes `p i` and numbers `e i`. -/
76-
theorem Submodule.isInternal_prime_power_torsion_of_pid [Module.Finite R M]
74+
theorem Submodule.isInternal_prime_power_torsion_of_pid [DecidableEq (Ideal R)] [Module.Finite R M]
7775
(hM : Module.IsTorsion R M) :
7876
DirectSum.IsInternal fun p : (factors (⊤ : Submodule R M).annihilator).toFinset =>
7977
torsionBy R M
@@ -90,6 +88,7 @@ theorem Submodule.exists_isInternal_prime_power_torsion_of_pid [Module.Finite R
9088
(hM : Module.IsTorsion R M) :
9189
∃ (ι : Type u) (_ : Fintype ι) (_ : DecidableEq ι) (p : ι → R) (_ : ∀ i, Irreducible <| p i)
9290
(e : ι → ℕ), DirectSum.IsInternal fun i => torsionBy R M <| p i ^ e i := by
91+
classical
9392
refine ⟨_, ?_, _, _, ?_, _, Submodule.isInternal_prime_power_torsion_of_pid hM⟩
9493
· exact Finset.fintypeCoeSort _
9594
· rintro ⟨p, hp⟩
@@ -108,6 +107,7 @@ open Ideal Submodule.IsPrincipal
108107

109108
theorem _root_.Ideal.torsionOf_eq_span_pow_pOrder (x : M) :
110109
torsionOf R M x = span {p ^ pOrder hM x} := by
110+
classical
111111
dsimp only [pOrder]
112112
rw [← (torsionOf R M x).span_singleton_generator, Ideal.span_singleton_eq_span_singleton, ←
113113
Associates.mk_eq_mk_iff_associated, Associates.mk_pow]

0 commit comments

Comments
 (0)