mathlib3

706d88f2 - feat(combinatorics/quiver/*): More edge reversal constructions (#17665)

feat(combinatorics/quiver/*): More edge reversal constructions (#17665) Move * `quiver.symmetrify`, * `quiver.has_reverse`, * `quiver.has_involutive_reverse`, * `quiver.reverse`, * `quiver.path.reverse`, * `quiver.symmetrify.of`, * `quiver.lift`, * associated lemmas, from `combinatorics/quiver/connected_component.lean` to `combinatorics/quiver/symmetrify.lean`. Add * the class `prefunctor.map_reverse` witnessing that a prefunctor maps reverses to reverses, and change the lemmas taking this property as an explicit argument. * `prefunctor.symmetrify` mapping a prefunctor to the prefunctor between symmetrifications, * associated lemmas, to `combinatorics/quiver/symmetrify.lean`. Move `quiver.hom.to_pos` and `quiver.hom.to_neg` from `category_theory/groupoid/free_groupoid.lean` to `combinatorics/quiver/symmetrify.lean`. Add `map_reverse` instance for functors between groupoids. Co-authored-by: Rémi Bottinelli <bottine@users.noreply.github.com>