Nits c05

MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean

@@ -32,7 +32,7 @@ The command specifies that ``Nat`` is the datatype generated
 freely and inductively by the two constructors ``zero : Nat`` and
 ``succ : Nat → Nat``.
 Of course, the library introduces notation ``ℕ`` and ``0`` for
-``nat`` and ``zero`` respectively. (Numerals are translated to binary
+``Nat`` and ``zero`` respectively. (Numerals are translated to binary
 representations, but we don't have to worry about the details of that now.)
 
 What "freely" means for the working mathematician is that the type

MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean

@@ -218,16 +218,14 @@ theorem fib_add' : ∀ m n, fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib
 
 /- TEXT:
 As an exercise, use ``fib_add`` to prove the following.
-EXAMPLES: -/
--- QUOTE:
-example (n : ℕ): (fib n) ^ 2 + (fib (n + 1)) ^ 2 = fib (2 * n + 1) := by sorry
--- QUOTE.
-/- SOLUTIONS:
-example (n : ℕ): (fib n) ^ 2 + (fib (n + 1)) ^ 2 = fib (2 * n + 1) := by
-  rw [two_mul, fib_add, pow_two, pow_two]
 BOTH: -/
+-- QUOTE:
 example (n : ℕ): (fib n) ^ 2 + (fib (n + 1)) ^ 2 = fib (2 * n + 1) := by
+/- EXAMPLES:
+  sorry
+SOLUTIONS: -/
   rw [two_mul, fib_add, pow_two, pow_two]
+-- QUOTE.
 
 /- TEXT:
 Lean's mechanisms for defining recursive functions are flexible enough to allow arbitrary
@@ -246,10 +244,10 @@ theorem ne_one_iff_exists_prime_dvd : ∀ {n}, n ≠ 1 ↔ ∃ p : ℕ, p.Prime
   | 0 => by simpa using Exists.intro 2 Nat.prime_two
   | 1 => by simp [Nat.not_prime_one]
   | n + 2 => by
-    have hn : n+2 ≠ 1 := by omega
+    have hn : n + 2 ≠ 1 := by omega
     simp only [Ne, not_false_iff, true_iff, hn]
     by_cases h : Nat.Prime (n + 2)
-    · use n+2, h
+    · use n + 2, h
     · have : 2 ≤ n + 2 := by omega
       rw [Nat.not_prime_iff_exists_dvd_lt this] at h
       rcases h with ⟨m, mdvdn, mge2, -⟩