Hyperlinking missing on some documentation

[hrmacbeth]

In the documentation for MulEquiv.withOneCongr, the declaration Equiv.optionCongr is referenced, but there is no automatic hyperlink to that declaration in the docs.

The corresponding documentation in doc-gen3 does have the hyperlink.

The same bug occurs elsewhere, e.g. a missing hyperlink to CanonicallyOrderedCommSemiring in this module docstring, and OrderIso.mulLeft where it misses the link to OrderEmbedding.mulLeft and instead links to a locally-defined mulLeft.

[hrmacbeth]

In other examples, a hyperlink is wrongly created. For example, in the module docstring of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/GroupPower/Basic.html the word pow gets a hyperlink, seemingly at random, to Dvd.dvd.pow. The same bug occurs in other module docstrings.

The corresponding documentation in doc-gen3 does not have that hyperlink.

[hargoniX]

This is due to our hyperlinking heuristic. Ideally I would hope we could at some point end up with a standartized version of Lean markdown that has a standartized implementation.

[alreadydone]

I came here to file an issue because I observed the reference to minpoly.equivAdjoin at AdjoinRoot.Minpoly.toAdjoin doesn't render as a link, only to discover this has already been reported 8 months ago.

[ericrbg]

Another one is Nat.toFinset_factors

[fpvandoorn]

Another one: WfDvdMonoidWfDvdMonoid not hyperlinking DvdNotUnit

[acmepjz]

I came here to file an issue because I observed the reference to minpoly.equivAdjoin at AdjoinRoot.Minpoly.toAdjoin doesn't render as a link, only to discover this has already been reported 8 months ago.

I think it's because that minpoly.equivAdjoin is a downstream definition.

Another one is Nat.toFinset_factors

Another one: WfDvdMonoidWfDvdMonoid not hyperlinking DvdNotUnit

These two are not related to the auto-linking of codes in markdown. That must be some other unimplemented things.