Typo in Init/MetaTypes.lean

Stream: lean4

[Jakub Nowak]

There's typo in the comment. "extract_lets" instead of "extract_lets". I would have reported it on lean4 github repo, though I wasn't sure whether I should make issue or PR.

[Marcus Rossel]

You can make a PR for this. (For this kind of PR I usually wait until I have found a couple of typos, and batch them all in one PR.)

[Kim Morrison]

lean#12174