Leo de Mora proposed Lean tactics—helper programs that automate repeated steps commonly needed in proofs.

“So the point is, there's a, there are lots of, lots of steps when writing math in this formal language that become kind of tedious and difficult. One of Leo de Mora's ideas for Lean is it would have these little helper programs called tactics, which will automate some of those repeated steps, those kind of things, steps that happen regularly in proofs.”