Merge pull request #2 from pitmonticone/lean-typos

Fix typos in docstrings and comments

Author: fredokun

LeanMachines/Event/Basic.lean

@@ -45,7 +45,7 @@ This comprises:
 class Machine (CTX : outParam (Type u)) (M) where
   /-- The context (i.e. parameters) of the machine. -/
   context : CTX
-  /-- The invariant property that must be satisified
+  /-- The invariant property that must be satisfied
   by a machine (state) of type `M`. -/
   invariant : M → Prop
   /-- The "before initialization", or *reset state*. -/
@@ -274,7 +274,7 @@ variable (γ)
 #check (Arrow.arrow f : _KEvent M γ α β)
 -/
 
--- Arrows are less poweful (but more general) than Monads
+-- Arrows are less powerful (but more general) than Monads
 -- but Events are monads in their output type
 -- and both monads and arrows do not apply on input types
 

LeanMachines/Event/Convergent.lean

@@ -31,7 +31,7 @@ refinements of the event.
 Basic well-founded orders are proposed, such as the natural ordering for
 natural numbers (type `Nat`), or subset ordering for finite sets
  (type `FinSet α`), and so on.  Order composition means are also
- available, such as lexicographic produc ordering, multiset ordering, etc.
+ available, such as lexicographic product ordering, multiset ordering, etc.
  And of course, custom orderings can be defined (cf. Mathlib's documentation).
 
 -/

LeanMachines/NonDet/Basic.lean

@@ -81,7 +81,7 @@ def skip_NDEvent [Machine CTX M] : _NDEvent M α β :=
 -/
 
 
--- Remark: The functor instance is existential, not suprising given the relational context
+-- Remark: The functor instance is existential, not surprising given the relational context
 instance [Machine CTX M] : Functor (_NDEvent M γ) where
   map f ev :=
   {