Lean 4 backend improvements

[JuanCoRo]

This issue is to document future improvements to the Lean 4 backend.

• Remove collisions in the generated declarations (such as ite). Related PR: Avoid clashes of generated declarations and Lean 4 #4742
• Format Lean 4 generated code #4747
• Unify definedness binders for function applications #4752
• Remove do blocks from generated Lean code when possible #4755
• Eliminate Option from total function result types #4756