> Sledgehammer is nice but probably just a question of time until an equivalent can be ported/created for Lean.

I have no knowledge of what sledgehammer is. However...

> it also makes proofs concise but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer"

This description makes sledgehammer sound identical to Mathlib's `grind`. https://leanprover-community.github.io/mathlib4_docs/Init/Gr...