doc: document Lean.Elab.StructInst

[thorimur]

This adds:

• a module doc for Lean.Elab.StructInst, which gives an overview of how the code for structure instance elaboration works
• docstrings for each definition in Lean.Elab.StructInst

Note: I'm aware this isn't the usual contribution process; however, I was encouraged on Zulip to make this pull request directly (i.e. without making an issue first) since this is a small PR (in the sense of no functionality being introduced).