tl;dr as an acolyte is that sometimes the bug can be fixed by adding extra data (e.g. number of minus signs, or method to compute minus signs) to your declaration of equality.
Concrete example from Kev Buzzard's "Lean proof of Fermat's Last Theorem" from yesterday (2024-06-19 UT)
p34:
"It is impossible to say which of the two canonical isomorphisms is “the most canonical”;
people working in different areas make different choices in order to locally minimise the
number of minus signs in their results."
Concrete example from Kev Buzzard's "Lean proof of Fermat's Last Theorem" from yesterday (2024-06-19 UT)
p34: "It is impossible to say which of the two canonical isomorphisms is “the most canonical”; people working in different areas make different choices in order to locally minimise the number of minus signs in their results."
https://imperialcollegelondon.github.io/FLT/blueprint.pdf
A lot of the subtleties seem to come from the pecularities of what is meant by "canonical" rather than by "isomorphic"