lean#296 mention tactics in docstrings

Stream: PR reviews

[Johan Commelin]

I think we should try to do something with this PR. I don't really care if we do this in core or in mathlib. But it would be great to have docstrings on forall and exists that tell the user which tactics to use.