mathlib

734c95f1 - feat(combinatorics/simple_graph/connectivity): walk.copy function to relax dependent type issues (#15764)

feat(combinatorics/simple_graph/connectivity): walk.copy function to relax dependent type issues (#15764) Walks in a graph present a special challenge since the endpoints of a walk appear as type indices, leading to a constant struggle with dependent types and strict definitional equality. This commit introduces a `walk.copy` function to be able to change the definitions of a walk's endpoints. There are also many simp lemmas to push the copy function out of most expressions. An example of a lemma that `copy` lets us express: ```lean lemma map_eq_of_eq {f : G →g G'} (f' : G →g G') (h : f = f') : p.map f = (p.map f').copy (by rw h) (by rw h) ``` Thanks to @**Junyan Xu|224323** for the idea.