leanprover-community · felixpernegger · Jul 9, 2026 · Jul 9, 2026
diff --git a/Mathlib/Algebra/GroupWithZero/Range.lean b/Mathlib/Algebra/GroupWithZero/Range.lean
@@ -172,7 +172,7 @@ end ValueGroup₀
 
 end Restrict
 
-noncomputable section GroupWithZero
+section GroupWithZero
 
 variable [GroupWithZero A] [GroupWithZero B] {f : A →*₀ B}
 

diff --git a/Mathlib/Algebra/MvPolynomial/Coeff.lean b/Mathlib/Algebra/MvPolynomial/Coeff.lean
@@ -19,8 +19,6 @@ public import Mathlib.Data.Nat.Choose.Multinomial
 
 public section
 
-noncomputable section
-
 namespace MvPolynomial
 
 open Finsupp

diff --git a/Mathlib/Algebra/Polynomial/Degree/Domain.lean b/Mathlib/Algebra/Polynomial/Degree/Domain.lean
@@ -18,8 +18,6 @@ public import Mathlib.Algebra.Polynomial.Degree.Operations
 
 public section
 
-noncomputable section
-
 open Finsupp Finset
 
 open Polynomial

diff --git a/Mathlib/Algebra/Polynomial/Degree/Lemmas.lean b/Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
@@ -19,8 +19,6 @@ Some of the main results include
 public section
 
 
-noncomputable section
-
 open Polynomial
 
 open Finsupp Finset

diff --git a/Mathlib/Algebra/Polynomial/Degree/Monomial.lean b/Mathlib/Algebra/Polynomial/Degree/Monomial.lean
@@ -15,8 +15,6 @@ public import Mathlib.Data.Nat.SuccPred
 
 public section
 
-noncomputable section
-
 open Finsupp Finset Polynomial
 
 namespace Polynomial

diff --git a/Mathlib/Algebra/Polynomial/Degree/Support.lean b/Mathlib/Algebra/Polynomial/Degree/Support.lean
@@ -19,8 +19,6 @@ public import Mathlib.Algebra.Polynomial.Degree.Operations
 
 public section
 
-noncomputable section
-
 open Finsupp Finset
 
 open Polynomial

diff --git a/Mathlib/Algebra/Polynomial/Degree/Units.lean b/Mathlib/Algebra/Polynomial/Degree/Units.lean
@@ -14,8 +14,6 @@ public import Mathlib.Algebra.Polynomial.Degree.SmallDegree
 
 public section
 
-noncomputable section
-
 open Finsupp Finset Polynomial
 
 namespace Polynomial

diff --git a/Mathlib/Algebra/Polynomial/Eval/Algebra.lean b/Mathlib/Algebra/Polynomial/Eval/Algebra.lean
@@ -18,8 +18,6 @@ TODO: merge with parts of `Mathlib/Algebra/Polynomial/AlgebraMap.lean`?
 
 public section
 
-noncomputable section
-
 open Finset AddMonoidAlgebra
 
 open Polynomial

diff --git a/Mathlib/Algebra/Polynomial/Eval/Irreducible.lean b/Mathlib/Algebra/Polynomial/Eval/Irreducible.lean
@@ -20,8 +20,6 @@ public import Mathlib.Algebra.Prime.Defs
 
 public section
 
-noncomputable section
-
 open Finset AddMonoidAlgebra
 
 open Polynomial

diff --git a/Mathlib/Algebra/Polynomial/Splits.lean b/Mathlib/Algebra/Polynomial/Splits.lean
@@ -696,8 +696,6 @@ theorem splits_iff_splits {f : R[X]} :
 
 end Field
 
-noncomputable section
-
 open Polynomial
 
 universe u v w
@@ -954,6 +952,4 @@ alias nextCoeff_eq_neg_sum_roots_of_monic_of_splits := Splits.nextCoeff_eq_neg_s
 
 end Splits
 
-end
-
 end Polynomial
diff --git a/Mathlib/Analysis/Analytic/Within.lean b/Mathlib/Analysis/Analytic/Within.lean
@@ -25,8 +25,6 @@ ambient space, which allows us to relate `AnalyticWithinAt` to analyticity of a
 
 public section
 
-noncomputable section
-
 open scoped Topology Filter ENNReal
 open Set Filter Metric
 

diff --git a/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean b/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean
@@ -50,8 +50,6 @@ open Filter Set Finset Metric
 
 open BoxIntegral.IntegrationParams (GP gp_le)
 
-noncomputable section
-
 universe u
 
 variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ}

diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean
@@ -19,7 +19,7 @@ constants, products, composition with linear maps, etc.
 derivative, differentiability, higher derivative, `C^n`, multilinear, Taylor series, formal series
 -/
 
-public noncomputable section
+public section
 
 open Set Fin Filter Function
 

diff --git a/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean b/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
@@ -20,8 +20,6 @@ public import Mathlib.Data.Nat.Choose.Multinomial
 
 public section
 
-noncomputable section
-
 open scoped NNReal Nat ContDiff
 
 universe u uD uE uF uG

diff --git a/Mathlib/Analysis/Calculus/ContDiff/Comp.lean b/Mathlib/Analysis/Calculus/ContDiff/Comp.lean
@@ -33,7 +33,7 @@ In this file, we denote `WithTop ℕ∞` with `ℕ∞ω`, `(⊤ : ℕ∞) : ℕ
 derivative, differentiability, higher derivative, `C^n`, multilinear, Taylor series, formal series
 -/
 
-public noncomputable section
+public section
 
 open Set Filter Function
 

diff --git a/Mathlib/Analysis/Calculus/ContDiff/Deriv.lean b/Mathlib/Analysis/Calculus/ContDiff/Deriv.lean
@@ -19,7 +19,7 @@ to use. In this file, we reformulate some higher smoothness results in terms of
 derivative, differentiability, higher derivative, `C^n`, multilinear, Taylor series, formal series
 -/
 
-public noncomputable section
+public section
 
 open scoped ContDiff
 

diff --git a/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean b/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean
@@ -16,8 +16,6 @@ public import Mathlib.Analysis.Normed.Module.FiniteDimension
 public section
 
 
-noncomputable section
-
 universe uD uE uF
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

diff --git a/Mathlib/Analysis/Calculus/ContDiff/RCLike.lean b/Mathlib/Analysis/Calculus/ContDiff/RCLike.lean
@@ -14,8 +14,6 @@ public import Mathlib.Analysis.Calculus.MeanValue
 
 public section
 
-noncomputable section
-
 open Set Fin Filter Function
 
 open scoped NNReal Topology

diff --git a/Mathlib/Analysis/Calculus/Deriv/Mul.lean b/Mathlib/Analysis/Calculus/Deriv/Mul.lean
@@ -27,8 +27,6 @@ public section
 
 universe u v w
 
-noncomputable section
-
 open scoped Topology Filter ENNReal
 
 open Filter Asymptotics Set

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Add.lean b/Mathlib/Analysis/Calculus/FDeriv/Add.lean
@@ -28,8 +28,6 @@ public section
 
 open Filter Asymptotics ContinuousLinearMap
 
-noncomputable section
-
 section
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
@@ -111,8 +111,6 @@ public section
 
 open Filter Asymptotics ContinuousLinearMap Set Metric Topology NNReal ENNReal
 
-noncomputable section
-
 section
 section DerivativeUniqueness
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean b/Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean
@@ -22,8 +22,6 @@ public section
 
 open Asymptotics Topology
 
-noncomputable section
-
 section
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Comp.lean b/Mathlib/Analysis/Calculus/FDeriv/Comp.lean
@@ -22,8 +22,6 @@ public section
 
 open Filter Asymptotics ContinuousLinearMap Set Metric Topology NNReal ENNReal
 
-noncomputable section
-
 section
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Congr.lean b/Mathlib/Analysis/Calculus/FDeriv/Congr.lean
@@ -22,8 +22,6 @@ public section
 
 open Filter Asymptotics ContinuousLinearMap Set Metric Topology NNReal ENNReal
 
-noncomputable section
-
 section
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 variable {E : Type*} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Const.lean b/Mathlib/Analysis/Calculus/FDeriv/Const.lean
@@ -25,8 +25,6 @@ public section
 open Asymptotics Function Filter Set Metric
 open scoped Topology NNReal ENNReal
 
-noncomputable section
-
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 variable {E : Type*} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
 variable {F : Type*} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
@@ -394,6 +392,3 @@ protected theorem HasCompactSupport.fderiv_apply (hf : HasCompactSupport f) (v :
   hf.of_isClosed_subset (isClosed_tsupport _) (tsupport_fderiv_apply_subset 𝕜 v)
 
 end Support
-
-
-end
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean b/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
@@ -26,8 +26,6 @@ public section
 
 open Filter Asymptotics ContinuousLinearMap Set Metric Topology NNReal ENNReal
 
-noncomputable section
-
 section
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Prod.lean b/Mathlib/Analysis/Calculus/FDeriv/Prod.lean
@@ -24,8 +24,6 @@ public section
 
 open Filter Asymptotics ContinuousLinearMap Set Metric Topology NNReal ENNReal
 
-noncomputable section
-
 section
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

diff --git a/Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.lean b/Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.lean
@@ -22,8 +22,6 @@ public section
 
 open Filter Asymptotics ContinuousLinearMap Set Metric Topology NNReal ENNReal
 
-noncomputable section
-
 section RestrictScalars
 
 /-!

diff --git a/Mathlib/Analysis/Calculus/ParametricIntegral.lean b/Mathlib/Analysis/Calculus/ParametricIntegral.lean
@@ -58,8 +58,6 @@ integral, derivative
 public section
 
 
-noncomputable section
-
 open TopologicalSpace MeasureTheory Filter Metric
 
 open scoped Topology Filter

diff --git a/Mathlib/Analysis/Complex/CauchyIntegral.lean b/Mathlib/Analysis/Complex/CauchyIntegral.lean
@@ -164,8 +164,6 @@ open TopologicalSpace Set MeasureTheory intervalIntegral Metric Filter Function
 
 open scoped Interval Real NNReal ENNReal Topology
 
-noncomputable section
-
 universe u
 
 variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E]

diff --git a/Mathlib/Analysis/Complex/ReImTopology.lean b/Mathlib/Analysis/Complex/ReImTopology.lean
@@ -37,8 +37,6 @@ public section
 
 open Set Topology
 
-noncomputable section
-
 namespace Complex
 
 /-- `Complex.re` turns `ℂ` into a trivial topological fiber bundle over `ℝ`. -/

diff --git a/Mathlib/Analysis/Fourier/PoissonSummation.lean b/Mathlib/Analysis/Fourier/PoissonSummation.lean
@@ -30,8 +30,6 @@ easier-to-use result `Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay`, in which
 public section
 
 
-noncomputable section
-
 open Function hiding comp_apply
 
 open Set hiding restrict_apply

diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
@@ -45,8 +45,6 @@ equivalence to an inner-product space.
 
 public section
 
-noncomputable section
-
 open MeasureTheory Filter Complex Set Module
 
 open scoped Filter Topology Real ENNReal FourierTransform RealInnerProductSpace NNReal

diff --git a/Mathlib/Analysis/InnerProductSpace/Continuous.lean b/Mathlib/Analysis/InnerProductSpace/Continuous.lean
@@ -21,8 +21,6 @@ inner product space, Hilbert space, norm
 
 public section
 
-noncomputable section
-
 open RCLike Real Filter Topology ComplexConjugate Finsupp
 open LinearMap renaming BilinForm → BilinForm
 

diff --git a/Mathlib/Analysis/MeanInequalities.lean b/Mathlib/Analysis/MeanInequalities.lean
@@ -114,8 +114,6 @@ universe u v
 open Finset NNReal ENNReal
 open scoped BigOperators
 
-noncomputable section
-
 variable {ι : Type u} (s : Finset ι)
 
 section GeomMeanLEArithMean

diff --git a/Mathlib/Analysis/Normed/Module/Dual.lean b/Mathlib/Analysis/Normed/Module/Dual.lean
@@ -35,8 +35,6 @@ strong dual, polar
 
 public section
 
-noncomputable section
-
 open Topology Bornology
 
 namespace NormedSpace

diff --git a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
@@ -25,8 +25,6 @@ public section
 
 assert_not_exists IsConformalMap Conformal
 
-noncomputable section
-
 open Filter Asymptotics Set Function
 open scoped Topology
 

diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean
@@ -29,8 +29,6 @@ Gamma
 public section
 
 
-noncomputable section
-
 open Filter Set Real Asymptotics
 open scoped Topology
 

diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
@@ -23,8 +23,6 @@ We prove various versions of the formula for the Gaussian integral:
 
 public section
 
-noncomputable section
-
 open Real Set MeasureTheory Filter Asymptotics
 
 open scoped Real Topology

diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
@@ -29,8 +29,6 @@ open scoped Real Topology FourierTransform RealInnerProductSpace
 
 open Complex hiding exp continuous_exp
 
-noncomputable section
-
 section GaussianPoisson
 
 /-! First we show that Gaussian-type functions have rapid decay along `cocompact ℝ`. -/

diff --git a/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean b/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
@@ -30,8 +30,6 @@ than the dimension.
 public section
 
 
-noncomputable section
-
 open scoped NNReal Filter Topology ENNReal
 
 open Asymptotics Filter Set Real MeasureTheory Module

diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean b/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
@@ -26,8 +26,6 @@ open Set Filter Function
 
 open Topology
 
-noncomputable section
-
 namespace Real
 
 theorem mul_log_strictMonoOn : StrictMonoOn (fun x ↦ x * log x) <| .Ici <| exp (-1) := by
-Original file line number
+Diff line change
@@ Expand Up / @@ -28,8 +28,6 @@ public section @@
     open Filter Asymptotics ContinuousLinearMap
-    noncomputable section
     section
     variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
@@ Expand Down @@