Lean4
theorem aux [DecidableEq V] {u v w : V} (hb : ∀ p : G.Walk v w, s(v, w) ∈ p.edges) (c : G.Walk u u) (hc : c.IsTrail)
(he : s(v, w) ∈ c.edges) (hw : w ∈ (c.takeUntil v (c.fst_mem_support_of_mem_edges he)).support) : False :=
by
have hv := c.fst_mem_support_of_mem_edges he
let puw := (c.takeUntil v hv).takeUntil w hw
let pwv := (c.takeUntil v hv).dropUntil w hw
let pvu := c.dropUntil v hv
have : c = (puw.append pwv).append pvu := by
simp [puw, pwv, pvu]
-- We have two walks from v to w
-- pvu puw
-- v ----> u ----> w
-- | ^
-- `-------------'
-- pwv.reverse
-- so they both contain the edge s(v, w), but that's a contradiction since c is a trail.
have hbq := hb (pvu.append puw)
have hpq' := hb pwv.reverse
rw [Walk.edges_reverse, List.mem_reverse] at hpq'
rw [Walk.isTrail_def, this, Walk.edges_append, Walk.edges_append, List.nodup_append_comm, ← List.append_assoc, ←
Walk.edges_append] at hc
exact List.disjoint_of_nodup_append hc hbq hpq'
