Fix some typos from a brief overview

MIL/C01_Introduction/S02_Overview.lean

@@ -65,7 +65,7 @@ Lean accepts it as a term of that type,
 you have done something very impressive.
 (Using ``sorry`` is cheating, and Lean knows it.)
 So now you know the game.
-All that is left to learn are the rules.
+All that is left to learn is the rules.
 
 This book is complementary to a companion tutorial,
 `Theorem Proving in Lean <https://leanprover.github.io/theorem_proving_in_lean4/>`_,

MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean

@@ -470,7 +470,7 @@ If ``x`` has type ``α`` and ``s`` has type ``Set α``, then ``x ∈ s`` is a pr
 that asserts that ``x`` is an element of ``s``. If ``y`` has some different type ``β`` then the
 expression ``y ∈ s`` makes no sense. Here "makes no sense" means "has no type hence Lean does not
 accept it as a well-formed statement". This contrasts with Zermelo-Fraenkel set theory for instance
-where ``a ∈ b`` is a well-formed statement for every mathematical objects ``a`` and ``b``.
+where ``a ∈ b`` is a well-formed statement for both mathematical objects ``a`` and ``b``.
 For instance ``sin ∈ cos`` is a well-formed statement in ZF. This defect of set theoretic
 foundations is an important motivation for not using it in a proof assistant which is meant to assist
 us by detecting meaningless expressions. In Lean ``sin`` has type ``ℝ → ℝ`` and ``cos`` has type

MIL/C04_Sets_and_Functions/S01_Sets.lean

@@ -328,7 +328,7 @@ In type theory, a *property* or *predicate* on a type ``α``
 is just a function ``P : α → Prop``.
 This makes sense:
 given ``a : α``, ``P a`` is just the proposition
-that ``P`` holds of ``a``.
+that ``P`` holds for ``a``.
 In the library, ``Set α`` is defined to be ``α → Prop`` and ``x ∈ s`` is defined to be ``s x``.
 In other words, sets are really properties, treated as objects.