But the key difference between Mizar style proofs and Coq/Lean style proofs is just that the former is declarative and the latter is procedural. They're both ul

But the key difference between Mizar style proofs and Coq/Lean style proofs is just that the former is declarative and the latter is procedural. They're both ultimately just tactics based. Sure, a declarative style is nice when reasoning about equations, but otherwise the proofs simply degenerate into awkwardly written procedural tactics proofs.