Merge branch 'ys-working' into beta

Author: yisiox

README.md

@@ -16,7 +16,7 @@ This repository contains a formalization of Mazurkiewicz trace theory in the Lea
 ### Ochmański's Theorem
 - `Language.lean` contains basic definitions and lemmas for trace languages.
 - `MyhillNerode.lean` supplies a proof of the Myhill-Nerode theorem in the context of monoids.
-- `Hashiguchi.lean` currently contains just the statement of Hashiguchi's theorem on sufficient conditions for a trace language to have finite rank.
+- `Hashiguchi.lean` contains a proof of Hashiguchi's theorem on recognizable trace closures.
 - `RegularExpressions.lean` reinterprets mathlib4's `RegularExpression` on traces.
 - `Ochmanski.lean` contains the proof of Ochmański's theorem on recognizable trace languages and lemmas leading up to it.