-- Mathlib/Combinatorics/Quiver/Path.lean
lemma 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

Proof state:
case cons
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n : ℕ
hp : (p.cons q).length = n + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
cases n

Result:
case cons.zero
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
hp : (p.cons q).length = 0 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : (p.cons q).length = n✝ + 1 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Proof state:
case cons.succ.intro.intro.intro.intro
V : Type u
inst✝ : Quiver V
a b c d : V
q : c ⟶ d
n✝ : ℕ
x : V
q'' : a ⟶ x
p'' : Path x c
hl : p''.length = n✝
h : ∀ {n : ℕ}, (q''.toPath.comp p'').length = n + 1 → ∃ c_1 f q x_1, q''.toPath.comp p'' = f.toPath.comp q
hp : (q''.toPath.comp p'').length = n✝ + 1
⊢ ∃ c_1 f q_1 x_1, (q''.toPath.comp p'').cons q = f.toPath.comp q_1

Tactic:
exact ⟨x, q'', p''.cons q, by simpa, rfl⟩

Result:
no goals

Proof state:
case cons.zero
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
hp : (p.cons q).length = 0 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
rw [length_cons, Nat.zero_add, Nat.add_left_eq_self] at hp

Result:
case cons.zero
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
hp : p.length = 0
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Proof state:
V : Type u
inst✝ : Quiver V
a b c d : V
q : c ⟶ d
n✝ : ℕ
x : V
q'' : a ⟶ x
p'' : Path x c
hl : p''.length = n✝
h : ∀ {n : ℕ}, (q''.toPath.comp p'').length = n + 1 → ∃ c_1 f q x_1, q''.toPath.comp p'' = f.toPath.comp q
hp : (q''.toPath.comp p'').length = n✝ + 1
⊢ (p''.cons q).length = n✝ + 1

Tactic:
simpa

Result:
no goals

Proof state:
case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : p.length = n✝ + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
obtain ⟨x, q'', p'', hl, rfl⟩ := h hp

Result:
case cons.succ.intro.intro.intro.intro
V : Type u
inst✝ : Quiver V
a b c d : V
q : c ⟶ d
n✝ : ℕ
x : V
q'' : a ⟶ x
p'' : Path x c
hl : p''.length = n✝
h : ∀ {n : ℕ}, (q''.toPath.comp p'').length = n + 1 → ∃ c_1 f q x_1, q''.toPath.comp p'' = f.toPath.comp q
hp : (q''.toPath.comp p'').length = n✝ + 1
⊢ ∃ c_1 f q_1 x_1, (q''.toPath.comp p'').cons q = f.toPath.comp q_1

Proof state:
case cons.zero
V : Type u
inst✝ : Quiver V
a b d : V
q : a ⟶ d
h : ∀ {n : ℕ}, nil.length = n + 1 → ∃ c f q x, nil = f.toPath.comp q
hp : nil.length = 0
⊢ ∃ c f q_1 x, nil.cons q = f.toPath.comp q_1

Tactic:
exact ⟨d, q, nil, rfl, rfl⟩

Result:
no goals

Proof state:
case cons.zero
V : Type u
inst✝ : Quiver V
a b d : V
p : Path a a
q : a ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c f q x, p = f.toPath.comp q
hp : p.length = 0
⊢ ∃ c f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
obtain rfl := eq_nil_of_length_zero p hp

Result:
case cons.zero
V : Type u
inst✝ : Quiver V
a b d : V
q : a ⟶ d
h : ∀ {n : ℕ}, nil.length = n + 1 → ∃ c f q x, nil = f.toPath.comp q
hp : nil.length = 0
⊢ ∃ c f q_1 x, nil.cons q = f.toPath.comp q_1

Proof state:
case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : (p.cons q).length = n✝ + 1 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
rw [length_cons, Nat.add_right_cancel_iff] at hp

Result:
case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : p.length = n✝ + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Proof state:
case nil
V : Type u
inst✝ : Quiver V
a b : V
n : ℕ
hp : nil.length = n + 1
⊢ ∃ c f q x, nil = f.toPath.comp q

Tactic:
simp at hp

Result:
no goals

Proof state:
case cons.zero
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
hp : p.length = 0
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
obtain rfl := eq_of_length_zero p hp

Result:
case cons.zero
V : Type u
inst✝ : Quiver V
a b d : V
p : Path a a
q : a ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c f q x, p = f.toPath.comp q
hp : p.length = 0
⊢ ∃ c f q_1 x, p.cons q = f.toPath.comp q_1