Autocomplete/actions for Wingman's tactic block

[Ailrun]

It would be great if we don't need to remember the names of Wingman's tactics, using autocompletion or actions activated only in Wingman's tactic blocks.

For example, when we have

foo :: Int -> Int
foo = (+) 1

bar :: Int
bar = [wingman| · |]

(where · is the position of the cursor) we may get either

1. Autocompletion
   With apply, application, use, ... (listing only applicable tactics if possible)
2. Actions
   Like add 'apply' in tactic block, add 'use' in tactic block, ... (likewise, only applicable if possible)

[isovector]

It's a good idea, but I don't think I'll prioritize this. It sounds a lot like dealing with LSP, which I try to avoid as hard as possible :) PRs very welcome though!