chore: conform to header linter (#517)

I recently discovered that while the header linter is included as part
of the weekly linting set that CSLib enables, its implementation was
such that it only worked in Mathlib. Kim has kindly fixed this in
leanprover-community/mathlib4#38396, which
should be merged soon.

Unfortunately, when I did the port to the module system, I accidentally
placed some of the `public section` incorrectly above the module
docstring, getting no warning from the header linter, and subsequently
others followed my lead. Most of the changes here are just this, plus
just a few missing module docstrings and typos.

Author: chenson2018

Cslib/Algorithms/Lean/MergeSort/MergeSort.lean

@@ -11,8 +11,6 @@ public import Mathlib.Data.Nat.Cast.Order.Ring
 public import Mathlib.Data.Nat.Lattice
 public import Mathlib.Data.Nat.Log
 
-@[expose] public section
-
 /-!
 # MergeSort on a list
 
@@ -27,6 +25,8 @@ over the list `TimeM ℕ (List α)`. The time complexity of `mergeSort` is the n
 
 -/
 
+@[expose] public section
+
 set_option autoImplicit false
 
 namespace Cslib.Algorithms.Lean.TimeM

Cslib/Algorithms/Lean/TimeM.lean

@@ -9,9 +9,6 @@ module
 public import Cslib.Init
 public import Mathlib.Algebra.Group.Defs
 
-
-@[expose] public section
-
 /-!
 
 # TimeM: Time Complexity Monad
@@ -40,6 +37,9 @@ actual wall time, or as more complex types in order to model more general costs.
 
 See [Danielsson2008] for the discussion.
 -/
+
+@[expose] public section
+
 namespace Cslib.Algorithms.Lean
 
 /-- A monad for tracking time complexity of computations.

Cslib/Computability/Automata/Acceptors/Acceptor.lean

@@ -9,6 +9,8 @@ module
 public import Cslib.Init
 public import Mathlib.Computability.Language
 
+/-! -/
+
 @[expose] public section
 
 namespace Cslib.Automata

Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean

@@ -8,6 +8,8 @@ module
 
 public import Cslib.Computability.Languages.OmegaLanguage
 
+/-! -/
+
 @[expose] public section
 
 namespace Cslib.Automata

Cslib/Computability/Automata/DA/Basic.lean

@@ -11,8 +11,6 @@ public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 public import Cslib.Foundations.Data.OmegaSequence.InfOcc
 public import Cslib.Foundations.Semantics.FLTS.Basic
 
-@[expose] public section
-
 /-! # Deterministic Automata
 
 A Deterministic Automaton (`DA`) is an automaton defined by a transition function equipped with an
@@ -28,6 +26,8 @@ finiteness assumptions), deterministic Buchi automata, and deterministic Muller
   *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
 -/
 
+@[expose] public section
+
 open List Filter Cslib.ωSequence
 open scoped Cslib.FLTS
 

Cslib/Computability/Automata/DA/Buchi.lean

@@ -8,12 +8,10 @@ module
 
 public import Cslib.Computability.Automata.DA.Basic
 
-public section
-
 /-! # Deterministic Buchi automata.
 -/
 
-open Filter
+public section
 
 namespace Cslib.Automata.DA
 

Cslib/Computability/Automata/DA/Congr.lean

@@ -9,10 +9,10 @@ module
 public import Cslib.Computability.Automata.DA.Basic
 public import Cslib.Computability.Languages.Congruences.RightCongruence
 
-@[expose] public section
-
 /-! # Deterministic automaton corresponding to a right congruence. -/
 
+@[expose] public section
+
 namespace Cslib
 
 open scoped FLTS RightCongruence

Cslib/Computability/Automata/DA/Prod.lean

@@ -9,10 +9,10 @@ module
 public import Cslib.Computability.Automata.DA.Basic
 public import Cslib.Foundations.Semantics.FLTS.Prod
 
-@[expose] public section
-
 /-! # Product of deterministic automata. -/
 
+@[expose] public section
+
 namespace Cslib.Automata
 
 open List

Cslib/Computability/Automata/DA/ToNA.lean

@@ -10,12 +10,12 @@ public import Cslib.Computability.Automata.DA.Basic
 public import Cslib.Computability.Automata.NA.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
 
-@[expose] public section
-
 /-! # Translation of Deterministic Automata into Nonodeterministic Automata.
 
 This is the general version of the standard translation of DFAs into NFAs. -/
 
+@[expose] public section
+
 namespace Cslib.Automata.DA
 
 variable {State Symbol : Type*}

Cslib/Computability/Automata/EpsilonNA/Basic.lean

@@ -9,10 +9,10 @@ module
 public import Cslib.Computability.Automata.NA.Basic
 public import Cslib.Foundations.Semantics.LTS.HasTau
 
-@[expose] public section
-
 /-! # Nondeterministic automata with ε-transitions. -/
 
+@[expose] public section
+
 namespace Cslib.Automata
 
 /-- A nondeterministic finite automaton with ε-transitions (`εNA`) is an `NA` with an `Option`