Example: in the original FLT blueprint, we have Wiles_Frey and Wiles_Frey_again both corresponding to \lean{Wiles_Frey}. Because only one attribute can be added to a Lean declaration, they are merged and the second is discarded. In the converted LaTeX, both theorems are \inputleannode{Wiles_Frey}. This causes duplicate \label{Wiles_Frey} in two locations, giving a LaTeX warning and this also causes \uses links to not resolve correctly to both nodes.
Example: in the original FLT blueprint, we have
Wiles_FreyandWiles_Frey_againboth corresponding to\lean{Wiles_Frey}. Because only one attribute can be added to a Lean declaration, they are merged and the second is discarded. In the converted LaTeX, both theorems are\inputleannode{Wiles_Frey}. This causes duplicate\label{Wiles_Frey}in two locations, giving a LaTeX warning and this also causes \uses links to not resolve correctly to both nodes.