Lean tactics can handle obvious things automatically, for some value of "obvious".

Knowing very little about lean but speculating here: is lean something that could output a few natural language expressions at key points so that you can still have “it should be clear that” for the natural language reader but have it undeniably proven.

Ie entrust the more tedious aspects but be able to follow along and still have references to check if you are curious about thoroughness.

Almost like a tap with a latex renderer at various insertion points?