diff --git a/Mathlib/Computability/NFA.lean b/Mathlib/Computability/NFA.lean
index 65480352e29d0..13f58ecc80f06 100644
--- a/Mathlib/Computability/NFA.lean
+++ b/Mathlib/Computability/NFA.lean
@@ -15,7 +15,7 @@ which determines whether a string (implemented as a list over an arbitrary alpha
 set by evaluating the string over every possible path.
 We show that DFA's are equivalent to NFA's however the construction from NFA to DFA uses an
 exponential number of states.
-Note that this definition allows for Automaton with infinite states, a `Fintype` instance must be
+Note that this definition allows for Automaton with infinite states; a `Fintype` instance must be
 supplied for true NFA's.
 -/
 
@@ -30,7 +30,7 @@ universe u v
 set_option linter.uppercaseLean3 false
 
 /-- An NFA is a set of states (`σ`), a transition function from state to state labelled by the
-  alphabet (`step`), a starting state (`start`) and a set of acceptance states (`accept`).
+  alphabet (`step`), a set of starting states (`start`) and a set of acceptance states (`accept`).
   Note the transition function sends a state to a `Set` of states. These are the states that it
   may be sent to. -/
 structure NFA (α : Type u) (σ : Type v) where