[Merged by Bors] - doc: merge mathlib3 and mathlib4 READMEs

[j-loreaux]

This tries to merge the READMEs for mathlib3 and mathlib4 in a sensible way. Some irrelevant material about leanproject was removed, as well as a few mathlib3-specific items. Some of these should be replaced by mathlib4 counterparts in the future.

A section has been added about transitioning from Lean 3 to Lean 4 linking to the survival guide and running mathport on a project depending on mathlib.

---

some things that were deleted but need replacing in the future:

from the documentation section:

In addition to the pages generated for each file in the library, the docs also include pages on:

• tactics,
• commands,
• hole commands, and
• attributes.
• A couple of tutorial Lean files

from the guidelines section:

• The commit naming conventions

[ADedecker]

This command should be added to the contributing guidelines, I'd say we should keep it their (in the "contributing" section) for now.

[j-loreaux]

good point, I just added that entire bulleted list back under Contributing

[ADedecker]

Thanks!

bors d+

[bors]

✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[j-loreaux]

bors merge

[j-loreaux]

trying again?

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style