English
If a vertex v occurs in p.vertices, there exist p1: a→v and p2: v→b with p = p1 ∘ p2 and v not in the tail of p2.vertices.
Русский
Если вершина v встречается в p.vertices, тогда существует разбиение p = p1 ∘ p2 с требованием, чтобы v не входила в хвост p2.vertices.
LaTeX
$$$v \in p.vertices \Rightarrow \exists p_1 : Path\ a\ v, \exists p_2 : Path\ v\ b,\; p = p_1.comp p_2 ∧ v \notin p_2.vertices.tail$$$
Lean4
/-- Split a path at the *last* occurrence of a vertex. -/
theorem exists_eq_comp_and_notMem_tail_of_mem_vertices {v : V} (hv : v ∈ p.vertices) :
∃ (p₁ : Path a v) (p₂ : Path v b), p = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail := by
induction p with
| nil =>
have hxa : v = a := by simpa [vertices_nil, List.mem_singleton] using hv
subst hxa
exact
⟨Path.nil, Path.nil, by simp only [comp_nil], by
simp only [vertices_nil, tail_cons, not_mem_nil, not_false_eq_true]⟩
| cons pPrev e
ih =>
have hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end := by simpa using (mem_vertices_cons pPrev e).1 hv
have h_case₁ :
v = (pPrev.cons e).end →
∃ (p₁ : Path a v) (p₂ : Path v (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail :=
by
rintro rfl
exact ⟨pPrev.cons e, Path.nil, by simp [comp_nil], by simp [vertices_nil]⟩
have h_case₂ :
v ∈ pPrev.vertices →
v ≠ (pPrev.cons e).end →
∃ (p₁ : Path a v) (p₂ : Path v (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail :=
by
intro hxPrev hxe_ne
obtain ⟨q₁, q₂, h_prev, h_not_tail⟩ := ih hxPrev
let q₂' : Path v (pPrev.cons e).end := q₂.cons e
have h_no_tail : v ∉ q₂'.vertices.tail := by
intro hmem
have hmem' : v ∈ (q₂.vertices ++ [(pPrev.cons e).end]).tail := by
simpa [q₂', vertices_cons, concat_eq_append] using hmem
cases hq2 : q₂.vertices with
| nil => simp [hq2] at hmem'
| cons y ys =>
have hx_in : v ∈ ys ++ [(pPrev.cons e).end] := by simpa [hq2] using hmem'
obtain (hx_ys | hx_last) := List.mem_append.mp hx_in
· exact h_not_tail <| by simpa [hq2]
· have : v = (pPrev.cons e).end := by simpa [List.mem_singleton] using hx_last
exact hxe_ne this
exact ⟨q₁, q₂', by simp [q₂', h_prev], h_no_tail⟩
cases hv' with
| inl h_in_prefix =>
by_cases h_eq_end : v = (pPrev.cons e).end
· exact h_case₁ h_eq_end
· exact h_case₂ h_in_prefix h_eq_end
| inr h_eq_end => exact h_case₁ h_eq_end
