batch of typos

MIL/C03_Logic/S03_Negation.lean

@@ -91,7 +91,7 @@ example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by
 /- TEXT:
 Remember that it is often convenient to use ``linarith``
 when a goal follows from linear equations and
-inequalities that in the context.
+inequalities that are in the context.
 
 See if you can prove these in a similar way:
 TEXT. -/

MIL/C03_Logic/S04_Conjunction_and_Iff.lean

@@ -190,7 +190,7 @@ You have already seen that you can write ``h.mp`` and ``h.mpr``
 or ``h.1`` and ``h.2`` for the two directions of ``h : A ↔ B``.
 You can also use ``cases`` and friends.
 To prove an if-and-only-if statement,
-you can uses ``constructor`` or angle brackets,
+you can use ``constructor`` or angle brackets,
 just as you would if you were proving a conjunction.
 TEXT. -/
 -- QUOTE:

MIL/C03_Logic/S05_Disjunction.lean

@@ -114,7 +114,7 @@ example : x < |y| → x < y ∨ x < -y := by
 
 /- TEXT:
 The names ``inl`` and ``inr`` are short for "intro left" and "intro right,"
-respectively. Using ``case`` has the advantage is that you can prove the
+respectively. Using ``case`` has the advantage that you can prove the
 cases in either order; Lean uses the tag to find the relevant goal.
 If you don't care about that, you can use ``next``, or ``match``,
 or even a pattern-matching ``have``.
@@ -129,7 +129,6 @@ example : x < |y| → x < y ∨ x < -y := by
     rw [abs_of_neg h]
     intro h; right; exact h
 
-
 example : x < |y| → x < y ∨ x < -y := by
   match le_or_gt 0 y with
     | Or.inl h =>
@@ -141,12 +140,12 @@ example : x < |y| → x < y ∨ x < -y := by
 -- QUOTE.
 
 /- TEXT:
-In the case of the ``match``, we need to use the full names
+In the case of ``match``, we need to use the full names
 ``Or.inl`` and ``Or.inr`` of the canonical ways to prove a disjunction.
 In this textbook, we will generally use ``rcases`` to split on the
 cases of a disjunction.
 
-Try proving the triangle inequality using the two
+Try proving the triangle inequality using the
 first two theorems in the next snippet.
 They are given the same names they have in Mathlib.
 TEXT. -/