3.5.3: question about `1 + x` in `(fun (x : Nat) => 1 + x) = (Nat.succ ·)`

I'm not sure if this is incorrect, but just feel it questionable.

https://github.com/leanprover/fp-lean/blob/c30ec0985b695c6470f2ba104819e974e150c2f3/book/FPLean/TypeClasses/StandardClasses.lean#L144-L145

The statement (fun (x : Nat) => 1 + x) = (Nat.succ ·) is a perfectly reasonable statement. From the perspective of mathematics, two functions are equal if they map equal inputs to equal outputs, so this statement is even true, though it requires a one-line proof to convince Lean of this fact.

I think the one-line proof here is funext; apply Nat.add_comm. Is this what is intended?
The proof of the following statement seems easier:

(fun (x : Nat) => x + 1) = (Nat.succ ·)

example : (fun (x : Nat) => 1 + x) = (Nat.succ ·) := by
  funext
  apply Nat.add_comm

example : (fun (x : Nat) => x + 1) = (Nat.succ ·) := by
  rfl

Anyway, thanks for the great book!

Open book/FPLean/TypeClasses/StandardClasses.lean around lines 144–145 and compare the two function-equality examples in the issue. Check whether the text should explain the one-line proof or use the definitionally equal form; done means the book’s statement and accompanying explanation accurately reflect the intended Lean proof.