mathlib

e8b1a293 - feat(tactic/move_add, test/move_add): a tactic for moving around summands (#13483)

feat(tactic/move_add, test/move_add): a tactic for moving around summands (#13483) This PR introduces a tactic for moving summands of an expression. Individual terms can be named, also using pattern-matching, and moved to the beginning or to the end of the sum. #14228 shows a sample of golfing and usage of `move_add`, and the [diff](https://github.com/leanprover-community/mathlib/compare/aa_sort...adomani_move_add_random_golf) between them. #14618 contains the doc-string update to `ac_change`: I moved it to a separate PR to save CI cycles. See `compute_degree` in #14040 for a related tactic to compute `degree`s and `nat_degree`s of polynomials that uses `move_add`. ~~A future PR may add support for sorting also factors of a product, though this may happen after the switch to Lean4.~~ Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com>