English
If a path p has length n+1, then there exist a vertex c, an edge e: a→c, and a path q from c to b, with q.length = n, such that p = e.toPath.comp q.
Русский
Если путь p имеет длину n+1, то существует вершина c, ребро e: a→c и путь q: c→b длины n, такой что p = e.toPath.comp q.
LaTeX
$$$\\forall p:\\, \\mathrm{Path}(a,b),\\; \\exists c:\\, V,\\; \\exists e:\\, a\\to c,\\; \\exists q:\\, \\mathrm{Path}(c,b),\\; q.length = n \\land p = e^{\\toPath}.comp q.$$$
Lean4
theorem eq_toPath_comp_of_length_eq_succ (p : Path a b) {n : ℕ} (hp : p.length = n + 1) :
∃ (c : V) (f : a ⟶ c) (q : Quiver.Path c b) (_ : q.length = n), p = f.toPath.comp q := by
induction p generalizing n with
| nil => simp at hp
| @cons c d p q h =>
cases n
· rw [length_cons, Nat.zero_add, Nat.add_eq_right] at hp
obtain rfl := eq_of_length_zero p hp
obtain rfl := eq_nil_of_length_zero p hp
exact ⟨d, q, nil, rfl, rfl⟩
· rw [length_cons, Nat.add_right_cancel_iff] at hp
obtain ⟨x, q'', p'', hl, rfl⟩ := h hp
exact ⟨x, q'', p''.cons q, by simpa, rfl⟩
