fix: remove lambda abstraction of Nat.rec_zero and Nat.rec_add_one (

#3839)

```lean
theorem rec_zero {C : ℕ → Sort u} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) :
    (Nat.rec h0 h : ∀ n, C n) 0 = h0 :=
  rfl
```
The above theorem is elaborated as follow:
```lean
theorem rec_zero {C : ℕ → Sort u} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) :
    (fun n => Nat.rec h0 h n) 0 = h0 :=
  rfl
```
This form of the theorem isn't generic. This PR fixes this problem.



Co-authored-by: Pol_tta <52843868+Komyyy@users.noreply.github.com>

Mathlib/Data/Nat/Basic.lean

@@ -373,16 +373,18 @@ This section is here due to dependencies -- the lemmas here require some of the
 proved above, and some of the results in later sections depend on the definitions in this section.
 -/
 
+-- Porting note: The type ascriptions of these two theorems need to be changed,
+-- as mathport wrote a lambda that wasn't there in mathlib3, that prevents `simp` applying them.
 
 @[simp]
 theorem rec_zero {C : ℕ → Sort u} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) :
-    (Nat.rec h0 h : ∀ n, C n) 0 = h0 :=
+    Nat.rec h0 h 0 = h0 :=
   rfl
 #align nat.rec_zero Nat.rec_zero
 
 @[simp]
 theorem rec_add_one {C : ℕ → Sort u} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) (n : ℕ) :
-    (Nat.rec h0 h : ∀ n, C n) (n + 1) = h n ((Nat.rec h0 h : ∀ n, C n) n) :=
+    Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n) :=
   rfl
 #align nat.rec_add_one Nat.rec_add_one