diff --git a/MIL/C06_Discrete_Mathematics/S01_More_Induction.lean b/MIL/C06_Discrete_Mathematics/S01_More_Induction.lean
index 03daee92..e148b72c 100644
--- a/MIL/C06_Discrete_Mathematics/S01_More_Induction.lean
+++ b/MIL/C06_Discrete_Mathematics/S01_More_Induction.lean
@@ -11,7 +11,7 @@ namespace more_induction
 More Induction
 --------------
 
-In :numref:`induction_and_recursion` we saw how to define the factorial function by recursion on
+In :numref:`section_induction_and_recursion` we saw how to define the factorial function by recursion on
 the natural numbers.
 EXAMPLES: -/
 -- QUOTE:
@@ -94,7 +94,7 @@ EXAMPLES: -/
 The ``@[simp]`` annotation means that the simplifier will use the defining equations.
 You can also apply them by writing ``rw [fib]``.
 Below it will be helpful to give a name to the ``n+2`` case.
-EXAMPLES:-/
+EXAMPLES: -/
 -- QUOTE:
 theorem fib_add_two (n : ℕ) : fib (n+2) = fib n + fib (n+1) := rfl
 
@@ -105,7 +105,7 @@ example (n : ℕ) : fib (n+2) = fib n + fib (n+1) := by rw [fib]
 Using Lean's notation for recursive functions, you can carry out proofs by induction on the
 natural numbers that mirror the recursive definition of ``fib``.
 The following example provides an explicit formula for the nth Fibonacci number in terms of
-the golden mean, ``φ``, and its conjugate, ``φ '``.
+the golden mean, ``φ``, and its conjugate, ``φ'``.
 We have to tell Lean that we don't expect our definitions to generate code because the
 arithmetic operations on the real numbers are not computable.
 EXAMPLES: -/
@@ -229,6 +229,7 @@ example (n : ℕ): (fib n)^2 + (fib (n + 1))^2 = fib (2 * n + 1) :=
   sorry
 EXAMPLES: -/
   by rw [two_mul, fib_add, pow_two, pow_two]
+-- QUOTE.
 -- BOTH:
 
 /- TEXT:
diff --git a/MIL/C06_Discrete_Mathematics/S02_Finsets_and_Fintypes.lean b/MIL/C06_Discrete_Mathematics/S02_Finsets_and_Fintypes.lean
index d4762fa8..c4d1a950 100644
--- a/MIL/C06_Discrete_Mathematics/S02_Finsets_and_Fintypes.lean
+++ b/MIL/C06_Discrete_Mathematics/S02_Finsets_and_Fintypes.lean
@@ -74,7 +74,7 @@ If you step through the last example below, you will see applying ``ext``
 followed by ``simp`` reduces the identity to a problem
 in propositional logic.
 As an exercise, you can try proving some of set identities from
-:numref:`Chapter %s <set_and_functions>`, transported to finsets.
+:numref:`Chapter %s <sets_and_functions>`, transported to finsets.
 
 You have already seen the notation ``Finset.range n`` for the
 finite set of natural numbers :math:`\{ 0, 1, \ldots, n-1 \}`.
@@ -136,7 +136,7 @@ set_option pp.notation false in
 Unfortunately, we cannot use set-builder notation with finsets: we can't write
 an expression like ``{ x : ℕ | Even x ∧ x < 5 }`` because Lean can't straightforwardly infer that such a set is finite.
 However, you can start with a finset and separate the elements you want using ``Finset.filter``.
-TEXT.-/
+EXAMPLES: -/
 -- QUOTE:
 #check (range n).filter Even
 #check (range n).filter (fun x ↦ Even x ∧ x ≠ 3)
@@ -204,7 +204,7 @@ has a property, show that the empty set has the property and that the property i
 preserved when we add one new element to a finset. (The ``@`` in ``@insert`` is need
 in the induction step to give names to the parameters ``a`` and ``s`` because they
 have been marked implicit. )
-EXAMPLE: -/
+EXAMPLES: -/
 -- QUOTE:
 #check Finset.induction
 
@@ -309,7 +309,7 @@ end
 We have already seen a prototypical example of a fintype, namely, the types ``Fin n`` for
 each ``n``.
 But Lean also recognizes that the fintypes are closed under operations like the product operation.
--/
+EXAMPLES: -/
 -- QUOTE:
 example : Fintype.card (Fin 5) = 5 := by simp
 example : Fintype.card ((Fin 5) × (Fin 3)) = 15 := by simp
diff --git a/MIL/C06_Discrete_Mathematics/S03_Counting_Arguments.lean b/MIL/C06_Discrete_Mathematics/S03_Counting_Arguments.lean
index cde987c8..eae0bc37 100644
--- a/MIL/C06_Discrete_Mathematics/S03_Counting_Arguments.lean
+++ b/MIL/C06_Discrete_Mathematics/S03_Counting_Arguments.lean
@@ -97,6 +97,7 @@ theorem doubleCounting {α β : Type*} (s : Finset α) (t : Finset β)
         -- congr; ext b; apply h_right
         apply Finset.sum_congr rfl h_right
     _ ≤ t.card := by simp
+-- QUOTE.
 
 /- TEXT:
 An exercise from Bhavik. Also: replace = by ≤ in the previous theorem.
diff --git a/sphinx_source/unixode.sty b/sphinx_source/unixode.sty
index f909a83e..075b375f 100644
--- a/sphinx_source/unixode.sty
+++ b/sphinx_source/unixode.sty
@@ -81,7 +81,7 @@
 \newunicodechar{⊞}{\ensuremath{\boxplus}}
 
 \newunicodechar{∇}{\ensuremath{\nabla}}
-\newunicodechar{√}{\ensuremath{\sqrt}}
+\newunicodechar{√}{\ensuremath{\surd}}
 
 \newunicodechar{⬝}{\ensuremath{\cdot}}
 \newunicodechar{•}{\ensuremath{\cdot}}