[Merged by Bors] - chore: remove ported tactic from Mathport syntax

[adomani]

move_add, move_mul and move_oper are all available in Mathlib.

---

[github-actions]

PR summary a6570e0d20

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[grunweg]

Thanks for doing this! move_add and move_mul look good to me - but wasn't move_op renamed to move_oper?

[grunweg]

awaiting-author

[adomani]

It is called move_oper now, yes, but where should I report that?

[grunweg]

Good question! I don't know if there's a way to report that - if there isn't, I won't object to removing this as-is.

[grunweg]

Should perhaps mathport be tweaked, to emit move_oper instead of move_op?

[adomani]

I have not looked at mathport, but the only references to move_op that I could find in mathlib are the ones that I removed. The tactic was almost never used anyway, and probably really never in its move_op/move_oper form, so I do not think that it is a big deal if mathport converts it incorrectly.

I am going to re-label as awaiting-review, and maybe someone else can give an opinion as well!

[Ruben-VandeVelde]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style