This wiki note includes my generic prompt that is included in .lean files as the first comment. It has proved useful for code that has errors or confusing syntax: ```lean /- Lean4 prompt: Correct and complete the code,and the comments, below this comment following these rules: * provide justifications for changes to the code, and the comments. * ensure that all lines of code are preceeded with a comment that includes the CURRENT GOAL as in: -- ⊢ <replace this text with the CURRENT GOAL> * rewrite to correct any line of code that has a comment that begins with -- FIX ERROR: * explain in extreme detail any line of code that has a comment that begins with -- EXPLAIN: * use exact show ... from ... instead of exact * use the rewrite tactic instead of the rw tactic if it immediately precedes the exact show ... from ... tactic. Otherwise use the rw tactic. * replace all sorry tactics. * Use simp, dsimp tactics that specify the tactics used in brackets. [SEASON TO TASTE] * rewrite the proof using ... * do not use ... -/ ```