FRONTEND: Get equation explorer to mention canonically equivalent form

[teorth]

Proposed in https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Questions.20for.20equation.20commentaries/near/518122864 : if viewing an equation in Equation Explorer that is equivalent to a lower numbered equation, mention the lowest numbered equivalent equation near the top of the page (in addition to where it is already listed at the end of the page). Furthermore, if this "canonically equivalent form" already has a commentary file, display that file (in addition to any file present for the non-canonical form).

[blefloch]

Ideally it would be best to also account for the dual equation and the corresponding commentary. The logic could be:

1. Display equation number, and lower-numbered equivalent equation if applicable (currently not done), and dual equation if different (currently done).
2. Display commentary:
   • if the equation has commentary display that;
   • elif the equation is equivalent to a lower-numbered equation with commentary, display that;
   • elif the equation is (equivalence + dual) to an equation with commentary, display that with a clear indication that this is the dual equation.

[Osalotioman]

This has already been resolved by #1386