file organization in mathlib4 repo

Stream: mathlib4

[Scott Morrison]

I would like to add some additional definitions to extend parts of the API in core Lean. (e.g. Lean.LocalContext.firstDeclM)

Where in the mathlib4 repo should they go?

My suggestion is a folder /Mathlib/Lean/.