Nudge porting `move_add`

Stream: mathlib4

[Damiano Testa]

Dear All,

a couple of weeks ago, docs#tactic.interactive.move_add was merged into mathlib.

I would like to port the tactic to mathlib4, but I am not really sure where to begin. Would anyone be willing to do a (short) pair programming session, where I can get started? I would be grateful for any time that anyone can share!

Thank you!