English
Let p be a walk from u to v and q a walk from v to w, with hx given. Then taking until x in the concatenated walk p.concat q equals taking until x in p with an adjusted membership: (p.append q).takeUntil x (subset_support_append_left _ _ hx) = p.takeUntil x hx.
Русский
Пусть p — пешеход от u к v, q — пешеход от v к w, и hx задано. Тогда взять до x в конкатенированном пешеходе p.concat q равно взять до x в p с поправкой на принадлежность: (p.append q).takeUntil x (subset_support_append_left _ _ hx) = p.takeUntil x hx.
LaTeX
$$$ (p.append q).takeUntil x (subset\_support\_append\_left \_ \_ hx) = p.takeUntil x hx $$$
Lean4
theorem takeUntil_append_of_mem_left {x : V} (p : G.Walk u v) (q : G.Walk v w) (hx : x ∈ p.support) :
(p.append q).takeUntil x (subset_support_append_left _ _ hx) = p.takeUntil _ hx := by
induction p with
| nil => rw [mem_support_nil_iff] at hx; subst_vars; simp
| @cons u _ _ _ _ ih =>
rw [support_cons] at hx
by_cases hxu : u = x
· subst_vars; simp
· have := List.mem_of_ne_of_mem (fun hf ↦ hxu hf.symm) hx
simp_rw [takeUntil_cons this hxu, cons_append, takeUntil_cons (subset_support_append_left _ _ this) hxu]
simpa using ih _ this
