chore: remove public section from end of files (#10684)

This PR removes `public section` lines from end of files; they look a
bit silly there.

src/Init/Control.lean

@@ -16,5 +16,3 @@ public import Init.Control.Option
 public import Init.Control.Lawful
 public import Init.Control.StateCps
 public import Init.Control.ExceptCps
-
-public section

src/Init/Control/Lawful.lean

@@ -10,5 +10,3 @@ public import Init.Control.Lawful.Basic
 public import Init.Control.Lawful.Instances
 public import Init.Control.Lawful.Lemmas
 public import Init.Control.Lawful.MonadLift
-
-public section

src/Init/Control/Lawful/MonadLift.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Control.Lawful.MonadLift.Basic
 public import Init.Control.Lawful.MonadLift.Lemmas
 public import Init.Control.Lawful.MonadLift.Instances
-
-public section

src/Init/Data.lean

@@ -53,5 +53,3 @@ public import Init.Data.Slice
 public import Init.Data.Order
 public import Init.Data.Rat
 public import Init.Data.Dyadic
-
-public section

src/Init/Data/Array.lean

@@ -30,5 +30,3 @@ public import Init.Data.Array.Erase
 public import Init.Data.Array.Zip
 public import Init.Data.Array.InsertIdx
 public import Init.Data.Array.Extract
-
-public section

src/Init/Data/Array/Lex.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Lemmas
-
-public section

src/Init/Data/Array/QSort.lean

@@ -7,5 +7,3 @@ module
 
 prelude
 public import Init.Data.Array.QSort.Basic
-
-public section

src/Init/Data/Basic.lean

@@ -16,5 +16,3 @@ public import Init.Data.UInt
 public import Init.Data.Repr
 public import Init.Data.ToString.Basic
 public import Init.Data.String.Extra
-
-public section

src/Init/Data/BitVec.lean

@@ -13,5 +13,3 @@ public import Init.Data.BitVec.Bitblast
 public import Init.Data.BitVec.Decidable
 public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Folds
-
-public section

src/Init/Data/ByteArray.lean

@@ -10,5 +10,3 @@ public import Init.Data.ByteArray.Basic
 public import Init.Data.ByteArray.Bootstrap
 public import Init.Data.ByteArray.Extra
 public import Init.Data.ByteArray.Lemmas
-
-public section

src/Init/Data/Char.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.Char.Basic
 public import Init.Data.Char.Lemmas
 public import Init.Data.Char.Order
-
-public section

src/Init/Data/Fin.lean

@@ -11,5 +11,3 @@ public import Init.Data.Fin.Log2
 public import Init.Data.Fin.Iterate
 public import Init.Data.Fin.Fold
 public import Init.Data.Fin.Lemmas
-
-public section

src/Init/Data/FloatArray.lean

@@ -7,5 +7,3 @@ module
 
 prelude
 public import Init.Data.FloatArray.Basic
-
-public section

src/Init/Data/Format.lean

@@ -10,5 +10,3 @@ public import Init.Data.Format.Basic
 public import Init.Data.Format.Macro
 public import Init.Data.Format.Instances
 public import Init.Data.Format.Syntax
-
-public section

src/Init/Data/Int.lean

@@ -18,5 +18,3 @@ public import Init.Data.Int.Pow
 public import Init.Data.Int.Cooper
 public import Init.Data.Int.Linear
 public import Init.Data.Int.OfNat
-
-public section

src/Init/Data/Int/Bitwise.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Int.Bitwise.Basic
 public import Init.Data.Int.Bitwise.Lemmas
-
-public section

src/Init/Data/Int/DivMod.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.Int.DivMod.Basic
 public import Init.Data.Int.DivMod.Bootstrap
 public import Init.Data.Int.DivMod.Lemmas
-
-public section

src/Init/Data/Iterators/Combinators.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.Iterators.Combinators.Monadic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.Iterators.Combinators.ULift
-
-public section

src/Init/Data/Iterators/Combinators/Monadic.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Iterators.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Combinators.Monadic.ULift
-
-public section

src/Init/Data/Iterators/Consumers.lean

@@ -13,5 +13,3 @@ public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Consumers.Partial
 
 public import Init.Data.Iterators.Consumers.Stream
-
-public section

src/Init/Data/Iterators/Consumers/Monadic.lean

@@ -10,5 +10,3 @@ public import Init.Data.Iterators.Consumers.Monadic.Access
 public import Init.Data.Iterators.Consumers.Monadic.Collect
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 public import Init.Data.Iterators.Consumers.Monadic.Partial
-
-public section

src/Init/Data/Iterators/Internal.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 public import Init.Data.Iterators.Internal.Termination
-
-public section

src/Init/Data/Iterators/Lemmas.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Iterators.Lemmas.Consumers
 public import Init.Data.Iterators.Lemmas.Combinators
-
-public section

src/Init/Data/Iterators/Lemmas/Combinators.lean

@@ -10,5 +10,3 @@ public import Init.Data.Iterators.Lemmas.Combinators.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic
 public import Init.Data.Iterators.Lemmas.Combinators.FilterMap
 public import Init.Data.Iterators.Lemmas.Combinators.ULift
-
-public section

src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
-
-public section

src/Init/Data/Iterators/Lemmas/Consumers.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
 public import Init.Data.Iterators.Lemmas.Consumers.Loop
-
-public section

src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
-
-public section

src/Init/Data/List.lean

@@ -31,5 +31,3 @@ public import Init.Data.List.MapIdx
 public import Init.Data.List.OfFn
 public import Init.Data.List.FinRange
 public import Init.Data.List.Lex
-
-public section

src/Init/Data/List/Nat.lean

@@ -18,5 +18,3 @@ public import Init.Data.List.Nat.BEq
 public import Init.Data.List.Nat.Modify
 public import Init.Data.List.Nat.InsertIdx
 public import Init.Data.List.Nat.Perm
-
-public section

src/Init/Data/List/Sort.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.List.Sort.Basic
 public import Init.Data.List.Sort.Impl
 public import Init.Data.List.Sort.Lemmas
-
-public section

src/Init/Data/Nat.lean

@@ -26,5 +26,3 @@ public import Init.Data.Nat.Compare
 public import Init.Data.Nat.Simproc
 public import Init.Data.Nat.Fold
 public import Init.Data.Nat.Order
-
-public section

src/Init/Data/Nat/Bitwise.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Nat.Bitwise.Basic
 public import Init.Data.Nat.Bitwise.Lemmas
-
-public section

src/Init/Data/Nat/Div.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Nat.Div.Basic
 public import Init.Data.Nat.Div.Lemmas
-
-public section

src/Init/Data/Option.lean

@@ -15,5 +15,3 @@ public import Init.Data.Option.Attach
 public import Init.Data.Option.List
 public import Init.Data.Option.Monadic
 public import Init.Data.Option.Array
-
-public section

src/Init/Data/Range.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Range.Basic
 public import Init.Data.Range.Lemmas
-
-public section

src/Init/Data/Slice/Array.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.Slice.Array.Basic
 public import Init.Data.Slice.Array.Iterator
 public import Init.Data.Slice.Array.Lemmas
-
-public section

src/Init/Data/String.lean

@@ -16,5 +16,3 @@ public import Init.Data.String.Bootstrap
 public import Init.Data.String.Slice
 public import Init.Data.String.Pattern
 public import Init.Data.String.Stream
-
-public section

src/Init/Data/Sum.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Sum.Basic
 public import Init.Data.Sum.Lemmas
-
-public section

src/Init/Data/ToString.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.ToString.Basic
 public import Init.Data.ToString.Macro
 public meta import Init.Data.ToString.Name
-
-public section

src/Init/Data/UInt.lean

@@ -11,5 +11,3 @@ public import Init.Data.UInt.Basic
 public import Init.Data.UInt.Log2
 public import Init.Data.UInt.Lemmas
 public import Init.Data.UInt.Bitwise
-
-public section

src/Init/Data/Vector.lean

@@ -24,5 +24,3 @@ public import Init.Data.Vector.Perm
 public import Init.Data.Vector.Find
 public import Init.Data.Vector.Algebra
 public import Init.Data.Vector.Stream
-
-public section

src/Init/Grind/Module.lean

@@ -9,4 +9,3 @@ public import Init.Grind.Module.Basic
 public import Init.Grind.Module.Envelope
 public import Init.Grind.Module.OfNatModule
 public import Init.Grind.Module.NatModuleNorm
-public section

src/Init/Grind/Ordered.lean

@@ -13,5 +13,3 @@ public import Init.Grind.Ordered.Field
 public import Init.Grind.Ordered.Int
 public import Init.Grind.Ordered.Rat
 public import Init.Grind.Ordered.Linarith
-
-public section

src/Init/GrindInstances.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.GrindInstances.ToInt
 public import Init.GrindInstances.Ring
 public import Init.GrindInstances.Nat
-
-public section

src/Init/GrindInstances/Ring.lean

@@ -13,5 +13,3 @@ public import Init.GrindInstances.Ring.SInt
 public import Init.GrindInstances.Ring.Fin
 public import Init.GrindInstances.Ring.BitVec
 public import Init.GrindInstances.Ring.Rat
-
-public section

src/Init/Internal/Order.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Internal.Order.Basic
 public import Init.Internal.Order.Lemmas
 public import Init.Internal.Order.Tactic
-
-public section

src/Init/Omega.lean

@@ -11,5 +11,3 @@ public import Init.Omega.IntList
 public import Init.Omega.LinearCombo
 public import Init.Omega.Constraint
 public import Init.Omega.Logic
-
-public section

src/Init/System.lean

@@ -10,5 +10,3 @@ public import Init.System.IO
 public import Init.System.Platform
 public import Init.System.Uri
 public import Init.System.Promise
-
-public section

src/Lean/Compiler.lean

@@ -19,5 +19,3 @@ public import Lean.Compiler.MetaAttr
 public import Lean.Compiler.NoncomputableAttr
 public import Lean.Compiler.Main
 public import Lean.Compiler.Old -- TODO: delete after we port code generator to Lean
-
-public section

src/Lean/Compiler/LCNF.lean

@@ -44,5 +44,3 @@ public import Lean.Compiler.LCNF.Closure
 public import Lean.Compiler.LCNF.LambdaLifting
 public import Lean.Compiler.LCNF.ReduceArity
 public import Lean.Compiler.LCNF.Probing
-
-public section

src/Lean/Data.lean

@@ -30,5 +30,3 @@ public import Lean.Data.NameTrie
 public import Lean.Data.RBTree
 public import Lean.Data.RBMap
 public import Lean.Data.RArray
-
-public section

src/Lean/Data/Json.lean

@@ -12,5 +12,3 @@ public import Lean.Data.Json.Printer
 public import Lean.Data.Json.Parser
 public import Lean.Data.Json.FromToJson
 public import Lean.Data.Json.Elab
-
-public section

src/Lean/Data/Json/FromToJson.lean

@@ -9,5 +9,3 @@ module
 prelude
 public import Lean.Data.Json.FromToJson.Basic
 public import Lean.Data.Json.FromToJson.Extra
-
-public section

src/Lean/Data/Lsp.lean

@@ -23,5 +23,3 @@ public import Lean.Data.Lsp.Workspace
 public import Lean.Data.Lsp.Ipc
 public import Lean.Data.Lsp.CodeActions
 public import Lean.Data.Lsp.Window
-
-public section

src/Lean/Data/Xml.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Lean.Data.Xml.Basic
 public import Lean.Data.Xml.Parser
-
-public section

src/Lean/Elab.lean

@@ -62,5 +62,3 @@ public import Lean.Elab.InfoTrees
 public import Lean.Elab.ErrorExplanation
 public import Lean.Elab.DocString
 public import Lean.Elab.DocString.Builtin
-
-public section

src/Lean/Elab/InfoTree.lean

@@ -9,5 +9,3 @@ module
 prelude
 public import Lean.Elab.InfoTree.Types
 public import Lean.Elab.InfoTree.Main
-
-public section

src/Lean/Elab/PreDefinition.lean

@@ -14,5 +14,3 @@ public import Lean.Elab.PreDefinition.WF
 public import Lean.Elab.PreDefinition.Eqns
 public import Lean.Elab.PreDefinition.Nonrec.Eqns
 public import Lean.Elab.PreDefinition.EqUnfold
-
-public section

src/Lean/Elab/PreDefinition/PartialFixpoint.lean

@@ -9,5 +9,3 @@ prelude
 public import Lean.Elab.PreDefinition.PartialFixpoint.Eqns
 public import Lean.Elab.PreDefinition.PartialFixpoint.Main
 public import Lean.Elab.PreDefinition.PartialFixpoint.Induction
-
-public section

src/Lean/Elab/PreDefinition/Structural.lean

@@ -7,5 +7,3 @@ module
 
 prelude
 public import Lean.Elab.PreDefinition.Structural.Main
-
-public section

src/Lean/Elab/PreDefinition/WF.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Lean.Elab.PreDefinition.WF.Main
 public import Lean.Elab.PreDefinition.WF.Eqns
-
-public section

src/Lean/Elab/Tactic.lean

@@ -55,5 +55,3 @@ public import Lean.Elab.Tactic.SimpArith
 public import Lean.Elab.Tactic.Show
 public import Lean.Elab.Tactic.Lets
 public import Lean.Elab.Tactic.Do
-
-public section

src/Lean/Elab/Tactic/Conv.lean

@@ -15,5 +15,3 @@ public import Lean.Elab.Tactic.Conv.Simp
 public import Lean.Elab.Tactic.Conv.Pattern
 public import Lean.Elab.Tactic.Conv.Delta
 public import Lean.Elab.Tactic.Conv.Unfold
-
-public section

src/Lean/Elab/Tactic/Do.lean

@@ -12,5 +12,3 @@ public import Lean.Elab.Tactic.Do.Attr
 public import Lean.Elab.Tactic.Do.LetElim
 public import Lean.Elab.Tactic.Do.Spec
 public import Lean.Elab.Tactic.Do.VCGen
-
-public section

src/Lean/Elab/Tactic/Do/ProofMode.lean

@@ -24,5 +24,3 @@ public import Lean.Elab.Tactic.Do.ProofMode.Cases
 public import Lean.Elab.Tactic.Do.ProofMode.Exfalso
 public import Lean.Elab.Tactic.Do.ProofMode.Have
 public import Lean.Elab.Tactic.Do.ProofMode.Refine
-
-public section

src/Lean/ErrorExplanations.lean

@@ -17,5 +17,3 @@ public import Lean.ErrorExplanations.ProjNonPropFromProp
 public import Lean.ErrorExplanations.PropRecLargeElim
 public import Lean.ErrorExplanations.RedundantMatchAlt
 public import Lean.ErrorExplanations.UnknownIdentifier
-
-public section

src/Lean/Linter.lean

@@ -17,5 +17,3 @@ public import Lean.Linter.Omit
 public import Lean.Linter.List
 public import Lean.Linter.Sets
 public import Lean.Linter.UnusedSimpArgs
-
-public section

src/Lean/Meta/Constructions.lean

@@ -11,5 +11,3 @@ public import Lean.Meta.Constructions.NoConfusion
 public import Lean.Meta.Constructions.RecOn
 public import Lean.Meta.Constructions.BRecOn
 public import Lean.Meta.Constructions.CasesOnSameCtor
-
-public section

src/Lean/Meta/Match/MatcherApp.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Lean.Meta.Match.MatcherApp.Basic
 public import Lean.Meta.Match.MatcherApp.Transform
-
-public section

src/Lean/Meta/Tactic.lean

@@ -45,5 +45,3 @@ public import Lean.Meta.Tactic.Rewrites
 public import Lean.Meta.Tactic.Grind
 public import Lean.Meta.Tactic.Ext
 public import Lean.Meta.Tactic.Try
-
-public section

src/Lean/Meta/Tactic/AC.lean

@@ -7,5 +7,3 @@ module
 
 prelude
 public import Lean.Meta.Tactic.AC.Main
-
-public section

src/Lean/Meta/Tactic/Grind/Arith.lean

@@ -13,4 +13,3 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing
 public import Lean.Meta.Tactic.Grind.Arith.Linear
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat
 public import Lean.Meta.Tactic.Grind.Arith.Simproc
-public section

src/Lean/Meta/Tactic/Grind/Arith/Model.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Offset.Model
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
-
-public section

src/Lean/Meta/Tactic/Simp/Arith/Int.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Lean.Meta.Tactic.Simp.Arith.Int.Basic
 public import Lean.Meta.Tactic.Simp.Arith.Int.Simp
-
-public section

src/Lean/Meta/Tactic/Simp/Arith/Nat.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Lean.Meta.Tactic.Simp.Arith.Nat.Basic
 public import Lean.Meta.Tactic.Simp.Arith.Nat.Simp
-
-public section

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean

@@ -19,5 +19,3 @@ public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
 public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Array
 public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.MethodSpecs
 public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.CtorIdx
-
-public section

src/Lean/PrettyPrinter/Delaborator.lean

@@ -11,5 +11,3 @@ public import Lean.PrettyPrinter.Delaborator.SubExpr
 public import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
 public import Lean.PrettyPrinter.Delaborator.Basic
 public import Lean.PrettyPrinter.Delaborator.Builtins
-
-public section

src/Lean/Server.lean

@@ -12,5 +12,3 @@ public import Lean.Server.FileWorker
 public import Lean.Server.Rpc
 public import Lean.Server.CodeActions
 public import Lean.Server.Test
-
-public section

src/Lean/Server/CodeActions.lean

@@ -10,5 +10,3 @@ prelude
 public import Lean.Server.CodeActions.Attr
 public import Lean.Server.CodeActions.Basic
 public import Lean.Server.CodeActions.Provider
-
-public section

src/Lean/Server/Rpc.lean

@@ -10,5 +10,3 @@ prelude
 public import Lean.Server.Rpc.Basic
 public import Lean.Server.Rpc.Deriving
 public import Lean.Server.Rpc.RequestHandling
-
-public section

src/Lean/Server/Test.lean

@@ -10,5 +10,3 @@ prelude
 public import Lean.Server.Test.Cancel
 public import Lean.Server.Test.Runner
 public import Lean.Server.Test.Refs
-
-public section

src/Lean/Util.lean

@@ -38,5 +38,3 @@ public import Lean.Util.NumApps
 public import Lean.Util.FVarSubset
 public import Lean.Util.SortExprs
 public import Lean.Util.Reprove
-
-public section

src/Lean/Widget.lean

@@ -13,5 +13,3 @@ public import Lean.Widget.InteractiveGoal
 public import Lean.Widget.TaggedText
 public import Lean.Widget.UserWidget
 public import Lean.Widget.Commands
-
-public section

src/Std/Data.lean

@@ -31,5 +31,3 @@ public import Std.Data.TreeSet.Raw
 
 public import Std.Data.Iterators
 public import Std.Data.ByteSlice
-
-@[expose] public section

src/Std/Data/DHashMap.lean

@@ -9,5 +9,3 @@ prelude
 public import Std.Data.DHashMap.Basic
 public import Std.Data.DHashMap.Lemmas
 public import Std.Data.DHashMap.AdditionalOperations
-
-public section

src/Std/Data/DTreeMap.lean

@@ -9,5 +9,3 @@ prelude
 public import Std.Data.DTreeMap.Basic
 public import Std.Data.DTreeMap.AdditionalOperations
 public import Std.Data.DTreeMap.Lemmas
-
-@[expose] public section

src/Std/Data/DTreeMap/Raw.lean

@@ -10,5 +10,3 @@ public import Std.Data.DTreeMap.Raw.Basic
 public import Std.Data.DTreeMap.Raw.AdditionalOperations
 public import Std.Data.DTreeMap.Raw.Lemmas
 public import Std.Data.DTreeMap.Raw.WF
-
-@[expose] public section

src/Std/Data/ExtDHashMap.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Std.Data.ExtDHashMap.Basic
 public import Std.Data.ExtDHashMap.Lemmas
-
-@[expose] public section

src/Std/Data/ExtDTreeMap.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Std.Data.ExtDTreeMap.Basic
 public import Std.Data.ExtDTreeMap.Lemmas
-
-@[expose] public section

src/Std/Data/ExtHashMap.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Std.Data.ExtHashMap.Basic
 public import Std.Data.ExtHashMap.Lemmas
-
-@[expose] public section

src/Std/Data/ExtHashSet.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Std.Data.ExtHashSet.Basic
 public import Std.Data.ExtHashSet.Lemmas
-
-@[expose] public section

src/Std/Data/ExtTreeMap.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Std.Data.ExtTreeMap.Basic
 public import Std.Data.ExtTreeMap.Lemmas
-
-@[expose] public section

src/Std/Data/ExtTreeSet.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Std.Data.ExtTreeSet.Basic
 public import Std.Data.ExtTreeSet.Lemmas
-
-@[expose] public section

src/Std/Data/HashMap.lean

@@ -9,5 +9,3 @@ prelude
 public import Std.Data.HashMap.Basic
 public import Std.Data.HashMap.Lemmas
 public import Std.Data.HashMap.AdditionalOperations
-
-@[expose] public section

src/Std/Data/HashSet.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Std.Data.HashSet.Basic
 public import Std.Data.HashSet.Lemmas
-
-@[expose] public section

src/Std/Data/Iterators/Combinators.lean

@@ -13,5 +13,3 @@ public import Std.Data.Iterators.Combinators.Drop
 public import Std.Data.Iterators.Combinators.DropWhile
 public import Std.Data.Iterators.Combinators.StepSize
 public import Std.Data.Iterators.Combinators.Zip
-
-@[expose] public section

src/Std/Data/Iterators/Combinators/Monadic.lean

@@ -12,5 +12,3 @@ public import Std.Data.Iterators.Combinators.Monadic.Drop
 public import Std.Data.Iterators.Combinators.Monadic.DropWhile
 public import Std.Data.Iterators.Combinators.Monadic.StepSize
 public import Std.Data.Iterators.Combinators.Monadic.Zip
-
-@[expose] public section

src/Std/Data/Iterators/Lemmas.lean

@@ -11,5 +11,3 @@ public import Std.Data.Iterators.Lemmas.Monadic
 public import Std.Data.Iterators.Lemmas.Combinators
 public import Std.Data.Iterators.Lemmas.Producers
 public import Std.Data.Iterators.Lemmas.Equivalence
-
-@[expose] public section

src/Std/Data/Iterators/Lemmas/Combinators.lean

@@ -12,5 +12,3 @@ public import Std.Data.Iterators.Lemmas.Combinators.TakeWhile
 public import Std.Data.Iterators.Lemmas.Combinators.Drop
 public import Std.Data.Iterators.Lemmas.Combinators.DropWhile
 public import Std.Data.Iterators.Lemmas.Combinators.Zip
-
-@[expose] public section

src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean

@@ -12,5 +12,3 @@ public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
-
-@[expose] public section