Commit 2024-09-04 01:36 26750503

View on Github →

chore(Combinatorics/SimpleGraph): remove sndOfNotNil (#16352) Readd the refactorings to sndOfNotNil and tail The changes in 17b10a9d3d309648fbbad36a565603835fcef157 were accidentally reverted in 5025874dc5f9f8dd1598190e60ef20dda7b42566 This PR reintroduces the changes. The patch applied cleanly, except for some small conflict in Hamiltonian.lean which I fixed.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

modified theorem SimpleGraph.Walk.IsPath.tail

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.adj_getVert_one

deleted theorem SimpleGraph.Walk.adj_sndOfNotNil

deleted theorem SimpleGraph.Walk.cons_getVert

deleted theorem SimpleGraph.Walk.cons_getVert_succ

deleted theorem SimpleGraph.Walk.cons_sndOfNotNil

modified theorem SimpleGraph.Walk.cons_tail_eq

added def SimpleGraph.Walk.drop

added theorem SimpleGraph.Walk.getVert_cons

added theorem SimpleGraph.Walk.getVert_cons_one

added theorem SimpleGraph.Walk.getVert_cons_succ

added theorem SimpleGraph.Walk.getVert_copy

deleted theorem SimpleGraph.Walk.getVert_one

modified theorem SimpleGraph.Walk.getVert_tail

added theorem SimpleGraph.Walk.not_nil_iff_lt_length

deleted def SimpleGraph.Walk.sndOfNotNil

modified theorem SimpleGraph.Walk.support_tail

added theorem SimpleGraph.Walk.support_tail_of_not_nil

modified def SimpleGraph.Walk.tail

added theorem SimpleGraph.Walk.tail_cons_eq

added theorem SimpleGraph.Walk.tail_cons_nil

deleted theorem SimpleGraph.Walk.tail_support_eq_support_tail