[siknad]

Big:

* tactics (proof scripts are a lot easier than manual proving)

* syntax extensibility (Racket-like, supports custom elaboration/delaboration)

* mathlib (library of formalized math)

* tooling (can't say it's better, I haven't used Idris, but it's at least a lot nicer than Agda's: rustup-like version manager `elan`, own build system `lake`, official vscode extension supporting mini web apps which can interact with the code)

Small things I can remember:

* do-notation with early return and imperative loops

* easier termination proof handling (provide some expression using function arguments with `decreasing_by` and prove it's decreasing with `termination_by` block, which may be automatic even for non-structural recursion because of some built-in tactic)

[dmytrish]

Regarding tactics: I started with Coq and I felt for a long time that I had no idea what tactics actually do. Proofs with tactics look nice on the surface, but I really did not like hidden state and hidden actions.

Redoing some proofs in Lean by construction of proof terms was eye-opening, it's just functional programming with dependent types! I still think that teaching with tactics first without exposing proof terms is a mistake.

I've learned to see the value of tactics later, again thanks to Lean: there are proofs that are more natural in the tactics style. Sometimes a mixed approach is ideal: growing intermediate proof terms from the premises and then wrangling the hypothesis with tactics to meet the lemmas.