diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index fc70789451..ba357fab91 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/src/lake/Lake/Build/Common.lean
@@ -54,7 +54,6 @@ and will be rebuilt on different host platforms.
   [ToString α] [ComputeHash α Id] (a : α) (caption := "pure")
 : JobM PUnit := addTrace <| .ofHash (pureHash a) s!"{caption}: {toString a}"
 
-public section -- for `ToJson`
 /--
 The build trace file format,
 which stores information about a (successful) build.
@@ -67,7 +66,6 @@ public structure BuildMetadata where
   /-- A trace file that was created from fetching an artifact from the cache. -/
   synthetic : Bool
   deriving ToJson
-end
 
 public protected def BuildMetadata.fromJson? (json : Json) : Except String BuildMetadata := do
   let obj ← JsonObject.fromJson? json
diff --git a/src/lake/Lake/Build/Job/Basic.lean b/src/lake/Lake/Build/Job/Basic.lean
index a6ac2e4ec6..a2ce6ca24b 100644
--- a/src/lake/Lake/Build/Job/Basic.lean
+++ b/src/lake/Lake/Build/Job/Basic.lean
@@ -25,7 +25,6 @@ namespace Lake
 
 /-! ## JobAction -/
 
-public section -- for `Ord`
 /-- Information on what this job did. -/
 public inductive JobAction
 /-- No information about this job's action is available. -/
@@ -37,7 +36,6 @@ public inductive JobAction
 /-- Tried to perform a build action (set by `buildUnlessUpToDate?`) -/
 | build
 deriving Inhabited, Repr, DecidableEq, Ord
-end
 
 namespace JobAction
 
diff --git a/src/lake/Lake/Config/ConfigDecl.lean b/src/lake/Lake/Config/ConfigDecl.lean
index 7448cb5e6a..7335c66f1a 100644
--- a/src/lake/Lake/Config/ConfigDecl.lean
+++ b/src/lake/Lake/Config/ConfigDecl.lean
@@ -30,7 +30,6 @@ public abbrev ConfigType (kind : Name) (pkgName name : Name) : Type :=
 /-- Forward declared `ConfigTarget` to work around recursion issues (e.g., with `Package`). -/
 public opaque OpaqueConfigTarget (kind : Name) : Type
 
-public section -- for `TypeName`
 public structure ConfigDecl where
   pkg : Name
   name : Name
@@ -38,7 +37,6 @@ public structure ConfigDecl where
   config : ConfigType kind pkg name
   wf_data : ¬ kind.isAnonymous → CustomData pkg name = DataType kind ∧ DataType kind = OpaqueConfigTarget kind
   deriving TypeName
-end
 
 public structure PConfigDecl (p : Name) extends ConfigDecl where
   pkg_eq : toConfigDecl.pkg = p := by rfl
diff --git a/src/lake/Lake/Config/Dependency.lean b/src/lake/Lake/Config/Dependency.lean
index a120e321fe..dc5956a508 100644
--- a/src/lake/Lake/Config/Dependency.lean
+++ b/src/lake/Lake/Config/Dependency.lean
@@ -31,7 +31,6 @@ public inductive DependencySrc where
 | git (url : String) (rev : Option String) (subDir : Option FilePath)
 deriving Inhabited, Repr
 
-public section -- for `TypeName`
 /--
 A `Dependency` of a package.
 It specifies a package which another package depends on.
@@ -66,7 +65,6 @@ public structure Dependency where
   -/
   opts : NameMap String
   deriving Inhabited, TypeName
-end
 
 /-- The full name of a dependency (i.e., `<scope>/<name>`)-/
 public def Dependency.fullName (dep : Dependency) : String :=
diff --git a/src/lake/Lake/Config/LeanConfig.lean b/src/lake/Lake/Config/LeanConfig.lean
index e367eb3399..f0dbc5c798 100644
--- a/src/lake/Lake/Config/LeanConfig.lean
+++ b/src/lake/Lake/Config/LeanConfig.lean
@@ -70,7 +70,6 @@ public def orPreferLeft : Backend → Backend → Backend
 
 end Backend
 
-public section -- for `Ord`
 /--
 Lake equivalent of CMake's
 [`CMAKE_BUILD_TYPE`](https://stackoverflow.com/a/59314670).
@@ -99,7 +98,6 @@ public inductive BuildType
   -/
   | release
 deriving Inhabited, Repr, DecidableEq, Ord
-end
 
 namespace BuildType
 
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index d0b7c24f95..9e971dae6c 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -320,13 +320,11 @@ deriving Inhabited
 /-- The package's name. -/
 public abbrev PackageConfig.name (_ : PackageConfig n) := n
 
-public section -- for `TypeName`
 /-- A package declaration from a configuration written in Lean. -/
 public structure PackageDecl where
   name : Name
   config : PackageConfig name
   deriving TypeName
-end
 
 --------------------------------------------------------------------------------
 /-! # Package -/
@@ -423,12 +421,10 @@ public structure PostUpdateHook (pkgName : Name) where
 
 public hydrate_opaque_type OpaquePostUpdateHook PostUpdateHook name
 
-public section -- for `TypeName`
 public structure PostUpdateHookDecl where
   pkg : Name
   fn : PostUpdateFn pkg
   deriving TypeName
-end
 
 namespace Package
 
diff --git a/src/lake/Lake/Toml/Data/Value.lean b/src/lake/Lake/Toml/Data/Value.lean
index b6afcf9ee6..576bae91cf 100644
--- a/src/lake/Lake/Toml/Data/Value.lean
+++ b/src/lake/Lake/Toml/Data/Value.lean
@@ -18,7 +18,6 @@ open Lean
 
 namespace Lake.Toml
 
-public section -- for `BEq`
 /-- A TOML value with optional source info. -/
 public inductive Value
 | string (ref : Syntax) (s : String)
@@ -29,7 +28,6 @@ public inductive Value
 | array (ref : Syntax) (xs : Array Value)
 | table' (ref : Syntax) (xs : RBDict Name Value Name.quickCmp)
 deriving Inhabited, BEq
-end
 
 /-- A TOML table, an ordered key-value map of TOML values (`Lake.Toml.Value`). -/
 public abbrev Table := NameDict Value
diff --git a/src/lake/Lake/Util/Date.lean b/src/lake/Lake/Util/Date.lean
index b6b8c7ee9f..675246a1a8 100644
--- a/src/lake/Lake/Util/Date.lean
+++ b/src/lake/Lake/Util/Date.lean
@@ -26,14 +26,12 @@ public def rpad (s : String) (c : Char) (len : Nat) : String :=
 public def zpad (n : Nat) (len : Nat) : String :=
   lpad (toString n) '0' len
 
-public section -- for `Ord`
 /-- A date (year-month-day). -/
 public structure Date where
   year : Nat
   month : Nat
   day : Nat
   deriving Inhabited, DecidableEq, Ord, Repr
-end
 
 namespace Date
 
diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean
index ab15ef9efc..3d91e4f472 100644
--- a/src/lake/Lake/Util/Log.lean
+++ b/src/lake/Lake/Util/Log.lean
@@ -19,13 +19,11 @@ open Lean
 
 namespace Lake
 
-public section -- for `Ord`
 public inductive Verbosity
 | quiet
 | normal
 | verbose
 deriving Repr, DecidableEq, Ord
-end
 
 public instance : LT Verbosity := ltOfOrd
 public instance : LE Verbosity := leOfOrd
@@ -75,14 +73,12 @@ public def OutStream.get : OutStream → BaseIO IO.FS.Stream
 public instance : Coe IO.FS.Stream OutStream := ⟨.stream⟩
 public instance : Coe IO.FS.Handle OutStream := ⟨fun h => .stream (.ofHandle h)⟩
 
-public section -- for `Ord`, `ToJson`, `FromJson`
 public inductive LogLevel
 | trace
 | info
 | warning
 | error
 deriving Inhabited, Repr, DecidableEq, Ord, ToJson, FromJson
-end
 
 public instance : LT LogLevel := ltOfOrd
 public instance : LE LogLevel := leOfOrd
@@ -132,12 +128,10 @@ public def Verbosity.minLogLv : Verbosity → LogLevel
 | .normal =>  .info
 | .verbose => .trace
 
-public section -- for `ToJson`, `FromJson`
 public structure LogEntry where
   level : LogLevel
   message : String
   deriving Inhabited, ToJson, FromJson
-end
 
 public protected def LogEntry.toString (self : LogEntry) (useAnsi := false) : String :=
   if useAnsi then
diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean
index d8f86d07f0..bdcf3e1f2f 100644
--- a/src/lake/Lake/Util/Version.lean
+++ b/src/lake/Lake/Util/Version.lean
@@ -19,14 +19,12 @@ open System Lean
 
 namespace Lake
 
-public section -- for `Ord`
 /-- The major-minor-patch triple of a [SemVer](https://semver.org/). -/
 public structure SemVerCore where
   major : Nat := 0
   minor : Nat := 0
   patch : Nat := 0
   deriving Inhabited, Repr, DecidableEq, Ord
-end
 
 public instance : LT SemVerCore := ltOfOrd
 public instance : LE SemVerCore := leOfOrd