Rewriting arrows and paths along vertex equalities #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This files defines
path.cast (and associated lemmas) in order to allow
rewriting arrows and paths along equalities of their endpoints.
Rewriting arrows along equalities of vertices #
Change the endpoints of an arrow using equalities.
Rewriting paths along equalities of vertices #
Change the endpoints of a path using equalities.