diff --git a/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean b/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean
index c4a0b24..4649313 100644
--- a/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean
+++ b/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean
@@ -157,8 +157,8 @@ Alternatively, you can use the ``trans`` tactic
 which takes ``y`` as an argument and produces the expected goals ``x ≤ y`` and
 ``y ≤ z``.
 Of course you can also avoid this issue by providing directly a full proof such as
-``exact le_trans inf_le_left inf_le_right``, but this requires a lot more
-planning.
+``exact le_trans (inf_le_left : (x ⊓ y) ⊓ z ≤ x ⊓ y) (inf_le_right : x ⊓ y ≤ y)``;
+but this requires a lot more planning.
 TEXT. -/
 -- QUOTE:
 example : x ⊓ y = y ⊓ x := by
diff --git a/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean b/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean
index f83cd70..d506b82 100644
--- a/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean
+++ b/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean
@@ -105,7 +105,7 @@ example (n : ℕ) : fib (n + 2) = fib n + fib (n + 1) := by rw [fib]
 /- TEXT:
 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 following example provides an explicit formula for the ``n``th Fibonacci number in terms of
 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.