Commit 2025-11-20 11:57 35a1d502

View on Github →

feat: turn a closed walk into a cycle (#31217) From the ProofBench workshop Closes #23637, which does the same thing under a stronger hypothesis on the starting closed walk.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

added theorem SimpleGraph.Walk.IsTrail.isCycle_cycleBypass

modified theorem SimpleGraph.Walk.bypass_copy

modified theorem SimpleGraph.Walk.bypass_eq_self_of_length_le

modified theorem SimpleGraph.Walk.bypass_isPath

deleted theorem SimpleGraph.Walk.cons_isTrail_iff

added def SimpleGraph.Walk.cycleBypass

added theorem SimpleGraph.Walk.cycleBypass_nil

modified theorem SimpleGraph.Walk.darts_bypass_subset

modified theorem SimpleGraph.Walk.darts_toPath_subset

modified theorem SimpleGraph.Walk.edges_bypass_subset

added theorem SimpleGraph.Walk.edges_cycleBypass_subset

modified theorem SimpleGraph.Walk.edges_toPath_subset

added theorem SimpleGraph.Walk.isTrail_cons

modified theorem SimpleGraph.Walk.length_bypass_le

modified theorem SimpleGraph.Walk.support_bypass_subset

modified theorem SimpleGraph.Walk.support_toPath_subset

modified def SimpleGraph.Walk.toPath

Modified Mathlib/Combinatorics/SimpleGraph/Trails.lean

Modified Mathlib/Tactic/GCongr/CoreAttrs.lean