chore: remove some open Classical, part 3 (#15417)

See #15371.

Author: grunweg

Mathlib/Algebra/Order/CompleteField.lean

@@ -42,7 +42,6 @@ archimedean. We also construct the natural map from a `LinearOrderedField` to su
 reals, conditionally complete, ordered field, uniqueness
 -/
 
-
 variable {F α β γ : Type*}
 
 noncomputable section

Mathlib/Analysis/Analytic/Composition.lean

@@ -70,7 +70,7 @@ variable {𝕜 : Type*} {E F G H : Type*}
 
 open Filter List
 
-open scoped Topology Classical NNReal ENNReal
+open scoped Topology NNReal ENNReal
 
 section Topological
 

Mathlib/Analysis/Analytic/Inverse.lean

@@ -26,8 +26,7 @@ we prove that they coincide and study their properties (notably convergence).
 
 -/
 
-
-open scoped Classical Topology
+open scoped Topology
 
 open Finset Filter
 
@@ -91,6 +90,7 @@ term is invertible. -/
 theorem leftInv_comp (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F)
     (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) : (leftInv p i).comp p = id 𝕜 E := by
   ext (n v)
+  classical
   match n with
   | 0 =>
     simp only [leftInv_coeff_zero, ContinuousMultilinearMap.zero_apply, id_apply_ne_one, Ne,
@@ -192,8 +192,8 @@ theorem comp_rightInv_aux1 {n : ℕ} (hn : 0 < n) (p : FormalMultilinearSeries 
     (q : FormalMultilinearSeries 𝕜 F E) (v : Fin n → F) :
     p.comp q n v =
       ∑ c ∈ {c : Composition n | 1 < c.length}.toFinset,
-          p c.length (q.applyComposition c v) +
-        p 1 fun _ => q n v := by
+          p c.length (q.applyComposition c v) + p 1 fun _ => q n v := by
+  classical
   have A :
     (Finset.univ : Finset (Composition n)) =
       {c | 1 < Composition.length c}.toFinset ∪ {Composition.single n hn} := by

Mathlib/Analysis/Analytic/Linear.lean

@@ -17,8 +17,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCom
   [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*}
   [NormedAddCommGroup G] [NormedSpace 𝕜 G]
 
-open scoped Topology Classical NNReal ENNReal
-
+open scoped Topology NNReal ENNReal
 open Set Filter Asymptotics
 
 noncomputable section

Mathlib/Analysis/Analytic/RadiusLiminf.lean

@@ -19,7 +19,7 @@ because this would create a circular dependency once we redefine `exp` using
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
   [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 
-open scoped Topology Classical NNReal ENNReal
+open scoped Topology NNReal ENNReal
 
 open Filter Asymptotics
 

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -50,8 +50,7 @@ non-Riemann filter (e.g., Henstock-Kurzweil and McShane).
 integral
 -/
 
-
-open scoped Classical Topology NNReal Filter Uniformity BoxIntegral
+open scoped Topology NNReal Filter Uniformity BoxIntegral
 
 open Set Finset Function Filter Metric BoxIntegral.IntegrationParams
 
@@ -101,6 +100,7 @@ theorem integralSum_inf_partition (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[
     integralSum f vol (π.infPrepartition π') = integralSum f vol π :=
   integralSum_biUnion_partition f vol π _ fun _J hJ => h.restrict (Prepartition.le_of_mem _ hJ)
 
+open Classical in
 theorem integralSum_fiberwise {α} (g : Box ι → α) (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F)
     (π : TaggedPrepartition I) :
     (∑ y ∈ π.boxes.image g, integralSum f vol (π.filter (g · = y))) = integralSum f vol π :=
@@ -159,6 +159,7 @@ predicate. -/
 def Integrable (I : Box ι) (l : IntegrationParams) (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) :=
   ∃ y, HasIntegral I l f vol y
 
+open Classical in
 /-- The integral of a function `f` over a box `I` along a filter `l` w.r.t. a volume `vol`.
 Returns zero on non-integrable functions. -/
 def integral (I : Box ι) (l : IntegrationParams) (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) :=
@@ -260,8 +261,9 @@ theorem integrable_neg : Integrable I l (-f) vol ↔ Integrable I l f vol :=
   ⟨fun h => h.of_neg, fun h => h.neg⟩
 
 @[simp]
-theorem integral_neg : integral I l (-f) vol = -integral I l f vol :=
-  if h : Integrable I l f vol then h.hasIntegral.neg.integral_eq
+theorem integral_neg : integral I l (-f) vol = -integral I l f vol := by
+  classical
+  exact if h : Integrable I l f vol then h.hasIntegral.neg.integral_eq
   else by rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]
 
 theorem HasIntegral.sub (h : HasIntegral I l f vol y) (h' : HasIntegral I l g vol y') :
@@ -298,6 +300,7 @@ theorem integral_zero : integral I l (fun _ => (0 : E)) vol = 0 :=
 theorem HasIntegral.sum {α : Type*} {s : Finset α} {f : α → ℝⁿ → E} {g : α → F}
     (h : ∀ i ∈ s, HasIntegral I l (f i) vol (g i)) :
     HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i) := by
+  classical
   induction' s using Finset.induction_on with a s ha ihs; · simp [hasIntegral_zero]
   simp only [Finset.sum_insert ha]; rw [Finset.forall_mem_insert] at h
   exact h.1.add (ihs h.2)
@@ -661,6 +664,7 @@ theorem integrable_of_bounded_and_ae_continuousWithinAt [CompleteSpace E] {I : B
   let t₁ (J : Box ι) : ℝⁿ := (π₁.infPrepartition π₂.toPrepartition).tag J
   let t₂ (J : Box ι) : ℝⁿ := (π₂.infPrepartition π₁.toPrepartition).tag J
   let B := (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes
+  classical
   let B' := B.filter (fun J ↦ J.toSet ⊆ U)
   have hB' : B' ⊆ B := B.filter_subset (fun J ↦ J.toSet ⊆ U)
   have μJ_ne_top : ∀ J ∈ B, μ J ≠ ⊤ :=
@@ -777,6 +781,7 @@ theorem HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (hl : l.bRiemann =
   rcases hs.exists_pos_forall_sum_le (div_pos ε0' H0) with ⟨εs, hεs0, hεs⟩
   simp only [le_div_iff' H0, mul_sum] at hεs
   rcases exists_pos_mul_lt ε0' (B I) with ⟨ε', ε'0, hεI⟩
+  classical
   set δ : ℝ≥0 → ℝⁿ → Ioi (0 : ℝ) := fun c x => if x ∈ s then δ₁ c x (εs x) else (δ₂ c) x ε'
   refine ⟨δ, fun c => l.rCond_of_bRiemann_eq_false hl, ?_⟩
   simp only [Set.mem_iUnion, mem_inter_iff, mem_setOf_eq]

Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean

@@ -26,8 +26,7 @@ Then `p I` is true.
 rectangular box, induction
 -/
 
-
-open Set Finset Function Filter Metric Classical Topology Filter ENNReal
+open Set Function Filter Topology
 
 noncomputable section
 
@@ -37,6 +36,7 @@ namespace Box
 
 variable {ι : Type*} {I J : Box ι}
 
+open Classical in
 /-- For a box `I`, the hyperplanes passing through its center split `I` into `2 ^ card ι` boxes.
 `BoxIntegral.Box.splitCenterBox I s` is one of these boxes. See also
 `BoxIntegral.Partition.splitCenter` for the corresponding `BoxIntegral.Partition`. -/

Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean

@@ -38,8 +38,7 @@ Henstock-Kurzweil integral.
 Henstock-Kurzweil integral, integral, Stokes theorem, divergence theorem
 -/
 
-
-open scoped Classical NNReal ENNReal Topology BoxIntegral
+open scoped NNReal ENNReal Topology BoxIntegral
 
 open ContinuousLinearMap (lsmul)
 

Mathlib/Analysis/BoxIntegral/Integrability.lean

@@ -21,8 +21,7 @@ We deduce that the same is true for the Riemann integral for continuous function
 integral, McShane integral, Bochner integral
 -/
 
-
-open scoped Classical NNReal ENNReal Topology
+open scoped NNReal ENNReal Topology
 
 universe u v
 
@@ -63,6 +62,7 @@ theorem hasIntegralIndicatorConst (l : IntegrationParams) (hl : l.bRiemann = fal
       nhds_basis_closedBall.mem_iff.1 (hFc.isOpen_compl.mem_nhds fun hx' => hx.2 (hFs hx').1)
     exact ⟨⟨r, hr₀⟩, hr⟩
   choose! rs' hrs'F using this
+  classical
   set r : (ι → ℝ) → Ioi (0 : ℝ) := s.piecewise rs rs'
   refine ⟨fun _ => r, fun c => l.rCond_of_bRiemann_eq_false hl, fun c π hπ hπp => ?_⟩; rw [mul_comm]
   /- Then the union of boxes `J ∈ π` such that `π.tag ∈ s` includes `F` and is included by `U`,

Mathlib/Analysis/BoxIntegral/Partition/Measure.lean

@@ -23,12 +23,11 @@ For the last statement, we both prove it as a proposition and define a bundled
 rectangular box, measure
 -/
 
-
 open Set
 
 noncomputable section
 
-open scoped ENNReal Classical BoxIntegral
+open scoped ENNReal BoxIntegral
 
 variable {ι : Type*}
 

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -32,10 +32,9 @@ In this file, we denote `⊤ : ℕ∞` with `∞`.
 derivative, differentiability, higher derivative, `C^n`, multilinear, Taylor series, formal series
 -/
 
-
 noncomputable section
 
-open scoped Classical NNReal Nat
+open scoped NNReal Nat
 
 local notation "∞" => (⊤ : ℕ∞)
 

Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

@@ -18,7 +18,7 @@ import Mathlib.Data.Nat.Choose.Multinomial
 
 noncomputable section
 
-open scoped Classical NNReal Nat
+open scoped NNReal Nat
 
 universe u uD uE uF uG
 

Mathlib/Analysis/Calculus/Deriv/Basic.lean

@@ -90,8 +90,7 @@ universe u v w
 
 noncomputable section
 
-open scoped Classical Topology Filter ENNReal NNReal
-
+open scoped Topology ENNReal NNReal
 open Filter Asymptotics Set
 
 open ContinuousLinearMap (smulRight smulRight_one_eq_iff)

Mathlib/Analysis/Calculus/Deriv/Mul.lean

@@ -20,12 +20,11 @@ For a more detailed overview of one-dimensional derivatives in mathlib, see the
 derivative, multiplication
 -/
 
-
 universe u v w
 
 noncomputable section
 
-open scoped Classical Topology Filter ENNReal
+open scoped Topology Filter ENNReal
 
 open Filter Asymptotics Set
 
@@ -326,12 +325,15 @@ variable {ι : Type*} {𝔸' : Type*} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜
   {u : Finset ι} {f : ι → 𝕜 → 𝔸'} {f' : ι → 𝔸'}
 
 theorem DifferentiableAt.finset_prod (hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) :
-    DifferentiableAt 𝕜 (∏ i ∈ u, f i ·) x :=
-  (HasDerivAt.finset_prod (fun i hi ↦ DifferentiableAt.hasDerivAt (hd i hi))).differentiableAt
+    DifferentiableAt 𝕜 (∏ i ∈ u, f i ·) x := by
+  classical
+  exact
+    (HasDerivAt.finset_prod (fun i hi ↦ DifferentiableAt.hasDerivAt (hd i hi))).differentiableAt
 
 theorem DifferentiableWithinAt.finset_prod (hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) :
-    DifferentiableWithinAt 𝕜 (∏ i ∈ u, f i ·) s x :=
-  (HasDerivWithinAt.finset_prod (fun i hi ↦
+    DifferentiableWithinAt 𝕜 (∏ i ∈ u, f i ·) s x := by
+  classical
+  exact (HasDerivWithinAt.finset_prod (fun i hi ↦
     DifferentiableWithinAt.hasDerivWithinAt (hd i hi))).differentiableWithinAt
 
 theorem DifferentiableOn.finset_prod (hd : ∀ i ∈ u, DifferentiableOn 𝕜 (f i) s) :

Mathlib/Analysis/Calculus/Deriv/Polynomial.lean

@@ -30,9 +30,8 @@ derivative, polynomial
 
 universe u v w
 
-open scoped Classical Topology Filter ENNReal Polynomial
-
-open Filter Asymptotics Set
+open scoped Topology Filter ENNReal Polynomial
+open Set
 
 open ContinuousLinearMap (smulRight smulRight_one_eq_iff)
 

Mathlib/Analysis/Calculus/Dslope.lean

@@ -17,26 +17,28 @@ In this file we define `dslope` and prove some basic lemmas about its continuity
 differentiability.
 -/
 
-
-open scoped Classical Topology Filter
+open scoped Topology Filter
 
 open Function Set Filter
 
 variable {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 
+open Classical in
 /-- `dslope f a b` is defined as `slope f a b = (b - a)⁻¹ • (f b - f a)` for `a ≠ b` and
 `deriv f a` for `a = b`. -/
 noncomputable def dslope (f : 𝕜 → E) (a : 𝕜) : 𝕜 → E :=
   update (slope f a) a (deriv f a)
 
 @[simp]
-theorem dslope_same (f : 𝕜 → E) (a : 𝕜) : dslope f a a = deriv f a :=
-  update_same _ _ _
+theorem dslope_same (f : 𝕜 → E) (a : 𝕜) : dslope f a a = deriv f a := by
+  classical
+  exact update_same _ _ _
 
 variable {f : 𝕜 → E} {a b : 𝕜} {s : Set 𝕜}
 
-theorem dslope_of_ne (f : 𝕜 → E) (h : b ≠ a) : dslope f a b = slope f a b :=
-  update_noteq h _ _
+theorem dslope_of_ne (f : 𝕜 → E) (h : b ≠ a) : dslope f a b = slope f a b := by
+  classical
+  exact update_noteq h _ _
 
 theorem ContinuousLinearMap.dslope_comp {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
     (f : E →L[𝕜] F) (g : 𝕜 → E) (a b : 𝕜) (H : a = b → DifferentiableAt 𝕜 g a) :
@@ -89,6 +91,7 @@ theorem ContinuousOn.of_dslope (h : ContinuousOn (dslope f a) s) : ContinuousOn
 theorem continuousWithinAt_dslope_of_ne (h : b ≠ a) :
     ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b := by
   refine ⟨ContinuousWithinAt.of_dslope, fun hc => ?_⟩
+  classical
   simp only [dslope, continuousWithinAt_update_of_ne h]
   exact ((continuousWithinAt_id.sub continuousWithinAt_const).inv₀ (sub_ne_zero.2 h)).smul
     (hc.sub continuousWithinAt_const)

Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

@@ -45,7 +45,7 @@ We introduce some `local notation` to make formulas shorter:
 
 open Function Set Filter Metric
 
-open scoped Topology Classical NNReal
+open scoped Topology NNReal
 
 noncomputable section
 

Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean

@@ -40,7 +40,7 @@ derivative, strictly differentiable, continuously differentiable, smooth, invers
 
 open Function Set Filter Metric
 
-open scoped Topology Classical NNReal
+open scoped Topology NNReal
 
 noncomputable section
 

Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

@@ -40,11 +40,9 @@ by translating the corresponding result `iteratedFDerivWithin_succ_apply_left` f
 iterated Fréchet derivative.
 -/
 
-
 noncomputable section
 
-open scoped Classical Topology
-
+open scoped Topology
 open Filter Asymptotics Set
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]