Should Exercise 3.5.12 have a second part?

Stream: Analysis I

[Dan Abramov]

In the book, Exercise 3.5.12 has a second part:

Screenshot 2025-08-13 at 18.00.00.png

I solved SetTheory.Set.recursion using Nat.rec like this:

/-- Exercise 3.5.12, with errata from web site incorporated -/
theorem SetTheory.Set.recursion (X: Type) (f: nat → X → X) (c:X) :
    ∃! a: nat → X, a 0 = c ∧ ∀ n, a (n + 1:ℕ) = f n (a n) := by
  apply existsUnique_of_exists_of_unique
  · let a : ℕ → X := Nat.rec c fun n x ↦ f n x
    use fun n ↦ a n
    simp_all [a]
  intro f1 f2 ⟨h1z, h1s⟩ ⟨h2z, h2s⟩
  ext x
  rw [show x = (x:ℕ) by simp]
  induction' (x:ℕ) with n hn
  · rw [show ((0:ℕ):nat) = 0 by rfl]
    cc
  rw [h1s, h2s, hn]

Assuming this solution makes sense, it only covers the first part.

Is it worth trying to approach the second part (using only Peano Axioms)? I suppose this would require importing Chapter2.Nat? Or would the recommended approach be to work with Mathlib Nat but to avoid Nat.rec and order?

Or is the second part of this exercise not well-suited to this formalization in general?

Thanks.

[Dan Abramov]

I guess I'm also not sure that my solution is legit at all (even for the first part) since depending on Nat.rec might be defeating the point?

[Dan Abramov]

Yeah on a second thought, my solution is kind of circular and doesn't follow the hint so I'll give it another try. Still, wondering if the second part is intended to be done.

[Terence Tao]

The general philosophy I have in the book is that once a relevant concept (e.g., the natural numbers) is developed, one transitions over to the Mathlib version of that concept, and full access to all the API of that version is then permitted; for instance, after Chapter 2, one is encouraged use the entire library of Nat, including Nat.rec.

With this perspective, one way to proceed would be to continue to use Mathlib's Nat, but only via the Mathlib_Nat object constructed in the Chapter 2 epilogue. (But as one can see from that object, Nat.rec is oneo of the components, so your argument would basically fulfill the spirit of the exercise already.)