From 19d45367b4348e95ddfdadfc98ab1656a068486d Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sat, 3 Aug 2024 10:01:55 +0000 Subject: [PATCH] chore: remove some uses of `open Classical`, part 2 (#15413) See #15371. --- .../Algebra/Category/AlgebraCat/Basic.lean | 4 +-- .../Algebra/Category/AlgebraCat/Limits.lean | 4 +-- .../Algebra/Category/FGModuleCat/Basic.lean | 2 -- .../Algebra/Category/FGModuleCat/Limits.lean | 4 +-- Mathlib/Algebra/Category/Grp/Adjunctions.lean | 2 -- .../Category/Grp/FilteredColimits.lean | 8 ++--- .../Category/ModuleCat/Adjunctions.lean | 2 -- .../Category/ModuleCat/FilteredColimits.lean | 2 -- .../Category/MonCat/FilteredColimits.lean | 8 ++--- .../Algebra/Category/Ring/Adjunctions.lean | 2 -- Mathlib/Algebra/Category/Ring/Colimits.lean | 4 +-- .../Algebra/Category/Ring/Constructions.lean | 2 +- .../Category/Ring/FilteredColimits.lean | 8 ++--- Mathlib/Algebra/EuclideanDomain/Defs.lean | 7 ++-- Mathlib/Algebra/Field/IsField.lean | 3 +- Mathlib/Algebra/Group/Subgroup/Basic.lean | 2 -- Mathlib/Algebra/GroupWithZero/Basic.lean | 7 ++-- Mathlib/Algebra/GroupWithZero/Commute.lean | 2 -- .../Algebra/GroupWithZero/Units/Basic.lean | 6 ++-- Mathlib/Algebra/Homology/ComplexShape.lean | 4 +-- .../Algebra/Homology/DifferentialObject.lean | 3 +- Mathlib/Algebra/Homology/Homotopy.lean | 4 +-- .../Algebra/Homology/HomotopyCategory.lean | 3 +- Mathlib/Algebra/Homology/ImageToKernel.lean | 2 -- Mathlib/Algebra/Module/DedekindDomain.lean | 14 ++++---- Mathlib/Algebra/Module/PID.lean | 6 ++-- Mathlib/Algebra/MonoidAlgebra/Degree.lean | 21 ++++++----- Mathlib/Algebra/MvPolynomial/Rename.lean | 3 +- Mathlib/Algebra/Order/CauSeq/Completion.lean | 3 +- Mathlib/Algebra/Order/CompleteField.lean | 2 +- .../Algebra/Order/GroupWithZero/Synonym.lean | 2 -- .../EllipticCurve/Affine.lean | 6 ++-- .../EllipticCurve/Jacobian.lean | 6 ++-- Mathlib/AlgebraicGeometry/Limits.lean | 1 - .../PrimeSpectrum/Basic.lean | 2 -- .../PrimeSpectrum/Maximal.lean | 2 -- Mathlib/AlgebraicGeometry/StructureSheaf.lean | 2 -- .../AlgebraicTopology/TopologicalSimplex.lean | 6 +++- Mathlib/Analysis/Analytic/Basic.lean | 5 +-- Mathlib/Analysis/ConstantSpeed.lean | 2 +- Mathlib/Analysis/Hofer.lean | 6 +--- Mathlib/Analysis/MeanInequalities.lean | 2 -- Mathlib/Analysis/MeanInequalitiesPow.lean | 5 +-- Mathlib/Analysis/Seminorm.lean | 3 +- .../RotationNumber/TranslationNumber.lean | 1 - Mathlib/Dynamics/Ergodic/Conservative.lean | 6 +--- Mathlib/FieldTheory/AbelRuffini.lean | 2 -- Mathlib/FieldTheory/Finiteness.lean | 3 -- Mathlib/FieldTheory/Fixed.lean | 11 +++--- Mathlib/FieldTheory/IsPerfectClosure.lean | 2 -- Mathlib/FieldTheory/IsSepClosed.lean | 2 -- Mathlib/FieldTheory/KrullTopology.lean | 2 +- Mathlib/FieldTheory/Laurent.lean | 2 +- Mathlib/FieldTheory/MvPolynomial.lean | 4 --- Mathlib/FieldTheory/Normal.lean | 3 +- Mathlib/FieldTheory/PrimitiveElement.lean | 4 +-- Mathlib/FieldTheory/Separable.lean | 36 +++++++++++++------ Mathlib/FieldTheory/SeparableClosure.lean | 2 +- Mathlib/MeasureTheory/Group/Prod.lean | 2 +- Mathlib/MeasureTheory/Integral/Bochner.lean | 9 ++--- .../MeasureTheory/Integral/IntegrableOn.lean | 3 +- Mathlib/MeasureTheory/Integral/Lebesgue.lean | 9 ++--- Mathlib/MeasureTheory/Integral/Marginal.lean | 2 +- .../Integral/MeanInequalities.lean | 2 +- Mathlib/MeasureTheory/Integral/SetToL1.lean | 12 +++++-- .../MeasurableSpace/CountablyGenerated.lean | 3 +- .../MeasureTheory/MeasurableSpace/Defs.lean | 9 ++--- .../MeasurableSpace/Embedding.lean | 3 +- .../MeasureTheory/Measure/AEMeasurable.lean | 5 ++- Mathlib/MeasureTheory/Measure/Complex.lean | 2 +- Mathlib/MeasureTheory/Measure/Dirac.lean | 10 +++--- Mathlib/MeasureTheory/Measure/GiryMonad.lean | 6 +--- Mathlib/MeasureTheory/Measure/Haar/Basic.lean | 8 +++-- .../MeasureTheory/Measure/Lebesgue/Basic.lean | 1 - Mathlib/MeasureTheory/Measure/Stieltjes.lean | 1 - .../MeasureTheory/Measure/VectorMeasure.lean | 6 +++- .../Measure/WithDensityVectorMeasure.lean | 3 +- .../OuterMeasure/Caratheodory.lean | 2 +- .../MeasureTheory/OuterMeasure/Induced.lean | 3 +- .../OuterMeasure/OfFunction.lean | 2 +- .../OuterMeasure/Operations.lean | 2 +- Mathlib/RingTheory/DedekindDomain/Ideal.lean | 18 +++++----- 82 files changed, 173 insertions(+), 224 deletions(-) diff --git a/Mathlib/Algebra/Category/AlgebraCat/Basic.lean b/Mathlib/Algebra/Category/AlgebraCat/Basic.lean index 70bc0f37a8c20..6d3c2563e4879 100644 --- a/Mathlib/Algebra/Category/AlgebraCat/Basic.lean +++ b/Mathlib/Algebra/Category/AlgebraCat/Basic.lean @@ -17,9 +17,7 @@ associating to a type the free `R`-algebra on that type is left adjoint to the f -/ -open CategoryTheory - -open CategoryTheory.Limits +open CategoryTheory Limits universe v u diff --git a/Mathlib/Algebra/Category/AlgebraCat/Limits.lean b/Mathlib/Algebra/Category/AlgebraCat/Limits.lean index a408921e85ef4..bdbde8808325a 100644 --- a/Mathlib/Algebra/Category/AlgebraCat/Limits.lean +++ b/Mathlib/Algebra/Category/AlgebraCat/Limits.lean @@ -16,9 +16,7 @@ the underlying types are just the limits in the category of types. -/ -open CategoryTheory - -open CategoryTheory.Limits +open CategoryTheory Limits universe v w u t diff --git a/Mathlib/Algebra/Category/FGModuleCat/Basic.lean b/Mathlib/Algebra/Category/FGModuleCat/Basic.lean index e288c63e14e86..01ae8aab6bb4d 100644 --- a/Mathlib/Algebra/Category/FGModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/FGModuleCat/Basic.lean @@ -34,8 +34,6 @@ noncomputable section open CategoryTheory ModuleCat.monoidalCategory -open scoped Classical - universe u section Ring diff --git a/Mathlib/Algebra/Category/FGModuleCat/Limits.lean b/Mathlib/Algebra/Category/FGModuleCat/Limits.lean index 3682f87f8ed3b..8faee2b976d4c 100644 --- a/Mathlib/Algebra/Category/FGModuleCat/Limits.lean +++ b/Mathlib/Algebra/Category/FGModuleCat/Limits.lean @@ -28,9 +28,7 @@ noncomputable section universe v u -open CategoryTheory - -open CategoryTheory.Limits +open CategoryTheory Limits namespace FGModuleCat diff --git a/Mathlib/Algebra/Category/Grp/Adjunctions.lean b/Mathlib/Algebra/Category/Grp/Adjunctions.lean index 92b143f959c69..2cbb769fcc95c 100644 --- a/Mathlib/Algebra/Category/Grp/Adjunctions.lean +++ b/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`. -/ diff --git a/Mathlib/Algebra/Category/Grp/FilteredColimits.lean b/Mathlib/Algebra/Category/Grp/FilteredColimits.lean index a8487a47152d2..2fe1025945d7f 100644 --- a/Mathlib/Algebra/Category/Grp/FilteredColimits.lean +++ b/Mathlib/Algebra/Category/Grp/FilteredColimits.lean @@ -26,13 +26,9 @@ universe v u noncomputable section -open scoped Classical +open CategoryTheory Limits -open CategoryTheory - -open CategoryTheory.Limits - -open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`. +open IsFiltered renaming max → max' -- avoid name collision with `_root_.max`. namespace Grp.FilteredColimits diff --git a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean index 9927053031b52..9035d34b23389 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean @@ -24,8 +24,6 @@ namespace ModuleCat universe u -open scoped Classical - variable (R : Type u) section diff --git a/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean b/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean index d7905e97a94ab..5beb3d1633472 100644 --- a/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean +++ b/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`. diff --git a/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean b/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean index 3010093f4483f..8ef1a354bfcd7 100644 --- a/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean +++ b/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean @@ -26,13 +26,9 @@ universe v u noncomputable section -open scoped Classical +open CategoryTheory Limits -open CategoryTheory - -open CategoryTheory.Limits - -open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`. +open IsFiltered renaming max → max' -- avoid name collision with `_root_.max`. namespace MonCat.FilteredColimits diff --git a/Mathlib/Algebra/Category/Ring/Adjunctions.lean b/Mathlib/Algebra/Category/Ring/Adjunctions.lean index 9cd152875d3c5..49cbc29469c4e 100644 --- a/Mathlib/Algebra/Category/Ring/Adjunctions.lean +++ b/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`. -/ diff --git a/Mathlib/Algebra/Category/Ring/Colimits.lean b/Mathlib/Algebra/Category/Ring/Colimits.lean index 007846ae35086..01e11c4fde83c 100644 --- a/Mathlib/Algebra/Category/Ring/Colimits.lean +++ b/Mathlib/Algebra/Category/Ring/Colimits.lean @@ -18,9 +18,7 @@ by a tactic that analyses the shape of `CommRing` and `RingHom`. universe u v -open CategoryTheory - -open CategoryTheory.Limits +open CategoryTheory Limits namespace RingCat.Colimits diff --git a/Mathlib/Algebra/Category/Ring/Constructions.lean b/Mathlib/Algebra/Category/Ring/Constructions.lean index 1f731dd378510..0736d93d4951f 100644 --- a/Mathlib/Algebra/Category/Ring/Constructions.lean +++ b/Mathlib/Algebra/Category/Ring/Constructions.lean @@ -26,7 +26,7 @@ suppress_compilation universe u u' -open CategoryTheory CategoryTheory.Limits TensorProduct +open CategoryTheory Limits TensorProduct namespace CommRingCat diff --git a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean index ae9b4f16f6d0f..99fcc64a9f41a 100644 --- a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean +++ b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean @@ -26,13 +26,9 @@ universe v u noncomputable section -open scoped Classical +open CategoryTheory Limits -open CategoryTheory - -open CategoryTheory.Limits - -open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`. +open IsFiltered renaming max → max' -- avoid name collision with `_root_.max`. open AddMonCat.FilteredColimits (colimit_zero_eq colimit_add_mk_eq) diff --git a/Mathlib/Algebra/EuclideanDomain/Defs.lean b/Mathlib/Algebra/EuclideanDomain/Defs.lean index cbf6398f42982..81b62ab8bf111 100644 --- a/Mathlib/Algebra/EuclideanDomain/Defs.lean +++ b/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 diff --git a/Mathlib/Algebra/Field/IsField.lean b/Mathlib/Algebra/Field/IsField.lean index 2e2fa1c2c0a48..4890d9fed4f35 100644 --- a/Mathlib/Algebra/Field/IsField.lean +++ 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› diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean index a30b9d1bb2f78..2ca5fe50f09d6 100644 --- a/Mathlib/Algebra/Group/Subgroup/Basic.lean +++ b/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 => diff --git a/Mathlib/Algebra/GroupWithZero/Basic.lean b/Mathlib/Algebra/GroupWithZero/Basic.lean index 33a2ab0f957bf..857d0272350c0 100644 --- a/Mathlib/Algebra/GroupWithZero/Basic.lean +++ b/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 := diff --git a/Mathlib/Algebra/GroupWithZero/Commute.lean b/Mathlib/Algebra/GroupWithZero/Commute.lean index 857dbd7021783..59423cb09016f 100644 --- a/Mathlib/Algebra/GroupWithZero/Commute.lean +++ b/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) diff --git a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean index 9aa93f3327f8b..2dda38c3fdafd 100644 --- a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean +++ 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] diff --git a/Mathlib/Algebra/Homology/ComplexShape.lean b/Mathlib/Algebra/Homology/ComplexShape.lean index 84ca1ef14c1f4..217da35df2a5d 100644 --- a/Mathlib/Algebra/Homology/ComplexShape.lean +++ b/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. -/ diff --git a/Mathlib/Algebra/Homology/DifferentialObject.lean b/Mathlib/Algebra/Homology/DifferentialObject.lean index e2228fc04711b..cd85f3f0e9e6c 100644 --- a/Mathlib/Algebra/Homology/DifferentialObject.lean +++ b/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. -/ diff --git a/Mathlib/Algebra/Homology/Homotopy.lean b/Mathlib/Algebra/Homology/Homotopy.lean index b7d9369d9056e..508deb6f6d08f 100644 --- a/Mathlib/Algebra/Homology/Homotopy.lean +++ b/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 diff --git a/Mathlib/Algebra/Homology/HomotopyCategory.lean b/Mathlib/Algebra/Homology/HomotopyCategory.lean index 701bc36e72ed0..a938f482ae5ea 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory.lean +++ b/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 diff --git a/Mathlib/Algebra/Homology/ImageToKernel.lean b/Mathlib/Algebra/Homology/ImageToKernel.lean index 23729e925d685..7ab7f5ff1347d 100644 --- a/Mathlib/Algebra/Homology/ImageToKernel.lean +++ b/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 diff --git a/Mathlib/Algebra/Module/DedekindDomain.lean b/Mathlib/Algebra/Module/DedekindDomain.lean index 9e1889bead349..9a4b65f709a27 100644 --- a/Mathlib/Algebra/Module/DedekindDomain.lean +++ b/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 diff --git a/Mathlib/Algebra/Module/PID.lean b/Mathlib/Algebra/Module/PID.lean index 9650425b473c9..83c608ab901a1 100644 --- a/Mathlib/Algebra/Module/PID.lean +++ b/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] diff --git a/Mathlib/Algebra/MonoidAlgebra/Degree.lean b/Mathlib/Algebra/MonoidAlgebra/Degree.lean index b3ba9ae8af631..8f97bb08cbb59 100644 --- a/Mathlib/Algebra/MonoidAlgebra/Degree.lean +++ b/Mathlib/Algebra/MonoidAlgebra/Degree.lean @@ -20,8 +20,6 @@ variable {R R' A T B ι : Type*} namespace AddMonoidAlgebra -open scoped Classical - /-! # sup-degree and inf-degree of an `AddMonoidAlgebra` @@ -82,8 +80,10 @@ a type with *b*ot or *t*op respectively. variable (degb : A → B) (degt : A → T) (f g : R[A]) -theorem sup_support_add_le : (f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb := - (Finset.sup_mono Finsupp.support_add).trans_eq Finset.sup_union +theorem sup_support_add_le : + (f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb := by + classical + exact (Finset.sup_mono Finsupp.support_add).trans_eq Finset.sup_union theorem le_inf_support_add : f.support.inf degt ⊓ g.support.inf degt ≤ (f + g).support.inf degt := sup_support_add_le (fun a : A => OrderDual.toDual (degt a)) f g @@ -98,8 +98,9 @@ variable [Add A] [Add B] [Add T] [CovariantClass B B (· + ·) (· ≤ ·)] theorem sup_support_mul_le {degb : A → B} (degbm : ∀ {a b}, degb (a + b) ≤ degb a + degb b) (f g : R[A]) : - (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb := - (Finset.sup_mono <| support_mul _ _).trans <| Finset.sup_add_le.2 fun _fd fds _gd gds ↦ + (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb := by + classical + exact (Finset.sup_mono <| support_mul _ _).trans <| Finset.sup_add_le.2 fun _fd fds _gd gds ↦ degbm.trans <| add_le_add (Finset.le_sup fds) (Finset.le_sup gds) theorem le_inf_support_mul {degt : A → T} (degtm : ∀ {a b}, degt a + degt b ≤ degt (a + b)) @@ -232,13 +233,15 @@ theorem supDegree_sub_le {f g : R'[A]} : rw [sub_eq_add_neg, ← supDegree_neg (f := g)]; apply supDegree_add_le theorem supDegree_sum_le {ι} {s : Finset ι} {f : ι → R[A]} : - (∑ i ∈ s, f i).supDegree D ≤ s.sup (fun i => (f i).supDegree D) := - (Finset.sup_mono Finsupp.support_finset_sum).trans_eq (Finset.sup_biUnion _ _) + (∑ i ∈ s, f i).supDegree D ≤ s.sup (fun i => (f i).supDegree D) := by + classical + exact (Finset.sup_mono Finsupp.support_finset_sum).trans_eq (Finset.sup_biUnion _ _) theorem supDegree_single_ne_zero (a : A) {r : R} (hr : r ≠ 0) : (single a r).supDegree D = D a := by rw [supDegree, Finsupp.support_single_ne_zero a hr, Finset.sup_singleton] +open Classical in theorem supDegree_single (a : A) (r : R) : (single a r).supDegree D = if r = 0 then ⊥ else D a := by split_ifs with hr <;> simp [supDegree_single_ne_zero, hr] @@ -270,6 +273,7 @@ theorem supDegree_prod_le {R A B : Type*} [CommSemiring R] [AddCommMonoid A] [Ad {D : A → B} (hzero : D 0 = 0) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) {ι} {s : Finset ι} {f : ι → R[A]} : (∏ i ∈ s, f i).supDegree D ≤ ∑ i ∈ s, (f i).supDegree D := by + classical refine s.induction ?_ ?_ · rw [Finset.prod_empty, Finset.sum_empty, one_def, supDegree_single] split_ifs; exacts [bot_le, hzero.le] @@ -282,6 +286,7 @@ variable [CovariantClass B B (· + ·) (· < ·)] [CovariantClass B B (Function. theorem apply_add_of_supDegree_le (hD : D.Injective) {ap aq : A} (hp : p.supDegree D ≤ D ap) (hq : q.supDegree D ≤ D aq) : (p * q) (ap + aq) = p ap * q aq := by + classical simp_rw [mul_apply, Finsupp.sum] rw [Finset.sum_eq_single ap, Finset.sum_eq_single aq, if_pos rfl] · refine fun a ha hne => if_neg (fun he => ?_) diff --git a/Mathlib/Algebra/MvPolynomial/Rename.lean b/Mathlib/Algebra/MvPolynomial/Rename.lean index 3987d85a83ca3..3043309529923 100644 --- a/Mathlib/Algebra/MvPolynomial/Rename.lean +++ b/Mathlib/Algebra/MvPolynomial/Rename.lean @@ -106,8 +106,7 @@ section variable {f : σ → τ} (hf : Function.Injective f) -open scoped Classical - +open Classical in /-- Given a function between sets of variables `f : σ → τ` that is injective with proof `hf`, `MvPolynomial.killCompl hf` is the `AlgHom` from `R[τ]` to `R[σ]` that is left inverse to `rename f : R[σ] → R[τ]` and sends the variables in the complement of the range of `f` to `0`. -/ diff --git a/Mathlib/Algebra/Order/CauSeq/Completion.lean b/Mathlib/Algebra/Order/CauSeq/Completion.lean index 6a8ebe09f7d4b..1cf2efa956c83 100644 --- a/Mathlib/Algebra/Order/CauSeq/Completion.lean +++ b/Mathlib/Algebra/Order/CauSeq/Completion.lean @@ -172,8 +172,6 @@ instance Cauchy.commRing : CommRing (Cauchy abv) := end -open scoped Classical - section variable {α : Type*} [LinearOrderedField α] @@ -185,6 +183,7 @@ instance instRatCast : RatCast (Cauchy abv) where ratCast q := ofRat q @[simp, norm_cast] lemma ofRat_nnratCast (q : ℚ≥0) : ofRat (q : β) = (q : Cauchy abv) := rfl @[simp, norm_cast] lemma ofRat_ratCast (q : ℚ) : ofRat (q : β) = (q : Cauchy abv) := rfl +open Classical in noncomputable instance : Inv (Cauchy abv) := ⟨fun x => (Quotient.liftOn x fun f => mk <| if h : LimZero f then 0 else inv f h) fun f g fg => by diff --git a/Mathlib/Algebra/Order/CompleteField.lean b/Mathlib/Algebra/Order/CompleteField.lean index 4c82742b3d068..2effd10d52e6f 100644 --- a/Mathlib/Algebra/Order/CompleteField.lean +++ b/Mathlib/Algebra/Order/CompleteField.lean @@ -49,7 +49,7 @@ noncomputable section open Function Rat Real Set -open scoped Classical Pointwise +open scoped Pointwise /-- A field which is both linearly ordered and conditionally complete with respect to the order. This axiomatizes the reals. -/ diff --git a/Mathlib/Algebra/Order/GroupWithZero/Synonym.lean b/Mathlib/Algebra/Order/GroupWithZero/Synonym.lean index ab72ca78d9a3e..9a011c669888c 100644 --- a/Mathlib/Algebra/Order/GroupWithZero/Synonym.lean +++ b/Mathlib/Algebra/Order/GroupWithZero/Synonym.lean @@ -13,8 +13,6 @@ Transfer algebraic instances from `α` to `αᵒᵈ` and `Lex α`. -/ -open scoped Classical - open Function variable {α : Type*} diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean index b8e75f246b4db..d3e6d63300354 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean @@ -427,8 +427,7 @@ section Field /-! ### Group operation polynomials over a field -/ -open scoped Classical - +open Classical in /-- 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)$, and has slope $(y_1 - y_2) / (x_1 - x_2)$. Otherwise, if $y_1 \ne -y_1 - a_1x_1 - a_3$, @@ -640,10 +639,9 @@ 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 scoped Classical - variable {F : Type u} [Field F] {W : Affine F} +open Classical in /-- The addition of two nonsingular rational points on `W`. Given two nonsingular rational points `P` and `Q` on `W`, use `P + Q` instead of `add P Q`. -/ diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean index 79fbbd7ed1b07..2154fb228839b 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean @@ -1152,8 +1152,7 @@ section Addition /-! ### Addition on point representatives -/ -open scoped Classical - +open Classical in variable (W') in /-- The addition of two point representatives. -/ noncomputable def add (P Q : Fin 3 → R) : Fin 3 → R := @@ -1412,10 +1411,9 @@ section Affine /-! ### Equivalence with affine coordinates -/ -open scoped Classical - namespace Point +open Classical in variable (W) in /-- The map from a point representative that is nonsingular on a Weierstrass curve `W` in Jacobian coordinates to the corresponding nonsingular rational point on `W` in affine coordinates. -/ diff --git a/Mathlib/AlgebraicGeometry/Limits.lean b/Mathlib/AlgebraicGeometry/Limits.lean index e97a70c3bb3a2..7034f5fe1de27 100644 --- a/Mathlib/AlgebraicGeometry/Limits.lean +++ b/Mathlib/AlgebraicGeometry/Limits.lean @@ -124,7 +124,6 @@ section Coproduct variable {ι : Type u} (f : ι → Scheme.{u}) -open scoped Classical /-- (Implementation Detail) The glue data associated to a disjoint union. -/ @[simps] diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean index cb54759a505dd..07a434ddae9cb 100644 --- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean +++ b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean @@ -30,8 +30,6 @@ and Chris Hughes (on an earlier repository). noncomputable section -open scoped Classical - universe u v variable (R : Type u) (S : Type v) diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Maximal.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Maximal.lean index 7092a5c7c4c2c..09a9002985e01 100644 --- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Maximal.lean +++ b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Maximal.lean @@ -26,8 +26,6 @@ natural inclusion into the prime spectrum to avoid API duplication for zero loci noncomputable section -open scoped Classical - universe u v variable (R : Type u) [CommRing R] diff --git a/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/StructureSheaf.lean index 2bd0f2e4117e8..a145948515d7c 100644 --- a/Mathlib/AlgebraicGeometry/StructureSheaf.lean +++ b/Mathlib/AlgebraicGeometry/StructureSheaf.lean @@ -750,8 +750,6 @@ theorem normalize_finite_fraction_representation (U : Opens (PrimeSpectrum.Top R rw [pow_succ] ring -open scoped Classical - -- Porting note: in the following proof there are two places where `⋃ i, ⋃ (hx : i ∈ _), ... ` -- though `hx` is not used in `...` part, it is still required to maintain the structure of -- the original proof in mathlib3. diff --git a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean index ea6a3471f3979..9ec3a106004a8 100644 --- a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean +++ b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean @@ -20,7 +20,7 @@ noncomputable section namespace SimplexCategory -open Simplicial NNReal Classical CategoryTheory +open Simplicial NNReal CategoryTheory attribute [local instance] ConcreteCategory.hasCoeToSort ConcreteCategory.instFunLike @@ -39,6 +39,7 @@ instance (x : SimplexCategory) : CoeFun x.toTopObj fun _ => x → ℝ≥0 := theorem toTopObj.ext {x : SimplexCategory} (f g : x.toTopObj) : (f : x → ℝ≥0) = g → f = g := Subtype.ext +open Classical in /-- A morphism in `SimplexCategory` induces a map on the associated topological spaces. -/ def toTopMap {x y : SimplexCategory} (f : x ⟶ y) (g : x.toTopObj) : y.toTopObj := ⟨fun i => ∑ j ∈ Finset.univ.filter (f · = i), g j, by @@ -49,6 +50,7 @@ def toTopMap {x y : SimplexCategory} (f : x ⟶ y) (g : x.toTopObj) : y.toTopObj simp [Finset.eq_univ_iff_forall] · apply Set.pairwiseDisjoint_filter⟩ +open Classical in @[simp] theorem coe_toTopMap {x y : SimplexCategory} (f : x ⟶ y) (g : x.toTopObj) (i : y) : toTopMap f g i = ∑ j ∈ Finset.univ.filter (f · = i), g j := @@ -66,6 +68,7 @@ def toTop : SimplexCategory ⥤ TopCat where obj x := TopCat.of x.toTopObj map f := ⟨toTopMap f, by continuity⟩ map_id := by + classical intro Δ ext f apply toTopObj.ext @@ -73,6 +76,7 @@ def toTop : SimplexCategory ⥤ TopCat where change (Finset.univ.filter (· = i)).sum _ = _ simp [Finset.sum_filter, CategoryTheory.id_apply] map_comp := fun f g => by + classical ext h apply toTopObj.ext funext i diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean index 753771bcacc87..f3b6c32015311 100644 --- a/Mathlib/Analysis/Analytic/Basic.lean +++ b/Mathlib/Analysis/Analytic/Basic.lean @@ -80,10 +80,7 @@ noncomputable section variable {𝕜 E F G : Type*} -open scoped Classical -open Topology NNReal Filter ENNReal - -open Set Filter Asymptotics +open Topology NNReal Filter ENNReal Set Asymptotics namespace FormalMultilinearSeries diff --git a/Mathlib/Analysis/ConstantSpeed.lean b/Mathlib/Analysis/ConstantSpeed.lean index fdc2deba3b934..48b06bbe4565c 100644 --- a/Mathlib/Analysis/ConstantSpeed.lean +++ b/Mathlib/Analysis/ConstantSpeed.lean @@ -40,7 +40,7 @@ arc-length, parameterization open scoped NNReal ENNReal -open Set MeasureTheory Classical +open Set MeasureTheory variable {α : Type*} [LinearOrder α] {E : Type*} [PseudoEMetricSpace E] variable (f : ℝ → E) (s : Set ℝ) (l : ℝ≥0) diff --git a/Mathlib/Analysis/Hofer.lean b/Mathlib/Analysis/Hofer.lean index fc792ba302f13..6ed5d0e71bb32 100644 --- a/Mathlib/Analysis/Hofer.lean +++ b/Mathlib/Analysis/Hofer.lean @@ -18,11 +18,7 @@ example of a proof needing to construct a sequence by induction in the middle of * H. Hofer and C. Viterbo, *The Weinstein conjecture in the presence of holomorphic spheres* -/ - -open scoped Classical -open Topology - -open Filter Finset +open Topology Filter Finset local notation "d" => dist diff --git a/Mathlib/Analysis/MeanInequalities.lean b/Mathlib/Analysis/MeanInequalities.lean index cb2c6cb36164d..faa0d4a8ba9e3 100644 --- a/Mathlib/Analysis/MeanInequalities.lean +++ b/Mathlib/Analysis/MeanInequalities.lean @@ -104,10 +104,8 @@ less than or equal to the sum of the maximum values of the summands. universe u v -open scoped Classical open Finset NNReal ENNReal - noncomputable section variable {ι : Type u} (s : Finset ι) diff --git a/Mathlib/Analysis/MeanInequalitiesPow.lean b/Mathlib/Analysis/MeanInequalitiesPow.lean index 77e7e2413dc01..91c0a4ed1cb78 100644 --- a/Mathlib/Analysis/MeanInequalitiesPow.lean +++ b/Mathlib/Analysis/MeanInequalitiesPow.lean @@ -43,10 +43,7 @@ in order to avoid using real exponents. For real exponents we prove both this an universe u v -open Finset - -open scoped Classical -open NNReal ENNReal +open Finset NNReal ENNReal noncomputable section diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean index 66555ba6c6bf2..44d821de11bfc 100644 --- a/Mathlib/Analysis/Seminorm.lean +++ b/Mathlib/Analysis/Seminorm.lean @@ -471,8 +471,7 @@ theorem smul_inf [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] (r section Classical -open scoped Classical - +open Classical in /-- We define the supremum of an arbitrary subset of `Seminorm 𝕜 E` as follows: * if `s` is `BddAbove` *as a set of functions `E → ℝ`* (that is, if `s` is pointwise bounded above), we take the pointwise supremum of all elements of `s`, and we prove that it is indeed a diff --git a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean index 970cfeb8b6b2c..7464246e2fb52 100644 --- a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean +++ b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean @@ -116,7 +116,6 @@ circle homeomorphism, rotation number -/ -open scoped Classical open Filter Set Int Topology open Function hiding Commute diff --git a/Mathlib/Dynamics/Ergodic/Conservative.lean b/Mathlib/Dynamics/Ergodic/Conservative.lean index f9ec631f7d71c..4853d8c9c1bfc 100644 --- a/Mathlib/Dynamics/Ergodic/Conservative.lean +++ b/Mathlib/Dynamics/Ergodic/Conservative.lean @@ -38,11 +38,7 @@ conservative dynamical system, Poincare recurrence theorem noncomputable section -open scoped Classical -open Set Filter MeasureTheory Finset Function TopologicalSpace - -open scoped Classical -open Topology +open Set Filter MeasureTheory Finset Function TopologicalSpace Topology variable {ι : Type*} {α : Type*} [MeasurableSpace α] {f : α → α} {s : Set α} {μ : Measure α} diff --git a/Mathlib/FieldTheory/AbelRuffini.lean b/Mathlib/FieldTheory/AbelRuffini.lean index 4375f8b5ece79..2fb1bfe62c908 100644 --- a/Mathlib/FieldTheory/AbelRuffini.lean +++ b/Mathlib/FieldTheory/AbelRuffini.lean @@ -26,8 +26,6 @@ that is solvable by radicals has a solvable Galois group. noncomputable section -open scoped Classical Polynomial IntermediateField - open Polynomial IntermediateField section AbelRuffini diff --git a/Mathlib/FieldTheory/Finiteness.lean b/Mathlib/FieldTheory/Finiteness.lean index 51cbab65d5e7f..6c2e5621a9272 100644 --- a/Mathlib/FieldTheory/Finiteness.lean +++ b/Mathlib/FieldTheory/Finiteness.lean @@ -15,9 +15,6 @@ import Mathlib.LinearAlgebra.Dimension.Finite universe u v -open scoped Classical -open Cardinal - open Cardinal Submodule Module Function namespace IsNoetherian diff --git a/Mathlib/FieldTheory/Fixed.lean b/Mathlib/FieldTheory/Fixed.lean index 7271eac72885f..11e8c66077f0c 100644 --- a/Mathlib/FieldTheory/Fixed.lean +++ b/Mathlib/FieldTheory/Fixed.lean @@ -30,8 +30,6 @@ element of `G`, where `G` is a group that acts on `F`. noncomputable section -open scoped Classical - open MulAction Finset FiniteDimensional universe u v w @@ -114,7 +112,8 @@ theorem coe_algebraMap : theorem linearIndependent_smul_of_linearIndependent {s : Finset F} : (LinearIndependent (FixedPoints.subfield G F) fun i : (s : Set F) => (i : F)) → LinearIndependent F fun i : (s : Set F) => MulAction.toFun G F i := by - haveI : IsEmpty ((∅ : Finset F) : Set F) := by simp + classical + have : IsEmpty ((∅ : Finset F) : Set F) := by simp refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_ rw [coe_insert] at hs ⊢ rw [linearIndependent_insert (mt mem_coe.1 has)] at hs @@ -187,6 +186,7 @@ theorem ne_one : minpoly G F x ≠ (1 : Polynomial (FixedPoints.subfield G F)) : theorem of_eval₂ (f : Polynomial (FixedPoints.subfield G F)) (hf : Polynomial.eval₂ (Subfield.subtype <| FixedPoints.subfield G F) x f = 0) : minpoly G F x ∣ f := by + classical -- Porting note: the two `have` below were not needed. have : (subfield G F).subtype = (subfield G F).toSubring.subtype := rfl have h : Polynomial.map (MulSemiringActionHom.toRingHom (IsInvariantSubring.subtypeHom G @@ -263,8 +263,9 @@ instance normal : Normal (FixedPoints.subfield G F) F where Polynomial.map_toSubring _ (subfield G F).toSubring, prodXSubSMul] exact Polynomial.splits_prod _ fun _ _ => Polynomial.splits_X_sub_C _ -instance isSeparable : Algebra.IsSeparable (FixedPoints.subfield G F) F := - ⟨fun x => by +instance isSeparable : Algebra.IsSeparable (FixedPoints.subfield G F) F := by + classical + exact ⟨fun x => by cases nonempty_fintype G -- this was a plain rw when we were using unbundled subrings erw [IsSeparable, ← minpoly_eq_minpoly, diff --git a/Mathlib/FieldTheory/IsPerfectClosure.lean b/Mathlib/FieldTheory/IsPerfectClosure.lean index 45770089e7168..b9d456514b0a7 100644 --- a/Mathlib/FieldTheory/IsPerfectClosure.lean +++ b/Mathlib/FieldTheory/IsPerfectClosure.lean @@ -60,8 +60,6 @@ perfect ring, perfect closure, purely inseparable -/ -open scoped Classical Polynomial - open FiniteDimensional Polynomial IntermediateField Field noncomputable section diff --git a/Mathlib/FieldTheory/IsSepClosed.lean b/Mathlib/FieldTheory/IsSepClosed.lean index 04345fdd830ff..a986c4144c374 100644 --- a/Mathlib/FieldTheory/IsSepClosed.lean +++ b/Mathlib/FieldTheory/IsSepClosed.lean @@ -50,8 +50,6 @@ separable closure, separably closed universe u v w -open scoped Classical Polynomial - open Polynomial variable (k : Type u) [Field k] (K : Type v) [Field K] diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean index 81335556ddaac..18d9b02736673 100644 --- a/Mathlib/FieldTheory/KrullTopology.lean +++ b/Mathlib/FieldTheory/KrullTopology.lean @@ -52,7 +52,7 @@ all intermediate fields `E` with `E/K` finite dimensional. - `krullTopology K L` is defined as an instance for type class inference. -/ -open scoped Classical Pointwise +open scoped Pointwise /-- Mapping intermediate fields along the identity does not change them -/ theorem IntermediateField.map_id {K L : Type*} [Field K] [Field L] [Algebra K L] diff --git a/Mathlib/FieldTheory/Laurent.lean b/Mathlib/FieldTheory/Laurent.lean index 67da3a9bcaff4..6336d85e6f5df 100644 --- a/Mathlib/FieldTheory/Laurent.lean +++ b/Mathlib/FieldTheory/Laurent.lean @@ -30,7 +30,7 @@ noncomputable section open Polynomial -open scoped Classical nonZeroDivisors Polynomial +open scoped nonZeroDivisors variable {R : Type u} [CommRing R] [hdomain : IsDomain R] (r s : R) (p q : R[X]) (f : RatFunc R) diff --git a/Mathlib/FieldTheory/MvPolynomial.lean b/Mathlib/FieldTheory/MvPolynomial.lean index 3e27cb410ee71..fb3b4bacc303b 100644 --- a/Mathlib/FieldTheory/MvPolynomial.lean +++ b/Mathlib/FieldTheory/MvPolynomial.lean @@ -18,8 +18,6 @@ finitely supported functions from the indexing set to `ℕ`. noncomputable section -open scoped Classical - open Set LinearMap Submodule namespace MvPolynomial @@ -45,8 +43,6 @@ universe u variable {σ : Type u} {K : Type u} [Field K] -open scoped Classical - theorem rank_mvPolynomial : Module.rank K (MvPolynomial σ K) = Cardinal.mk (σ →₀ ℕ) := by rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank] diff --git a/Mathlib/FieldTheory/Normal.lean b/Mathlib/FieldTheory/Normal.lean index 4d617e4f95701..6631e005d1ab9 100644 --- a/Mathlib/FieldTheory/Normal.lean +++ b/Mathlib/FieldTheory/Normal.lean @@ -22,8 +22,6 @@ is the same as being a splitting field (`Normal.of_isSplittingField` and noncomputable section -open scoped Classical Polynomial - open Polynomial IsScalarTower variable (F K : Type*) [Field F] [Field K] [Algebra F K] @@ -57,6 +55,7 @@ instance normal_self : Normal F F where theorem Normal.exists_isSplittingField [h : Normal F K] [FiniteDimensional F K] : ∃ p : F[X], IsSplittingField F K p := by + classical let s := Basis.ofVectorSpace F K refine ⟨∏ x, minpoly F (s x), splits_prod _ fun x _ => h.splits (s x), diff --git a/Mathlib/FieldTheory/PrimitiveElement.lean b/Mathlib/FieldTheory/PrimitiveElement.lean index db00b65f85c7c..544521dd8fdca 100644 --- a/Mathlib/FieldTheory/PrimitiveElement.lean +++ b/Mathlib/FieldTheory/PrimitiveElement.lean @@ -37,8 +37,6 @@ exists_adjoin_simple_eq_top noncomputable section -open scoped Classical Polynomial - open FiniteDimensional Polynomial IntermediateField namespace Field @@ -80,6 +78,7 @@ variable {F : Type*} [Field F] [Infinite F] {E : Type*} [Field E] (ϕ : F →+* theorem primitive_element_inf_aux_exists_c (f g : F[X]) : ∃ c : F, ∀ α' ∈ (f.map ϕ).roots, ∀ β' ∈ (g.map ϕ).roots, -(α' - α) / (β' - β) ≠ ϕ c := by + classical let sf := (f.map ϕ).roots let sg := (g.map ϕ).roots let s := (sf.bind fun α' => sg.map fun β' => -(α' - α) / (β' - β)).toFinset @@ -96,6 +95,7 @@ variable [Algebra F E] /-- This is the heart of the proof of the primitive element theorem. It shows that if `F` is infinite and `α` and `β` are separable over `F` then `F⟮α, β⟯` is generated by a single element. -/ theorem primitive_element_inf_aux [Algebra.IsSeparable F E] : ∃ γ : E, F⟮α, β⟯ = F⟮γ⟯ := by + classical have hα := Algebra.IsSeparable.isIntegral F α have hβ := Algebra.IsSeparable.isIntegral F β let f := minpoly F α diff --git a/Mathlib/FieldTheory/Separable.lean b/Mathlib/FieldTheory/Separable.lean index 88a4ce5273fab..58a4f2be710fe 100644 --- a/Mathlib/FieldTheory/Separable.lean +++ b/Mathlib/FieldTheory/Separable.lean @@ -29,7 +29,6 @@ over `K` universe u v w -open scoped Classical open Polynomial Finset namespace Polynomial @@ -86,11 +85,13 @@ theorem Separable.of_dvd {f g : R[X]} (hf : f.Separable) (hfg : g ∣ f) : g.Sep rcases hfg with ⟨f', rfl⟩ exact Separable.of_mul_left hf -theorem separable_gcd_left {F : Type*} [Field F] {f : F[X]} (hf : f.Separable) (g : F[X]) : +theorem separable_gcd_left {F : Type*} [Field F] [DecidableEq F[X]] + {f : F[X]} (hf : f.Separable) (g : F[X]) : (EuclideanDomain.gcd f g).Separable := Separable.of_dvd hf (EuclideanDomain.gcd_dvd_left f g) -theorem separable_gcd_right {F : Type*} [Field F] {g : F[X]} (f : F[X]) (hg : g.Separable) : +theorem separable_gcd_right {F : Type*} [Field F] [DecidableEq F[X]] + {g : F[X]} (f : F[X]) (hg : g.Separable) : (EuclideanDomain.gcd f g).Separable := Separable.of_dvd hg (EuclideanDomain.gcd_dvd_right f g) @@ -166,7 +167,8 @@ theorem isUnit_of_self_mul_dvd_separable {p q : R[X]} (hp : p.Separable) (hq : q ring exact IsCoprime.of_mul_right_left (IsCoprime.of_mul_left_left this) -theorem multiplicity_le_one_of_separable {p q : R[X]} (hq : ¬IsUnit q) (hsep : Separable p) : +theorem multiplicity_le_one_of_separable [DecidableRel fun (x : R[X]) x_1 ↦ x ∣ x_1] + {p q : R[X]} (hq : ¬IsUnit q) (hsep : Separable p) : multiplicity q p ≤ 1 := by contrapose! hq apply isUnit_of_self_mul_dvd_separable hsep @@ -181,6 +183,7 @@ theorem multiplicity_le_one_of_separable {p q : R[X]} (hq : ¬IsUnit q) (hsep : See `PerfectField.separable_iff_squarefree` for the converse when the coefficients are a perfect field. -/ theorem Separable.squarefree {p : R[X]} (hsep : Separable p) : Squarefree p := by + classical rw [multiplicity.squarefree_iff_multiplicity_le_one p] exact fun f => or_iff_not_imp_right.mpr fun hunit => multiplicity_le_one_of_separable hunit hsep @@ -201,8 +204,9 @@ theorem Separable.mul {f g : R[X]} (hf : f.Separable) (hg : g.Separable) (h : Is theorem separable_prod' {ι : Sort _} {f : ι → R[X]} {s : Finset ι} : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → - (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable := - Finset.induction_on s (fun _ _ => separable_one) fun a s has ih h1 h2 => by + (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable := by + classical + exact Finset.induction_on s (fun _ _ => separable_one) fun a s has ih h1 h2 => by simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2; rw [prod_insert has] exact h2.1.mul (ih h1.2.2 h2.2) @@ -215,6 +219,7 @@ theorem separable_prod {ι : Sort _} [Fintype ι] {f : ι → R[X]} (h1 : Pairwi theorem Separable.inj_of_prod_X_sub_C [Nontrivial R] {ι : Sort _} {f : ι → R} {s : Finset ι} (hfs : (∏ i ∈ s, (X - C (f i))).Separable) {x y : ι} (hx : x ∈ s) (hy : y ∈ s) (hfxy : f x = f y) : x = y := by + classical by_contra hxy rw [← insert_erase hx, prod_insert (not_mem_erase _ _), ← insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy), prod_insert (not_mem_erase _ _), ← @@ -253,6 +258,7 @@ theorem separable_X_pow_sub_C_unit {n : ℕ} (u : Rˣ) (hn : IsUnit (n : R)) : theorem rootMultiplicity_le_one_of_separable [Nontrivial R] {p : R[X]} (hsep : Separable p) (x : R) : rootMultiplicity x p ≤ 1 := by + classical by_cases hp : p = 0 · simp [hp] rw [rootMultiplicity_eq_multiplicity, dif_neg hp, ← PartENat.coe_le_coe, PartENat.natCast_get, @@ -265,12 +271,14 @@ section IsDomain variable {R : Type u} [CommRing R] [IsDomain R] -theorem count_roots_le_one {p : R[X]} (hsep : Separable p) (x : R) : p.roots.count x ≤ 1 := by +theorem count_roots_le_one [DecidableEq R] {p : R[X]} (hsep : Separable p) (x : R) : + p.roots.count x ≤ 1 := by rw [count_roots p] exact rootMultiplicity_le_one_of_separable hsep x -theorem nodup_roots {p : R[X]} (hsep : Separable p) : p.roots.Nodup := - Multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep) +theorem nodup_roots {p : R[X]} (hsep : Separable p) : p.roots.Nodup := by + classical + exact Multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep) end IsDomain @@ -317,8 +325,9 @@ section CharP variable (p : ℕ) [HF : CharP F p] theorem separable_or {f : F[X]} (hf : Irreducible f) : - f.Separable ∨ ¬f.Separable ∧ ∃ g : F[X], Irreducible g ∧ expand F p g = f := - if H : derivative f = 0 then by + f.Separable ∨ ¬f.Separable ∧ ∃ g : F[X], Irreducible g ∧ expand F p g = f := by + classical + exact if H : derivative f = 0 then by rcases p.eq_zero_or_pos with (rfl | hp) · haveI := CharP.charP_to_charZero F have := natDegree_eq_zero_of_derivative_eq_zero H @@ -415,6 +424,7 @@ section Splits theorem card_rootSet_eq_natDegree [Algebra F K] {p : F[X]} (hsep : p.Separable) (hsplit : Splits (algebraMap F K) p) : Fintype.card (p.rootSet K) = p.natDegree := by + classical simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe] rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← natDegree_eq_card_roots hsplit] @@ -422,6 +432,7 @@ theorem card_rootSet_eq_natDegree [Algebra F K] {p : F[X]} (hsep : p.Separable) if and only if it is separable. -/ theorem nodup_roots_iff_of_splits {f : F[X]} (hf : f ≠ 0) (h : f.Splits (RingHom.id F)) : f.roots.Nodup ↔ f.Separable := by + classical refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩ rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep obtain ⟨x, hx⟩ := exists_root_of_splits _ @@ -438,6 +449,7 @@ theorem nodup_aroots_iff_of_splits [Algebra F K] {f : F[X]} (hf : f ≠ 0) theorem card_rootSet_eq_natDegree_iff_of_splits [Algebra F K] {f : F[X]} (hf : f ≠ 0) (h : f.Splits (algebraMap F K)) : Fintype.card (f.rootSet K) = f.natDegree ↔ f.Separable := by + classical simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, natDegree_eq_card_roots h, Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h] @@ -463,6 +475,7 @@ theorem eq_X_sub_C_of_separable_of_root_eq {x : F} {h : F[X]} (h_sep : h.Separab theorem exists_finset_of_splits (i : F →+* K) {f : F[X]} (sep : Separable f) (sp : Splits i f) : ∃ s : Finset K, f.map i = C (i f.leadingCoeff) * s.prod fun a : K => X - C a := by + classical obtain ⟨s, h⟩ := (splits_iff_exists_multiset _).1 sp use s.toFinset rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq] @@ -630,6 +643,7 @@ variable [Algebra K S] [Algebra K L] theorem AlgHom.card_of_powerBasis (pb : PowerBasis K S) (h_sep : IsSeparable K pb.gen) (h_splits : (minpoly K pb.gen).Splits (algebraMap K L)) : @Fintype.card (S →ₐ[K] L) (PowerBasis.AlgHom.fintype pb) = pb.dim := by + classical let _ := (PowerBasis.AlgHom.fintype pb : Fintype (S →ₐ[K] L)) rw [Fintype.card_congr pb.liftEquiv', Fintype.card_of_subtype _ (fun x => Multiset.mem_toFinset), ← pb.natDegree_minpoly, natDegree_eq_card_roots h_splits, Multiset.toFinset_card_of_nodup] diff --git a/Mathlib/FieldTheory/SeparableClosure.lean b/Mathlib/FieldTheory/SeparableClosure.lean index 86d3982eddee7..044959bd5502b 100644 --- a/Mathlib/FieldTheory/SeparableClosure.lean +++ b/Mathlib/FieldTheory/SeparableClosure.lean @@ -59,7 +59,7 @@ separable degree, degree, separable closure -/ -open scoped Classical Polynomial +open scoped Polynomial open FiniteDimensional Polynomial IntermediateField Field diff --git a/Mathlib/MeasureTheory/Group/Prod.lean b/Mathlib/MeasureTheory/Group/Prod.lean index f3f8d5a1e7468..f2e659ca8ab0e 100644 --- a/Mathlib/MeasureTheory/Group/Prod.lean +++ b/Mathlib/MeasureTheory/Group/Prod.lean @@ -46,7 +46,7 @@ open Function MeasureTheory open Filter hiding map -open scoped Classical ENNReal Pointwise MeasureTheory +open scoped ENNReal Pointwise MeasureTheory variable (G : Type*) [MeasurableSpace G] variable [Group G] [MeasurableMul₂ G] diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean index cc7ad243d8578..0e02937ac68d2 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner.lean @@ -298,7 +298,7 @@ theorem integral_eq {m : MeasurableSpace α} (μ : Measure α) (f : α →ₛ F) theorem integral_eq_sum_filter [DecidablePred fun x : F => x ≠ 0] {m : MeasurableSpace α} (f : α →ₛ F) (μ : Measure α) : f.integral μ = ∑ x ∈ f.range.filter fun x => x ≠ 0, (μ (f ⁻¹' {x})).toReal • x := by - rw [integral_def, setToSimpleFunc_eq_sum_filter]; simp_rw [weightedSMul_apply]; congr + simp_rw [integral_def, setToSimpleFunc_eq_sum_filter, weightedSMul_apply] /-- The Bochner integral is equal to a sum over any set that includes `f.range` (except `0`). -/ theorem integral_eq_sum_of_subset [DecidablePred fun x : F => x ≠ 0] {f : α →ₛ F} {s : Finset F} @@ -703,18 +703,13 @@ variable [NormedAddCommGroup E] [NormedSpace ℝ E] [hE : CompleteSpace E] [Nont [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] -section - -open scoped Classical - +open Classical in /-- The Bochner integral -/ irreducible_def integral {_ : MeasurableSpace α} (μ : Measure α) (f : α → G) : G := if _ : CompleteSpace G then if hf : Integrable f μ then L1.integral (hf.toL1 f) else 0 else 0 -end - /-! In the notation for integrals, an expression like `∫ x, g ‖x‖ ∂μ` will not be parsed correctly, and needs parentheses. We do not set the binding power of `r` to `0`, because then `∫ x, f x = 0` will be parsed incorrectly. -/ diff --git a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean index 72fd302ba5803..958b5b34a0ce4 100644 --- a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean +++ b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean @@ -23,7 +23,7 @@ noncomputable section open Set Filter TopologicalSpace MeasureTheory Function -open scoped Classical Topology Interval Filter ENNReal MeasureTheory +open scoped Topology Interval Filter ENNReal MeasureTheory variable {α β E F : Type*} [MeasurableSpace α] @@ -504,6 +504,7 @@ variable [NormedAddCommGroup E] theorem ContinuousOn.aemeasurable [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] {f : α → β} {s : Set α} {μ : Measure α} (hf : ContinuousOn f s) (hs : MeasurableSet s) : AEMeasurable f (μ.restrict s) := by + classical nontriviality α; inhabit α have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩ diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue.lean b/Mathlib/MeasureTheory/Integral/Lebesgue.lean index 2cc61b151535a..bd086669e7f0d 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue.lean @@ -36,13 +36,10 @@ noncomputable section open Set hiding restrict restrict_apply -open Filter ENNReal +open Filter ENNReal Topology NNReal MeasureTheory open Function (support) -open scoped Classical -open Topology NNReal ENNReal MeasureTheory - namespace MeasureTheory local infixr:25 " →ₛ " => SimpleFunc @@ -591,6 +588,7 @@ alias set_lintegral_smul_measure := setLIntegral_smul_measure @[simp] theorem lintegral_sum_measure {m : MeasurableSpace α} {ι} (f : α → ℝ≥0∞) (μ : ι → Measure α) : ∫⁻ a, f a ∂Measure.sum μ = ∑' i, ∫⁻ a, f a ∂μ i := by + classical simp only [lintegral, iSup_subtype', SimpleFunc.lintegral_sum, ENNReal.tsum_eq_iSup_sum] rw [iSup_comm] congr; funext s @@ -653,6 +651,7 @@ alias set_lintegral_measure_zero := setLIntegral_measure_zero theorem lintegral_finset_sum' (s : Finset β) {f : β → α → ℝ≥0∞} (hf : ∀ b ∈ s, AEMeasurable (f b) μ) : ∫⁻ a, ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ a, f b a ∂μ := by + classical induction' s using Finset.induction_on with a s has ih · simp · simp only [Finset.sum_insert has] @@ -932,6 +931,7 @@ theorem setLintegral_pos_iff {f : α → ℝ≥0∞} (hf : Measurable f) {s : Se /-- Weaker version of the monotone convergence theorem-/ theorem lintegral_iSup_ae {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, Measurable (f n)) (h_mono : ∀ n, ∀ᵐ a ∂μ, f n a ≤ f n.succ a) : ∫⁻ a, ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ a, f n a ∂μ := by + classical let ⟨s, hs⟩ := exists_measurable_superset_of_null (ae_iff.1 (ae_all_iff.2 h_mono)) let g n a := if a ∈ s then 0 else f n a have g_eq_f : ∀ᵐ a ∂μ, ∀ n, g n a = f n a := @@ -1258,6 +1258,7 @@ end theorem lintegral_tsum [Countable β] {f : β → α → ℝ≥0∞} (hf : ∀ i, AEMeasurable (f i) μ) : ∫⁻ a, ∑' i, f i a ∂μ = ∑' i, ∫⁻ a, f i a ∂μ := by + classical simp only [ENNReal.tsum_eq_iSup_sum] rw [lintegral_iSup_directed] · simp [lintegral_finset_sum' _ fun i _ => hf i] diff --git a/Mathlib/MeasureTheory/Integral/Marginal.lean b/Mathlib/MeasureTheory/Integral/Marginal.lean index 0d23d017587cf..60cf5d485cb95 100644 --- a/Mathlib/MeasureTheory/Integral/Marginal.lean +++ b/Mathlib/MeasureTheory/Integral/Marginal.lean @@ -55,7 +55,7 @@ since there is no well-behaved measure on the domain of `f`. -/ -open scoped Classical ENNReal +open scoped ENNReal open Set Function Equiv Finset noncomputable section diff --git a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean index 7bc9c044ec8c5..9db0c3fc5fb59 100644 --- a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean +++ b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean @@ -52,7 +52,6 @@ only to prove the more general results: noncomputable section -open scoped Classical open NNReal ENNReal MeasureTheory Finset @@ -193,6 +192,7 @@ theorem lintegral_prod_norm_pow_le {α ι : Type*} [MeasurableSpace α] {μ : Me (s : Finset ι) {f : ι → α → ℝ≥0∞} (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : ∑ i ∈ s, p i = 1) (h2p : ∀ i ∈ s, 0 ≤ p i) : ∫⁻ a, ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i := by + classical induction s using Finset.induction generalizing p with | empty => simp at hp diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean index 348737bc598db..c177aeb5d4943 100644 --- a/Mathlib/MeasureTheory/Integral/SetToL1.lean +++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean @@ -70,7 +70,7 @@ with finite measure. Its value on other sets is ignored. noncomputable section -open scoped Classical Topology NNReal ENNReal MeasureTheory Pointwise +open scoped Topology NNReal ENNReal MeasureTheory Pointwise open Set Filter TopologicalSpace ENNReal EMetric @@ -143,6 +143,7 @@ theorem map_iUnion_fin_meas_set_eq_sum (T : Set α → β) (T_empty : T ∅ = 0) (hS_meas : ∀ i, MeasurableSet (S i)) (hSp : ∀ i ∈ sι, μ (S i) ≠ ∞) (h_disj : ∀ᵉ (i ∈ sι) (j ∈ sι), i ≠ j → Disjoint (S i) (S j)) : T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i) := by + classical revert hSp h_disj refine Finset.induction_on sι ?_ ?_ · simp only [Finset.not_mem_empty, IsEmpty.forall_iff, iUnion_false, iUnion_empty, sum_empty, @@ -276,7 +277,8 @@ theorem setToSimpleFunc_zero_apply {m : MeasurableSpace α} (T : Set α → F setToSimpleFunc T (0 : α →ₛ F) = 0 := by cases isEmpty_or_nonempty α <;> simp [setToSimpleFunc] -theorem setToSimpleFunc_eq_sum_filter {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') +theorem setToSimpleFunc_eq_sum_filter [DecidablePred fun x ↦ x ≠ (0 : F)] + {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (f : α →ₛ F) : setToSimpleFunc T f = ∑ x ∈ f.range.filter fun x => x ≠ 0, (T (f ⁻¹' {x})) x := by symm @@ -287,6 +289,7 @@ theorem setToSimpleFunc_eq_sum_filter {m : MeasurableSpace α} (T : Set α → F theorem map_setToSimpleFunc (T : Set α → F →L[ℝ] F') (h_add : FinMeasAdditive μ T) {f : α →ₛ G} (hf : Integrable f μ) {g : G → F} (hg : g 0 = 0) : (f.map g).setToSimpleFunc T = ∑ x ∈ f.range, T (f ⁻¹' {x}) (g x) := by + classical have T_empty : T ∅ = 0 := h_add.map_empty_eq_zero have hfp : ∀ x ∈ f.range, x ≠ 0 → μ (f ⁻¹' {x}) ≠ ∞ := fun x _ hx0 => (measure_preimage_lt_top_of_integrable f hf hx0).ne @@ -376,6 +379,7 @@ theorem setToSimpleFunc_add_left {m : MeasurableSpace α} (T T' : Set α → F theorem setToSimpleFunc_add_left' (T T' T'' : Set α → E →L[ℝ] F) (h_add : ∀ s, MeasurableSet s → μ s < ∞ → T'' s = T s + T' s) {f : α →ₛ E} (hf : Integrable f μ) : setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f := by + classical simp_rw [setToSimpleFunc_eq_sum_filter] suffices ∀ x ∈ filter (fun x : E => x ≠ 0) f.range, T'' (f ⁻¹' {x}) = T (f ⁻¹' {x}) + T' (f ⁻¹' {x}) by @@ -397,6 +401,7 @@ theorem setToSimpleFunc_smul_left {m : MeasurableSpace α} (T : Set α → F → theorem setToSimpleFunc_smul_left' (T T' : Set α → E →L[ℝ] F') (c : ℝ) (h_smul : ∀ s, MeasurableSet s → μ s < ∞ → T' s = c • T s) {f : α →ₛ E} (hf : Integrable f μ) : setToSimpleFunc T' f = c • setToSimpleFunc T f := by + classical simp_rw [setToSimpleFunc_eq_sum_filter] suffices ∀ x ∈ filter (fun x : E => x ≠ 0) f.range, T' (f ⁻¹' {x}) = c • T (f ⁻¹' {x}) by rw [smul_sum] @@ -559,6 +564,7 @@ theorem setToSimpleFunc_indicator (T : Set α → F →L[ℝ] F') (hT_empty : T SimpleFunc.setToSimpleFunc T (SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0)) = T s x := by + classical obtain rfl | hs_empty := s.eq_empty_or_nonempty · simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero, setToSimpleFunc_zero_apply] @@ -1132,6 +1138,7 @@ section Function variable [CompleteSpace F] {T T' T'' : Set α → E →L[ℝ] F} {C C' C'' : ℝ} {f g : α → E} variable (μ T) +open Classical in /-- Extend `T : Set α → E →L[ℝ] F` to `(α → E) → F` (for integrable functions `α → E`). We set it to 0 if the function is not integrable. -/ def setToFun (hT : DominatedFinMeasAdditive μ T C) (f : α → E) : F := @@ -1223,6 +1230,7 @@ theorem setToFun_add (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f theorem setToFun_finset_sum' (hT : DominatedFinMeasAdditive μ T C) {ι} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, Integrable (f i) μ) : setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i) := by + classical revert hf refine Finset.induction_on s ?_ ?_ · intro _ diff --git a/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean b/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean index 8130eea07979e..67325d6b4ba98 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean @@ -237,10 +237,9 @@ theorem exists_countablyGenerated_le_of_countablySeparated [m : MeasurableSpace rw [@separatesPoints_iff] exact fun x y hxy ↦ hb _ trivial _ trivial fun _ hs ↦ hxy _ $ measurableSet_generateFrom hs -open scoped Classical - open Function +open Classical in /-- A map from a measurable space to the Cantor space `ℕ → Bool` induced by a countable sequence of sets generating the measurable space. -/ noncomputable diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean b/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean index 098197eb7f32e..f60cb8c5a745e 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean @@ -38,8 +38,6 @@ measurable space, σ-algebra, measurable function open Set Encodable Function Equiv -open scoped Classical - variable {α β γ δ δ' : Type*} {ι : Sort*} {s t u : Set α} /-- A measurable space is a space equipped with a σ-algebra. -/ @@ -195,6 +193,7 @@ protected theorem MeasurableSet.ite {t s₁ s₂ : Set α} (ht : MeasurableSet t (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (t.ite s₁ s₂) := (h₁.inter ht).union (h₂.diff ht) +open Classical in theorem MeasurableSet.ite' {s t : Set α} {p : Prop} (hs : p → MeasurableSet s) (ht : ¬p → MeasurableSet t) : MeasurableSet (ite p s t) := by split_ifs with h @@ -257,8 +256,10 @@ protected theorem MeasurableSet.insert {s : Set α} (hs : MeasurableSet s) (a : .union (.singleton a) hs @[simp] -theorem measurableSet_insert {a : α} {s : Set α} : MeasurableSet (insert a s) ↔ MeasurableSet s := - ⟨fun h => +theorem measurableSet_insert {a : α} {s : Set α} : + MeasurableSet (insert a s) ↔ MeasurableSet s := by + classical + exact ⟨fun h => if ha : a ∈ s then by rwa [← insert_eq_of_mem ha] else insert_diff_self_of_not_mem ha ▸ h.diff (.singleton _), fun h => h.insert a⟩ diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean b/Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean index facd0e89f3ba9..0f0f93a47b486 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean @@ -623,8 +623,6 @@ theorem of_measurable_inverse (hf₁ : Measurable f) (hf₂ : MeasurableSet (ran (hg : Measurable g) (H : LeftInverse g f) : MeasurableEmbedding f := of_measurable_inverse_on_range hf₁ hf₂ (hg.comp measurable_subtype_coe) H -open scoped Classical - /-- The **measurable Schröder-Bernstein Theorem**: given measurable embeddings `α → β` and `β → α`, we can find a measurable equivalence `α ≃ᵐ β`. -/ noncomputable def schroederBernstein {f : α → β} {g : β → α} (hf : MeasurableEmbedding f) @@ -635,6 +633,7 @@ noncomputable def schroederBernstein {f : α → β} {g : β → α} (hf : Measu -- However, we must find this fixed point manually instead of invoking Knaster-Tarski -- in order to make sure it is measurable. suffices Σ'A : Set α, MeasurableSet A ∧ F A = A by + classical rcases this with ⟨A, Ameas, Afp⟩ let B := f '' A have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas diff --git a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean index 707dd80ec1293..7f07b91e54462 100644 --- a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean +++ b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean @@ -14,7 +14,6 @@ function. This property, called `AEMeasurable f μ`, is defined in the file `Mea We discuss several of its properties that are analogous to properties of measurable functions. -/ -open scoped Classical open MeasureTheory MeasureTheory.Measure Filter Set Function ENNReal variable {ι α β γ δ R : Type*} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] @@ -72,6 +71,7 @@ theorem ae_inf_principal_eq_mk {s} (h : AEMeasurable f (μ.restrict s)) : f =ᶠ @[measurability] theorem sum_measure [Countable ι] {μ : ι → Measure α} (h : ∀ i, AEMeasurable f (μ i)) : AEMeasurable f (sum μ) := by + classical nontriviality β inhabit β set s : ι → Set α := fun i => toMeasurable (μ i) { x | f x ≠ (h i).mk f x } @@ -176,6 +176,7 @@ theorem prod_mk {f : α → β} {g : α → γ} (hf : AEMeasurable f μ) (hg : A theorem exists_ae_eq_range_subset (H : AEMeasurable f μ) {t : Set β} (ht : ∀ᵐ x ∂μ, f x ∈ t) (h₀ : t.Nonempty) : ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g := by + classical let s : Set α := toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ let g : α → β := piecewise s (fun _ => h₀.some) (H.mk f) refine ⟨g, ?_, ?_, ?_⟩ @@ -317,6 +318,7 @@ theorem aemeasurable_indicator_iff₀ {s} (hs : NullMeasurableSet s μ) : value `b` on a set `A` and `0` elsewhere. -/ lemma aemeasurable_indicator_const_iff {s} [MeasurableSingletonClass β] (b : β) [NeZero b] : AEMeasurable (s.indicator (fun _ ↦ b)) μ ↔ NullMeasurableSet s μ := by + classical constructor <;> intro h · convert h.nullMeasurable (MeasurableSet.singleton (0 : β)).compl rw [indicator_const_preimage_eq_union s {0}ᶜ b] @@ -358,6 +360,7 @@ theorem MeasureTheory.Measure.map_mono_of_aemeasurable {f : α → δ} (h : μ then the function is a.e.-measurable. -/ lemma MeasureTheory.NullMeasurable.aemeasurable {f : α → β} [hc : MeasurableSpace.CountablyGenerated β] (h : NullMeasurable f μ) : AEMeasurable f μ := by + classical nontriviality β; inhabit β rcases hc.1 with ⟨S, hSc, rfl⟩ choose! T hTf hTm hTeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_subset_ae_eq diff --git a/Mathlib/MeasureTheory/Measure/Complex.lean b/Mathlib/MeasureTheory/Measure/Complex.lean index 473cf44a4f8dd..ccb2008885c00 100644 --- a/Mathlib/MeasureTheory/Measure/Complex.lean +++ b/Mathlib/MeasureTheory/Measure/Complex.lean @@ -34,7 +34,7 @@ Complex measure noncomputable section -open scoped Classical MeasureTheory ENNReal NNReal +open scoped MeasureTheory ENNReal NNReal variable {α β : Type*} {m : MeasurableSpace α} diff --git a/Mathlib/MeasureTheory/Measure/Dirac.lean b/Mathlib/MeasureTheory/Measure/Dirac.lean index 1073a7ed4d975..ad6623a9ff812 100644 --- a/Mathlib/MeasureTheory/Measure/Dirac.lean +++ b/Mathlib/MeasureTheory/Measure/Dirac.lean @@ -15,7 +15,7 @@ and prove some basic facts about it. -/ open Function Set -open scoped ENNReal Classical +open scoped ENNReal noncomputable section @@ -54,8 +54,9 @@ theorem dirac_apply [MeasurableSingletonClass α] (a : α) (s : Set α) : dirac a s ≤ dirac a {a}ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h) _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl] -theorem map_dirac {f : α → β} (hf : Measurable f) (a : α) : (dirac a).map f = dirac (f a) := - ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply] +theorem map_dirac {f : α → β} (hf : Measurable f) (a : α) : (dirac a).map f = dirac (f a) := by + classical + exact ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply] lemma map_const (μ : Measure α) (c : β) : μ.map (fun _ ↦ c) = (μ Set.univ) • dirac c := by ext s hs @@ -92,7 +93,8 @@ theorem sum_smul_dirac [Countable α] [MeasurableSingletonClass α] (μ : Measur /-- Given that `α` is a countable, measurable space with all singleton sets measurable, write the measure of a set `s` as the sum of the measure of `{x}` for all `x ∈ s`. -/ theorem tsum_indicator_apply_singleton [Countable α] [MeasurableSingletonClass α] (μ : Measure α) - (s : Set α) (hs : MeasurableSet s) : (∑' x : α, s.indicator (fun x => μ {x}) x) = μ s := + (s : Set α) (hs : MeasurableSet s) : (∑' x : α, s.indicator (fun x => μ {x}) x) = μ s := by + classical calc (∑' x : α, s.indicator (fun x => μ {x}) x) = Measure.sum (fun a => μ {a} • Measure.dirac a) s := by diff --git a/Mathlib/MeasureTheory/Measure/GiryMonad.lean b/Mathlib/MeasureTheory/Measure/GiryMonad.lean index 4fed1d5962387..c84c4f1258001 100644 --- a/Mathlib/MeasureTheory/Measure/GiryMonad.lean +++ b/Mathlib/MeasureTheory/Measure/GiryMonad.lean @@ -30,11 +30,7 @@ giry monad noncomputable section -open scoped Classical -open ENNReal - -open scoped Classical -open Set Filter +open ENNReal Set Filter variable {α β : Type*} diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean index 4710b819f0406..f14d89823fcd7 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean @@ -65,7 +65,7 @@ noncomputable section open Set Inv Function TopologicalSpace MeasurableSpace -open scoped NNReal Classical ENNReal Pointwise Topology +open scoped NNReal ENNReal Pointwise Topology namespace MeasureTheory @@ -159,6 +159,7 @@ theorem index_elim {K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) theorem le_index_mul (K₀ : PositiveCompacts G) (K : Compacts G) {V : Set G} (hV : (interior V).Nonempty) : index (K : Set G) V ≤ index (K : Set G) K₀ * index (K₀ : Set G) V := by + classical obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV rw [← h2s, ← h2t, mul_comm] @@ -172,7 +173,8 @@ theorem le_index_mul (K₀ : PositiveCompacts G) (K : Compacts G) {V : Set G} @[to_additive addIndex_pos] theorem index_pos (K : PositiveCompacts G) {V : Set G} (hV : (interior V).Nonempty) : 0 < index (K : Set G) V := by - unfold index; rw [Nat.sInf_def, Nat.find_pos, mem_image] + classical + rw [index, Nat.sInf_def, Nat.find_pos, mem_image] · rintro ⟨t, h1t, h2t⟩; rw [Finset.card_eq_zero] at h2t; subst h2t obtain ⟨g, hg⟩ := K.interior_nonempty show g ∈ (∅ : Set G) @@ -189,6 +191,7 @@ theorem index_mono {K K' V : Set G} (hK' : IsCompact K') (h : K ⊆ K') (hV : (i @[to_additive addIndex_union_le] theorem index_union_le (K₁ K₂ : Compacts G) {V : Set G} (hV : (interior V).Nonempty) : index (K₁.1 ∪ K₂.1) V ≤ index K₁.1 V + index K₂.1 V := by + classical rcases index_elim K₁.2 hV with ⟨s, h1s, h2s⟩ rcases index_elim K₂.2 hV with ⟨t, h1t, h2t⟩ rw [← h2s, ← h2t] @@ -202,6 +205,7 @@ theorem index_union_le (K₁ K₂ : Compacts G) {V : Set G} (hV : (interior V).N theorem index_union_eq (K₁ K₂ : Compacts G) {V : Set G} (hV : (interior V).Nonempty) (h : Disjoint (K₁.1 * V⁻¹) (K₂.1 * V⁻¹)) : index (K₁.1 ∪ K₂.1) V = index K₁.1 V + index K₂.1 V := by + classical apply le_antisymm (index_union_le K₁ K₂ hV) rcases index_elim (K₁.2.union K₂.2) hV with ⟨s, h1s, h2s⟩; rw [← h2s] have : diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean index 8c814b274bd7a..504b07f6391be 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean @@ -33,7 +33,6 @@ assert_not_exists MeasureTheory.integral noncomputable section -open scoped Classical open Set Filter MeasureTheory MeasureTheory.Measure TopologicalSpace open ENNReal (ofReal) diff --git a/Mathlib/MeasureTheory/Measure/Stieltjes.lean b/Mathlib/MeasureTheory/Measure/Stieltjes.lean index 034cb2eef717c..98968697286c0 100644 --- a/Mathlib/MeasureTheory/Measure/Stieltjes.lean +++ b/Mathlib/MeasureTheory/Measure/Stieltjes.lean @@ -24,7 +24,6 @@ a Borel measure `f.measure`. noncomputable section -open scoped Classical open Set Filter Function ENNReal NNReal Topology MeasureTheory open ENNReal (ofReal) diff --git a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean index ebde3a14cc9ac..d9b3f84d8bdb6 100644 --- a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean @@ -43,7 +43,6 @@ vector measure, signed measure, complex measure noncomputable section -open scoped Classical open NNReal ENNReal MeasureTheory namespace MeasureTheory @@ -348,6 +347,7 @@ end VectorMeasure namespace Measure +open Classical in /-- A finite measure coerced into a real function is a signed measure. -/ @[simps] def toSignedMeasure (μ : Measure α) [hμ : IsFiniteMeasure μ] : SignedMeasure α where @@ -400,6 +400,7 @@ theorem toSignedMeasure_smul (μ : Measure α) [IsFiniteMeasure μ] (r : ℝ≥0 rw [toSignedMeasure_apply_measurable hi, VectorMeasure.smul_apply, toSignedMeasure_apply_measurable hi, coe_smul, Pi.smul_apply, ENNReal.toReal_smul] +open Classical in /-- A measure is a vector measure over `ℝ≥0∞`. -/ @[simps] def toENNRealVectorMeasure (μ : Measure α) : VectorMeasure α ℝ≥0∞ where @@ -479,6 +480,7 @@ variable [MeasurableSpace α] [MeasurableSpace β] variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] variable (v : VectorMeasure α M) +open Classical in /-- The pushforward of a vector measure along a function. -/ def map (v : VectorMeasure α M) (f : α → β) : VectorMeasure β M := if hf : Measurable f then @@ -577,6 +579,7 @@ end Module end +open Classical in /-- The restriction of a vector measure on some set. -/ def restrict (v : VectorMeasure α M) (i : Set α) : VectorMeasure α M := if hi : MeasurableSet i then @@ -1090,6 +1093,7 @@ end MutuallySingular section Trim +open Classical in /-- Restriction of a vector measure onto a sub-σ-algebra. -/ @[simps] def trim {m n : MeasurableSpace α} (v : VectorMeasure α M) (hle : m ≤ n) : diff --git a/Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean b/Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean index 58fa4df15d1b2..297f126f93f2f 100644 --- a/Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean @@ -24,7 +24,7 @@ the Radon-Nikodym theorem for signed measures. noncomputable section -open scoped Classical MeasureTheory NNReal ENNReal +open scoped MeasureTheory NNReal ENNReal variable {α β : Type*} {m : MeasurableSpace α} @@ -35,6 +35,7 @@ open TopologicalSpace variable {μ ν : Measure α} variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] +open Classical in /-- Given a measure `μ` and an integrable function `f`, `μ.withDensityᵥ f` is the vector measure which maps the set `s` to `∫ₛ f ∂μ`. -/ def Measure.withDensityᵥ {m : MeasurableSpace α} (μ : Measure α) (f : α → E) : VectorMeasure α E := diff --git a/Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean b/Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean index 544d5c4b44fe7..706d7e9a7b206 100644 --- a/Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean +++ b/Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean @@ -30,7 +30,7 @@ Carathéodory-measurable, Carathéodory's criterion noncomputable section open Set Function Filter -open scoped Classical NNReal Topology ENNReal +open scoped NNReal Topology ENNReal namespace MeasureTheory namespace OuterMeasure diff --git a/Mathlib/MeasureTheory/OuterMeasure/Induced.lean b/Mathlib/MeasureTheory/OuterMeasure/Induced.lean index a6ee00bdb14c8..b18e208fe28c9 100644 --- a/Mathlib/MeasureTheory/OuterMeasure/Induced.lean +++ b/Mathlib/MeasureTheory/OuterMeasure/Induced.lean @@ -26,7 +26,7 @@ outer measure noncomputable section open Set Function Filter -open scoped Classical NNReal Topology ENNReal +open scoped NNReal Topology ENNReal namespace MeasureTheory @@ -50,6 +50,7 @@ theorem extend_eq_top {s : α} (h : ¬P s) : extend m s = ∞ := by simp [extend theorem smul_extend {R} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [NoZeroSMulDivisors R ℝ≥0∞] {c : R} (hc : c ≠ 0) : c • extend m = extend fun s h => c • m s h := by + classical ext1 s dsimp [extend] by_cases h : P s diff --git a/Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean b/Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean index 4e933f225fa38..9bdbbdf07b9ed 100644 --- a/Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean +++ b/Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean @@ -37,7 +37,7 @@ outer measure, Carathéodory-measurable, Carathéodory's criterion noncomputable section open Set Function Filter -open scoped Classical NNReal Topology ENNReal +open scoped NNReal Topology ENNReal namespace MeasureTheory namespace OuterMeasure diff --git a/Mathlib/MeasureTheory/OuterMeasure/Operations.lean b/Mathlib/MeasureTheory/OuterMeasure/Operations.lean index 0267845e31d67..7dba544ed01e3 100644 --- a/Mathlib/MeasureTheory/OuterMeasure/Operations.lean +++ b/Mathlib/MeasureTheory/OuterMeasure/Operations.lean @@ -25,7 +25,7 @@ outer measure noncomputable section open Set Function Filter -open scoped Classical NNReal Topology ENNReal +open scoped NNReal Topology ENNReal namespace MeasureTheory namespace OuterMeasure diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal.lean b/Mathlib/RingTheory/DedekindDomain/Ideal.lean index 574ecdc9e6791..0a3b51efa73ac 100644 --- a/Mathlib/RingTheory/DedekindDomain/Ideal.lean +++ b/Mathlib/RingTheory/DedekindDomain/Ideal.lean @@ -851,20 +851,19 @@ section IsDedekindDomain variable {T : Type*} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} -open scoped Classical - open Multiset UniqueFactorizationMonoid Ideal theorem prod_normalizedFactors_eq_self (hI : I ≠ ⊥) : (normalizedFactors I).prod = I := associated_iff_eq.1 (normalizedFactors_prod hI) -theorem count_le_of_ideal_ge {I J : Ideal T} (h : I ≤ J) (hI : I ≠ ⊥) (K : Ideal T) : +theorem count_le_of_ideal_ge [DecidableEq (Ideal T)] + {I J : Ideal T} (h : I ≤ J) (hI : I ≠ ⊥) (K : Ideal T) : count K (normalizedFactors J) ≤ count K (normalizedFactors I) := le_iff_count.1 ((dvd_iff_normalizedFactors_le_normalizedFactors (ne_bot_of_le_ne_bot hI h) hI).1 (dvd_iff_le.2 h)) _ -theorem sup_eq_prod_inf_factors (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : +theorem sup_eq_prod_inf_factors [DecidableEq (Ideal T)] (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod := by have H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod = normalizedFactors I ∩ normalizedFactors J := by @@ -892,21 +891,24 @@ theorem sup_eq_prod_inf_factors (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : · exact ne_bot_of_le_ne_bot hI le_sup_left · exact this -theorem irreducible_pow_sup (hI : I ≠ ⊥) (hJ : Irreducible J) (n : ℕ) : +theorem irreducible_pow_sup [DecidableEq (Ideal T)](hI : I ≠ ⊥) (hJ : Irreducible J) (n : ℕ) : J ^ n ⊔ I = J ^ min ((normalizedFactors I).count J) n := by rw [sup_eq_prod_inf_factors (pow_ne_zero n hJ.ne_zero) hI, min_comm, normalizedFactors_of_irreducible_pow hJ, normalize_eq J, replicate_inter, prod_replicate] -theorem irreducible_pow_sup_of_le (hJ : Irreducible J) (n : ℕ) (hn : ↑n ≤ multiplicity J I) : +theorem irreducible_pow_sup_of_le [DecidableRel fun (x : Ideal T) x_1 ↦ x ∣ x_1] + (hJ : Irreducible J) (n : ℕ) (hn : ↑n ≤ multiplicity J I) : J ^ n ⊔ I = J ^ n := by + classical by_cases hI : I = ⊥ · simp_all rw [irreducible_pow_sup hI hJ, min_eq_right] rwa [multiplicity_eq_count_normalizedFactors hJ hI, PartENat.coe_le_coe, normalize_eq J] at hn -theorem irreducible_pow_sup_of_ge (hI : I ≠ ⊥) (hJ : Irreducible J) (n : ℕ) - (hn : multiplicity J I ≤ n) : +theorem irreducible_pow_sup_of_ge [DecidableRel fun (x : Ideal T) x_1 ↦ x ∣ x_1] + (hI : I ≠ ⊥) (hJ : Irreducible J) (n : ℕ) (hn : multiplicity J I ≤ n) : J ^ n ⊔ I = J ^ (multiplicity J I).get (PartENat.dom_of_le_natCast hn) := by + classical rw [irreducible_pow_sup hI hJ, min_eq_left] · congr rw [← PartENat.natCast_inj, PartENat.natCast_get,