[Merged by Bors] - chore(Tactic): rewrite order tactic docstring#37927

Vierkantor wants to merge 3 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

Vierkantor:document-order-tacticVierkantor/mathlib4:document-order-tacticCopy head branch name to clipboard