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

[xuhongxu96]

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

fp-lean/book/FPLean/TypeClasses/StandardClasses.lean

Lines 144 to 145 in c30ec09

	The statement {anchorTerm functionEqProp}`(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.

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!