refactor: InductiveVal.numNested instead of .isNested

[nomeata]

Before, in order to find out how many auxilary datatype are in a
mutual group of inductive with nested data type, one had to jump
through hoops like this:

private def numNestedInducts (indName : Name) : MetaM Nat := do
  let .inductInfo indVal ← getConstInfo indName | panic! "{indName} is an inductive"
  let .recInfo recVal ← getConstInfo (mkRecName indName) | panic! "{indName} has a recursor"
  return recVal.numMotives - indVal.all.length

The InductiveVal data structure already has .isNested : Bool, so it
seems to be a natural extension to beef that up to .numNested: Nat.

This touched kernel code.

[nomeata]

(This includes #4683, diff will be prettier once that’s merged.)

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-4684 has successfully built against this PR. (2024-07-08 14:12:36) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase db7a01d126e3f8f1b327228fe00f247381337648 --onto 4ed79472af1f85b13c51e9ed77d15d3b4c40e3cc. (2024-07-08 16:04:30)