dan on Nostr: if some junk in Lean can't be removed by syntax (section variables, implicit ...

if some junk in Lean can't be removed by syntax (section variables, implicit parameters etc), better abstraction layering, induction, and so on, you can always ask llm if it wants to write a new tactic or DSL. usually you won't need this but in some cases this is justified