refine structure proofs in docgen

Stream: mathlib4

[Yakov Pechersky]

Why does this appear in docgen? docs#LinearOrderedAddCommGroup.closure_equiv_closure.proof_17

[Kevin Buzzard]

...and about ten other such proofs below it!

[Henrik Böving]

https://github.com/leanprover/doc-gen4/blob/1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0/DocGen4/Process/DocInfo.lean#L120-L130 because it is not captured by this blacklist

[Henrik Böving]

.proof_n also seems like a name that people might choose for a proof? Not sure. But if we accept that it is there would need to be some attribute that tracks which theorems are part of this auto generated thing or we rename it to something like ._proof_n

[Jannis Limperg]

It would be really nice if Lean were to record whether a declaration was written by the user or auto-generated. Various tools approximate this with various name-based hacks, but it's not something that should need approximation.

[Eric Wieser]

I don't know if that's quite the right metric either. docs#add_left_comm is autogenerated, but what we really care about is whether it is intended to be user-facing

[Mario Carneiro]

I've been arguing for this for ages. Please make a @[autogenerated] and/or @[internal_detail] attribute

[Mario Carneiro]

The blacklist functions based on names have to change regularly and get out of date esp. when replicated elsewhere