leanprover-community · adomani · Jan 16, 2026 · Ruben-VandeVelde · Jan 16, 2026 · adomani
diff --git a/Mathlib/Algebra/Category/AlgCat/Monoidal.lean b/Mathlib/Algebra/Category/AlgCat/Monoidal.lean
@@ -43,8 +43,6 @@ noncomputable abbrev tensorHom {W X Y Z : AlgCat.{u} R} (f : W ⟶ X) (g : Y ⟶
     tensorObj W Y ⟶ tensorObj X Z :=
   ofHom <| Algebra.TensorProduct.map f.hom g.hom
 
-open MonoidalCategory
-
 end instMonoidalCategory
 
 open instMonoidalCategory

diff --git a/Mathlib/Algebra/Group/Equiv/Basic.lean b/Mathlib/Algebra/Group/Equiv/Basic.lean
@@ -28,11 +28,6 @@ open Function
 
 variable {F α β M M₁ M₂ M₃ N N₁ N₂ N₃ P Q G H : Type*}
 
-namespace EmbeddingLike
-variable [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N]
-
-end EmbeddingLike
-
 variable [EquivLike F α β]
 
 @[to_additive]

diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean
@@ -340,39 +340,13 @@ theorem op_smul_finset_smul_eq_smul_smul_finset (a : α) (s : Finset β) (t : Fi
 
 end SMul
 
-
-section IsRightCancelMul
-
-variable [Mul α] [IsRightCancelMul α] [DecidableEq α] {s t : Finset α} {a : α}
-
-
-end IsRightCancelMul
-
-section CancelMonoid
-variable [DecidableEq α] [CancelMonoid α] {s : Finset α} {m n : ℕ}
-
-
-end CancelMonoid
-
-section Group
-variable [Group α] [DecidableEq α] {s t : Finset α}
-
-
-end Group
-
 @[to_additive]
 theorem image_smul_comm [DecidableEq β] [DecidableEq γ] [SMul α β] [SMul α γ] (f : β → γ) (a : α)
     (s : Finset β) : (∀ b, f (a • b) = a • f b) → (a • s).image f = a • s.image f :=
   image_comm
 
 end Finset
 
-namespace Fintype
-variable {ι : Type*} {α β : ι → Type*} [Fintype ι] [DecidableEq ι] [∀ i, DecidableEq (β i)]
-  [∀ i, DecidableEq (α i)]
-
-end Fintype
-
 open Pointwise
 
 namespace Set

diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean
@@ -403,8 +403,6 @@ theorem _root_.normalizerCondition_iff_only_full_group_self_normalizing :
   simp only [lt_iff_le_and_ne, le_normalizer, le_top, Ne]
   tauto
 
-variable (H)
-
 end Normalizer
 
 end Subgroup

diff --git a/Mathlib/Algebra/Group/Submonoid/Membership.lean b/Mathlib/Algebra/Group/Submonoid/Membership.lean
@@ -42,12 +42,6 @@ assert_not_exists MonoidWithZero
 
 variable {M A B : Type*}
 
-section Assoc
-
-variable [Monoid M] [SetLike B M] [SubmonoidClass B M] {S : B}
-
-end Assoc
-
 section NonAssoc
 
 variable [MulOneClass M]

diff --git a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean
@@ -133,8 +133,6 @@ theorem inverse_zero : inverse (0 : M₀) = 0 := by
   nontriviality
   exact inverse_non_unit _ not_isUnit_zero
 
-variable {M₀}
-
 end Ring
 
 theorem IsUnit.ringInverse {a : M₀} : IsUnit a → IsUnit (Ring.inverse a)

diff --git a/Mathlib/Algebra/Module/RingHom.lean b/Mathlib/Algebra/Module/RingHom.lean
@@ -63,8 +63,6 @@ abbrev Module.compHom [Semiring S] (f : S →+* R) : Module S M :=
     -- TODO(jmc): there should be a rw-lemma `smul_comp` close to `SMulZeroClass.compFun`
     add_smul := fun r s x => show f (r + s) • x = f r • x + f s • x by simp [add_smul] }
 
-variable {M}
-
 end AddCommMonoid
 
 /-- A ring homomorphism `f : R →+* M` defines a module structure by `r • x = f r * x`.

diff --git a/Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean b/Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean
@@ -1344,8 +1344,6 @@ lemma zpow_lt_zpow_iff_left₀ (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : 0 < n) : a ^
 
 end MulPosMono
 
-variable [MulPosStrictMono G₀]
-
 end GroupWithZero.LinearOrder
 
 section CommGroupWithZero

diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean
@@ -1216,8 +1216,6 @@ lemma specTargetImageFactorization_comp :
     specTargetImageFactorization f ≫ Spec.map (specTargetImageRingHom f) = f :=
   f.liftQuotient_comp _ _
 
-open RingHom
-
 end Factorization
 
 section Stalks

diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean b/Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean
@@ -399,8 +399,6 @@ instance : hoFunctor₂.{u}.Monoidal :=
 instance hoFunctor.monoidal : hoFunctor.{u}.Monoidal :=
   inferInstanceAs (truncation 2 ⋙ hoFunctor₂).Monoidal
 
-open MonoidalCategory
-
 end Truncated
 
 /-- An equivalence between the vertices of a simplicial set `X` and the

diff --git a/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean b/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
@@ -187,8 +187,6 @@ theorem superpolynomialDecay_const_mul_iff [ContinuousMul β] {c : β} (hc0 : c
   ⟨fun h => (h.const_mul c⁻¹).congr fun x => by simp [← mul_assoc, inv_mul_cancel₀ hc0], fun h =>
     h.const_mul c⟩
 
-variable {l k f}
-
 end Field
 
 section LinearOrderedField
@@ -272,8 +270,6 @@ theorem superpolynomialDecay_mul_param_pow_iff (hk : Tendsto k l atTop) (n : ℕ
     SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f := by
   simpa [mul_comm f] using superpolynomialDecay_param_pow_mul_iff f hk n
 
-variable {f}
-
 end LinearOrderedField
 
 section NormedLinearOrderedField

diff --git a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
@@ -459,8 +459,6 @@ theorem y_support {D : ℝ} (Dpos : 0 < D) (D_lt_one : D < 1) :
     ⟨fun _ hx => (y_pos_of_mem_ball Dpos D_lt_one hx).ne', fun _ hx =>
       y_eq_zero_of_notMem_ball Dpos hx⟩
 
-variable {E}
-
 end HelperDefinitions
 
 instance (priority := 100) {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

diff --git a/Mathlib/Analysis/Calculus/LineDeriv/Basic.lean b/Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
@@ -451,8 +451,6 @@ theorem norm_lineDeriv_le_of_lipschitz {f : E → F} {x₀ : E}
     {C : ℝ≥0} (hlip : LipschitzWith C f) : ‖lineDeriv 𝕜 f x₀ v‖ ≤ C * ‖v‖ :=
   norm_lineDeriv_le_of_lipschitzOn 𝕜 univ_mem (lipschitzOnWith_univ.2 hlip)
 
-variable {𝕜}
-
 end NormedSpace
 
 section Zero

diff --git a/Mathlib/Analysis/Convex/Cone/InnerDual.lean b/Mathlib/Analysis/Convex/Cone/InnerDual.lean
@@ -186,11 +186,6 @@ theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_notMem (K :
       _ = ⟪b - z, b - z + z⟫_ℝ := (inner_add_right _ _ _).symm
       _ = ⟪b - z, b⟫_ℝ := by rw [sub_add_cancel]
 
-namespace ProperCone
-variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
-
-end ProperCone
-
 end CompleteSpace
 
 end Dual
diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean
@@ -1227,8 +1227,6 @@ theorem toBoundedContinuousFunctionCLM_apply (f : 𝓢(E, F)) (x : E) :
     toBoundedContinuousFunctionCLM 𝕜 E F f x = f x :=
   rfl
 
-variable {E}
-
 end BoundedContinuousFunction
 
 section ZeroAtInfty

diff --git a/Mathlib/Analysis/Normed/Module/Alternating/Basic.lean b/Mathlib/Analysis/Normed/Module/Alternating/Basic.lean
@@ -365,8 +365,6 @@ def restrictScalarsLI : E [⋀^ι]→L[𝕜] F →ₗᵢ[𝕜'] E [⋀^ι]→L[
   map_smul' _ _ := rfl
   norm_map' _ := rfl
 
-variable {𝕜'}
-
 end restrictScalars
 
 /-- The difference `f m₁ - f m₂` is controlled in terms of `‖f‖` and `‖m₁ - m₂‖`, precise version.

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
@@ -334,12 +334,6 @@ theorem InitialMonoClass.of_isTerminal {I T : C} (hI : IsInitial I) (hT : IsTerm
     (_ : Mono (hI.to T)) : InitialMonoClass C :=
   InitialMonoClass.of_isInitial hI fun X => mono_of_mono_fac (hI.hom_ext (_ ≫ hT.from X) (hI.to T))
 
-section Comparison
-
-variable {D : Type u₂} [Category.{v₂} D] (G : C ⥤ D)
-
-end Comparison
-
 variable {J : Type u} [Category.{v} J]
 
 /-- From a functor `F : J ⥤ C`, given an initial object of `J`, construct a cone for `J`.

diff --git a/Mathlib/CategoryTheory/Noetherian.lean b/Mathlib/CategoryTheory/Noetherian.lean
@@ -45,6 +45,4 @@ class Artinian : Prop extends EssentiallySmall C where
 
 attribute [instance] Artinian.isArtinianObject
 
-open Subobject
-
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Sites/Canonical.lean b/Mathlib/CategoryTheory/Sites/Canonical.lean
@@ -229,8 +229,6 @@ theorem isSheaf_of_isRepresentable {J : GrothendieckTopology C} [Subcanonical J]
     (P : Cᵒᵖ ⥤ Type v) [P.IsRepresentable] : Presieve.IsSheaf J P :=
   Presieve.isSheaf_of_le _ J.le_canonical (Sheaf.isSheaf_of_isRepresentable P)
 
-variable {J : GrothendieckTopology C}
-
 end Subcanonical
 
 variable (J : GrothendieckTopology C)

diff --git a/Mathlib/Control/LawfulFix.lean b/Mathlib/Control/LawfulFix.lean
@@ -165,8 +165,6 @@ theorem fix_eq_of_ωScottContinuous (hc : ωScottContinuous g) :
     intro i
     exists i.succ
 
-variable {f}
-
 end Part
 
 namespace Part

diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean
@@ -157,12 +157,6 @@ end Diag
 
 open Matrix
 
-section AddCommMonoid
-
-variable [AddCommMonoid α] [Mul α]
-
-end AddCommMonoid
-
 section NonAssocSemiring
 
 variable [NonAssocSemiring α]

diff --git a/Mathlib/Data/Matrix/Mul.lean b/Mathlib/Data/Matrix/Mul.lean
@@ -472,8 +472,6 @@ theorem op_smul_one_eq_diagonal [DecidableEq m] (a : α) :
     MulOpposite.op a • (1 : Matrix m m α) = diagonal fun _ => a := by
   simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, op_smul_eq_mul, one_mul]
 
-variable (α n)
-
 end NonAssocSemiring
 
 section NonUnitalSemiring
@@ -1152,8 +1150,6 @@ theorem transpose_mul [AddCommMonoid α] [CommMagma α] [Fintype n] (M : Matrix
   ext
   apply dotProduct_comm
 
-variable (m n α)
-
 end Transpose
 
 theorem submatrix_mul [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p q : Type*}

diff --git a/Mathlib/Data/Tree/RBMap.lean b/Mathlib/Data/Tree/RBMap.lean
@@ -21,13 +21,3 @@ Implement a `Traversable` instance for `Tree`.
 
 <https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html>
 -/
-
-public section
-
-namespace Tree
-
-universe u
-
-variable {α : Type u}
-
-end Tree
diff --git a/Mathlib/GroupTheory/Congruence/Defs.lean b/Mathlib/GroupTheory/Congruence/Defs.lean
@@ -505,12 +505,6 @@ theorem comap_rel {f : M → N} (H : ∀ x y, f (x * y) = f x * f y) {c : Con N}
     comap f H c x y ↔ c (f x) (f y) :=
   Iff.rfl
 
-section
-
-open Quotient
-
-end
-
 end
 
 section MulOneClass

diff --git a/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean b/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean
@@ -155,8 +155,6 @@ variable (K V)
 instance finiteDimensional_bot : FiniteDimensional K (⊥ : Submodule K V) :=
   .of_rank_eq_zero <| by simp
 
-variable {K V}
-
 end ZeroRank
 
 namespace Submodule

diff --git a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean
@@ -53,8 +53,6 @@ abbrev tensorHom {W X Y Z : QuadraticModuleCat.{u} R} (f : W ⟶ X) (g : Y ⟶ Z
     tensorObj W Y ⟶ tensorObj X Z :=
   ⟨f.toIsometry.tmul g.toIsometry⟩
 
-open MonoidalCategory
-
 end instMonoidalCategory
 
 open instMonoidalCategory

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
@@ -316,8 +316,6 @@ def tprod (n : ℕ) : MultilinearMap R (fun _ : Fin n => M) (TensorAlgebra R M)
 theorem tprod_apply {n : ℕ} (x : Fin n → M) : tprod R M n x = (List.ofFn fun i => ι R (x i)).prod :=
   rfl
 
-variable {R M}
-
 end TensorAlgebra
 
 namespace FreeAlgebra

diff --git a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
@@ -115,8 +115,6 @@ theorem ae_eq_zero_of_forall_dual [NormedAddCommGroup E] [NormedSpace 𝕜 E]
   ae_eq_zero_of_forall_dual_of_isSeparable 𝕜 (.of_separableSpace Set.univ) hf
     (Eventually.of_forall fun _ => Set.mem_univ _)
 
-variable {𝕜}
-
 end AeEqOfForall
 
 variable {α E : Type*} {m m0 : MeasurableSpace α} {μ : Measure α}

diff --git a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
@@ -695,8 +695,6 @@ def coeToLp : Lp.simpleFunc E p μ →L[𝕜] Lp E p μ :=
     map_smul' := fun _ _ => rfl
     cont := Lp.simpleFunc.uniformContinuous.continuous }
 
-variable {α E 𝕜}
-
 end CoeToLp
 
 section Order
@@ -789,8 +787,6 @@ theorem denseRange_coeSimpleFuncNonnegToLpNonneg [hp : Fact (1 ≤ p)] (hp_ne_to
     exact h_toLp n
   · rfl
 
-variable {p μ G}
-
 end Order
 
 end simpleFunc

diff --git a/Mathlib/MeasureTheory/Integral/Prod.lean b/Mathlib/MeasureTheory/Integral/Prod.lean
@@ -162,8 +162,6 @@ theorem integrable_measure_prodMk_left {s : Set (α × β)} (hs : MeasurableSet
 
 end Measure
 
-open Measure
-
 end MeasureTheory
 
 open MeasureTheory.Measure

diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
@@ -321,12 +321,13 @@ end Valuation
 
 end PadicSeq
 
+-- Porting note: Commented out `padic_index_simp` tactic
+
+/-
 section
 
 open PadicSeq
 
--- Porting note: Commented out `padic_index_simp` tactic
-/-
 private unsafe def index_simp_core (hh hf hg : expr)
     (at_ : Interactive.Loc := Interactive.Loc.ns [none]) : tactic Unit := do
   let [v1, v2, v3] ← [hh, hf, hg].mapM fun n => tactic.mk_app `` stationary_point [n] <|> return n
@@ -344,9 +345,9 @@ unsafe def tactic.interactive.padic_index_simp (l : interactive.parse interactiv
     (at_ : interactive.parse interactive.types.location) : tactic Unit := do
   let [h, f, g] ← l.mapM tactic.i_to_expr
   index_simp_core h f g at_
--/
 
 end
+-/
 
 namespace PadicSeq
 

diff --git a/Mathlib/Order/Filter/AtTopBot/Monoid.lean b/Mathlib/Order/Filter/AtTopBot/Monoid.lean
@@ -171,11 +171,4 @@ theorem Tendsto.atBot_of_mul_const_le (hg : ∃ C, ∀ x, C ≤ g x)
 
 end OrderedCancelCommMonoid
 
-section OrderedCancelAddCommMonoid
-
-variable [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M]
-  {l : Filter α} {f g : α → M}
-
-end OrderedCancelAddCommMonoid
-
 end Filter
Original file line number	Diff line number	Diff line change
Expand Up		@@ -45,6 +45,4 @@ class Artinian : Prop extends EssentiallySmall C where

		attribute [instance] Artinian.isArtinianObject

		open Subobject

		end CategoryTheory
-Original file line number
+Diff line change
@@ Expand Up @@
         comap f H c x y ↔ c (f x) (f y) :=
       Iff.rfl
-    section
-    open Quotient
-    end
     end
     section MulOneClass
@@ Expand Down @@