The @[grind] tactic has to be the single most important addition to Lean in terms of it's growing popularity