fix compilation errors

MIL.lean

@@ -17,20 +17,23 @@ import MIL.C04_Sets_and_Functions.S03_The_Schroeder_Bernstein_Theorem
 import MIL.C05_Elementary_Number_Theory.S01_Irrational_Roots
 import MIL.C05_Elementary_Number_Theory.S02_Induction_and_Recursion
 import MIL.C05_Elementary_Number_Theory.S03_Infinitely_Many_Primes
-import MIL.C06_Structures.S01_Structures
-import MIL.C06_Structures.S02_Algebraic_Structures
-import MIL.C06_Structures.S03_Building_the_Gaussian_Integers
-import MIL.C07_Hierarchies.S01_Basics
-import MIL.C07_Hierarchies.S02_Morphisms
-import MIL.C07_Hierarchies.S03_Subobjects
-import MIL.C08_Groups_and_Rings.S01_Groups
-import MIL.C08_Groups_and_Rings.S02_Rings
-import MIL.C09_Topology.S01_Filters
-import MIL.C09_Topology.S02_Metric_Spaces
-import MIL.C09_Topology.S03_Topological_Spaces
-import MIL.C10_Differential_Calculus.S01_Elementary_Differential_Calculus
-import MIL.C10_Differential_Calculus.S02_Differential_Calculus_in_Normed_Spaces
-import MIL.C11_Integration_and_Measure_Theory.S01_Elementary_Integration
-import MIL.C11_Integration_and_Measure_Theory.S02_Measure_Theory
-import MIL.C11_Integration_and_Measure_Theory.S03_Integration
+import MIL.C06_Discrete_Mathematics.S01_More_Induction
+import MIL.C06_Discrete_Mathematics.S02_Finsets_and_Fintypes
+import MIL.C06_Discrete_Mathematics.S03_Counting_Arguments
+import MIL.C07_Structures.S01_Structures
+import MIL.C07_Structures.S02_Algebraic_Structures
+import MIL.C07_Structures.S03_Building_the_Gaussian_Integers
+import MIL.C08_Hierarchies.S01_Basics
+import MIL.C08_Hierarchies.S02_Morphisms
+import MIL.C08_Hierarchies.S03_Subobjects
+import MIL.C09_Groups_and_Rings.S01_Groups
+import MIL.C09_Groups_and_Rings.S02_Rings
+import MIL.C10_Topology.S01_Filters
+import MIL.C10_Topology.S02_Metric_Spaces
+import MIL.C10_Topology.S03_Topological_Spaces
+import MIL.C11_Differential_Calculus.S01_Elementary_Differential_Calculus
+import MIL.C11_Differential_Calculus.S02_Differential_Calculus_in_Normed_Spaces
+import MIL.C12_Integration_and_Measure_Theory.S01_Elementary_Integration
+import MIL.C12_Integration_and_Measure_Theory.S02_Measure_Theory
+import MIL.C12_Integration_and_Measure_Theory.S03_Integration
 import MIL.Common

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:

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

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.

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}}