Function hyperlink_proof 

pub fn hyperlink_proof(genv: GlobalEnv<'_, '_>, def_id: MaybeExternId)

Hyperlinks the proven_externally attribute to the proof’s def in the proof file, so users can easily jump to it. Call this after the Lean files are generated, so that the proof file exists on the first run. The def is found by searching the file, since the user may have edited it; if the file or the def is missing, we link to the first line of the file.