awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
h : p.vertices ≠ []
⊢ p.vertices.head h = a
have nil : ∀ (h : Ne.{u_1 + 1} (α := List V) (vertices.{u_1, u_2} (a := a) nil) []), head (vertices.{u_1, u_2} (a := a) nil) h = a
Tactic: induction p with
  | nil => simp only [vertices_nil, head_cons]
  | cons p' _ ih => simp [head_append_of_ne_nil (vertices_ne_nil p'), ih]
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
h : p.vertices ≠ []
nil :
  ∀ (h : Ne.{u_1 + 1} (α := List V) (vertices.{u_1, u_2} (a := a) Path.nil) []),
    head (vertices.{u_1, u_2} (a := a) Path.nil) h = a
⊢ p.vertices.head h = a
have cons : ∀ {b c : V} (p' : Path.{u_2, u_1} a b) (a_1 : b ⟶ c) (ih : ∀ (h : p'.vertices ≠ []), p'.vertices.head h = a)
  (h : (p'.cons a_1).vertices ≠ []), (p'.cons a_1).vertices.head h = a
Tactic: induction p with
  | nil => simp only [vertices_nil, head_cons]
  | cons p' _ ih => simp [head_append_of_ne_nil (vertices_ne_nil p'), ih]
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices 0 ⋯ = a
have nil : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (vertices.{u_1, u_2} (a := a) nil) 0 sorry = a
Tactic: induction p with
  | nil => simp
  | cons p' e ih => simp [ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
nil : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (vertices.{u_1, u_2} (a := a) Path.nil) 0 ⋯ = a
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices 0 ⋯ = a
have cons : ∀ {b c : V} (p' : Path.{u_2, u_1} a b) (e : b ⟶ c)
  (ih : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p'.vertices 0 sorry = a),
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (p'.cons e).vertices 0 sorry = a
Tactic: induction p with
  | nil => simp
  | cons p' e ih => simp [ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
h : p.vertices ≠ []
⊢ p.vertices.getLast h = b
have nil : ∀ (h : Ne.{u_1 + 1} (α := List V) (vertices.{u_1, u_2} (a := a) nil) []),
  getLast (vertices.{u_1, u_2} (a := a) nil) h = a
Tactic: induction p with
  | nil => simp only [vertices_nil, getLast_singleton]
  | cons p' e ih => simp
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
h : p.vertices ≠ []
nil :
  ∀ (h : Ne.{u_1 + 1} (α := List V) (vertices.{u_1, u_2} (a := a) Path.nil) []),
    getLast (vertices.{u_1, u_2} (a := a) Path.nil) h = a
⊢ p.vertices.getLast h = b
have cons : ∀ {b c : V} (p' : Path.{u_2, u_1} a b) (e : b ⟶ c) (ih : ∀ (h : p'.vertices ≠ []), p'.vertices.getLast h = b)
  (h : (p'.cons e).vertices ≠ []), (p'.cons e).vertices.getLast h = c
Tactic: induction p with
  | nil => simp only [vertices_nil, getLast_singleton]
  | cons p' e ih => simp
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
⊢ p.vertices.dropLast ++ [b] = p.vertices
have simp_rw : p.vertices.dropLast ++ [p.vertices.getLast sorry] = p.vertices
Tactic: simp_rw [← p.vertices_getLast p.vertices_ne_nil, dropLast_concat_getLast]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b c : V
p : Path.{u_2, u_1} a b
q : Path.{u_2, u_1} b c
⊢ (p.comp q).vertices = p.vertices.dropLast ++ q.vertices
have nil : (p.comp nil).vertices = p.vertices.dropLast ++ vertices.{u_1, u_2} (a := b) nil
Tactic: induction q with
  | nil => simp
  | cons q' e ih => simp [ih]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b c : V
p : Path.{u_2, u_1} a b
q : Path.{u_2, u_1} b c
nil : (p.comp Path.nil).vertices = p.vertices.dropLast ++ vertices.{u_1, u_2} (a := b) Path.nil
⊢ (p.comp q).vertices = p.vertices.dropLast ++ q.vertices
have cons : ∀ {b_1 c : V} (q' : Path.{u_2, u_1} b b_1) (e : b_1 ⟶ c)
  (ih : (p.comp q').vertices = p.vertices.dropLast ++ q'.vertices),
  (p.comp (q'.cons e)).vertices = p.vertices.dropLast ++ (q'.cons e).vertices
Tactic: induction q with
  | nil => simp
  | cons q' e ih => simp [ih]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a : V
p : Path.{u_2, u_1} a a
⊢ p.length = 0 ↔ p = nil
have nil : length.{u_1, u_2} (V := V) (a := a) nil = 0 ↔ Eq (α := Path.{u_2, u_1} a a) nil nil
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a : V
p : Path.{u_2, u_1} a a
nil : length.{u_1, u_2} (V := V) (a := a) Path.nil = 0 ↔ Eq (α := Path.{u_2, u_1} a a) Path.nil Path.nil
⊢ p.length = 0 ↔ p = Path.nil
have cons : ∀ {b : V} (a_1 : Path.{u_2, u_1} a b) (a_2 : b ⟶ a), (a_1.cons a_2).length = 0 ↔ a_1.cons a_2 = Path.nil
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a : V
⊢ length.{u_1, u_2} (V := V) (a := a) nil = 0 ↔ Eq (α := Path.{u_2, u_1} a a) nil nil
have nil : length.{u_1, u_2} (V := V) (a := a) nil = 0 → Eq (α := Path.{u_2, u_1} a a) nil nil
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a : V
nil : length.{u_1, u_2} (V := V) (a := a) Path.nil = 0 → Eq (α := Path.{u_2, u_1} a a) Path.nil Path.nil
⊢ length.{u_1, u_2} (V := V) (a := a) Path.nil = 0 ↔ Eq (α := Path.{u_2, u_1} a a) Path.nil Path.nil
have nil₁ : Eq (α := Path.{u_2, u_1} a a) Path.nil Path.nil → length.{u_1, u_2} (V := V) (a := a) Path.nil = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
a_1 : Path.{u_2, u_1} a b
a_2 : b ⟶ a
⊢ (a_1.cons a_2).length = 0 ↔ a_1.cons a_2 = nil
have cons : (a_1.cons a_2).length = 0 → a_1.cons a_2 = nil
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
a_1 : Path.{u_2, u_1} a b
a_2 : b ⟶ a
cons : (a_1.cons a_2).length = 0 → a_1.cons a_2 = nil
⊢ (a_1.cons a_2).length = 0 ↔ a_1.cons a_2 = nil
have cons₁ : a_1.cons a_2 = nil → (a_1.cons a_2).length = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
q : Path.{u_2, u_1} b a
h : p.comp q = nil
⊢ p.length = 0
have hlen : (p.comp q).length = 0
Tactic: have hlen : (p.comp q).length = 0 := by
    simpa using congrArg Path.length h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
q : Path.{u_2, u_1} b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
⊢ p.length = 0
have this : p.length + q.length = 0
Tactic: have : p.length + q.length = 0 := by
    simpa [length_comp] using hlen
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
q : Path.{u_2, u_1} b a
h : p.comp q = nil
⊢ q.length = 0
have hlen : (p.comp q).length = 0
Tactic: have hlen : (p.comp q).length = 0 := by
    simpa using congrArg Path.length h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
q : Path.{u_2, u_1} b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
⊢ q.length = 0
have this : p.length + q.length = 0
Tactic: have : p.length + q.length = 0 := by
    simpa [length_comp] using hlen
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
q : Path.{u_2, u_1} b a
⊢ p.comp q = nil ↔ p.length = 0 ∧ q.length = 0
have refine : p.length = 0 ∧ q.length = 0 → ∀ (hp : p.length = 0) (hq : q.length = 0), p.comp q = nil
Tactic: refine ⟨fun h ↦ ⟨nil_of_comp_eq_nil_left h, nil_of_comp_eq_nil_right h⟩, fun ⟨hp, hq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
q : Path.{u_2, u_1} b a
h : p.length = 0 ∧ q.length = 0
hp : p.length = 0
hq : q.length = 0
⊢ p.comp q = nil
have nil : ∀ {q : Path.{u_2, u_1} a a},
  length.{u_1, u_2} (V := V) (a := a) nil = 0 ∧ q.length = 0 →
    ∀ (hp : length.{u_1, u_2} (V := V) (a := a) nil = 0) (hq : q.length = 0), comp nil q = nil
Tactic: induction p with
  | nil => simpa using (length_eq_zero_iff q).mp hq
  | cons p' _ ihp => simp at hp
Cleared hypotheses: p, q, h, hp, hq
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
q : Path.{u_2, u_1} b a
h : p.length = 0 ∧ q.length = 0
hp : p.length = 0
hq : q.length = 0
nil :
  ∀ {q : Path.{u_2, u_1} a a},
    length.{u_1, u_2} (V := V) (a := a) Path.nil = 0 ∧ q.length = 0 →
      ∀ (hp : length.{u_1, u_2} (V := V) (a := a) Path.nil = 0) (hq : q.length = 0), comp Path.nil q = Path.nil
⊢ p.comp q = Path.nil
have cons : ∀ {b c : V} (p' : Path.{u_2, u_1} a b) (a_1 : b ⟶ c)
  (ihp :
    ∀ {q : Path.{u_2, u_1} b a},
      p'.length = 0 ∧ q.length = 0 → ∀ (hp : p'.length = 0) (hq : q.length = 0), p'.comp q = Path.nil)
  {q : Path.{u_2, u_1} c a},
  (p'.cons a_1).length = 0 ∧ q.length = 0 →
    ∀ (hp : (p'.cons a_1).length = 0) (hq : q.length = 0), (p'.cons a_1).comp q = Path.nil
Tactic: induction p with
  | nil => simpa using (length_eq_zero_iff q).mp hq
  | cons p' _ ihp => simp at hp
Cleared hypotheses: p, q, h, hp, hq
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
⊢ b ∈ p.vertices
have h₁ : p.vertices.getLast sorry = b
Tactic: have h₁ : p.vertices.getLast (vertices_ne_nil p) = b :=
    vertices_getLast p (vertices_ne_nil p)
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
h₁ : p.vertices.getLast ⋯ = b
⊢ b ∈ p.vertices
have h₂ : p.vertices.getLast sorry ∈ p.vertices
Tactic: have h₂ := getLast_mem (l := p.vertices) (vertices_ne_nil p)
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
n : ℕ
hn : n ≤ length.{u_1, u_2} (V := V) (a := a) nil
⊢ ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v a), nil = p₁.comp p₂ ∧ p₁.length = n
have nil : ∀ (hn : 0 ≤ length.{u_1, u_2} (V := V) (a := a) nil),
  ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v a), nil = p₁.comp p₂ ∧ p₁.length = 0
Tactic: obtain ⟨rfl⟩ : n = 0 := by simpa using hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
b_1 c : V
p' : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih :
  ∀ {n : ℕ} (hn : n ≤ p'.length),
    ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b_1), p' = p₁.comp p₂ ∧ p₁.length = n
n : ℕ
hn : n ≤ (p'.cons e).length
⊢ ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), p'.cons e = p₁.comp p₂ ∧ p₁.length = n
have hn₁ : n ≤ p'.length + 1
Tactic: rw [length_cons] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
b_1 c : V
p' : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih :
  ∀ {n : ℕ} (hn : n ≤ p'.length),
    ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b_1), p' = p₁.comp p₂ ∧ p₁.length = n
n : ℕ
hn : n ≤ p'.length + 1
⊢ ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), p'.cons e = p₁.comp p₂ ∧ p₁.length = n
have cons : ∀ (h : n ≤ p'.length),
  ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), p'.cons e = p₁.comp p₂ ∧ p₁.length = n
Tactic: rcases (Nat.le_succ_iff).1 hn with h | rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
b_1 c : V
p' : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih :
  ∀ {n : ℕ} (hn : n ≤ p'.length),
    ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b_1), p' = p₁.comp p₂ ∧ p₁.length = n
n : ℕ
hn : n ≤ p'.length + 1
cons :
  ∀ (h : n ≤ p'.length),
    ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), p'.cons e = p₁.comp p₂ ∧ p₁.length = n
⊢ ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), p'.cons e = p₁.comp p₂ ∧ p₁.length = n
have cons₁ : ∀ (hn : p'.length.succ ≤ p'.length + 1),
  ∃ (v : V),
    ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), p'.cons e = p₁.comp p₂ ∧ p₁.length = p'.length.succ
Tactic: rcases (Nat.le_succ_iff).1 hn with h | rfl
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
b_1 c : V
p' : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih :
  ∀ {n : ℕ} (hn : n ≤ p'.length),
    ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b_1), p' = p₁.comp p₂ ∧ p₁.length = n
n : ℕ
hn : n ≤ p'.length + 1
h : n ≤ p'.length
⊢ ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), p'.cons e = p₁.comp p₂ ∧ p₁.length = n
have cons : ∀ (d : V) (p₁ : Path.{u_2, u_1} a d) (p₂ : Path.{u_2, u_1} d b_1) (hp : p' = p₁.comp p₂) (hl : p₁.length = n),
  ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), p'.cons e = p₁.comp p₂ ∧ p₁.length = n
Tactic: obtain ⟨d, p₁, p₂, hp, hl⟩ := ih h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
n : ℕ
hn : n ≤ p.length
⊢ ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp p₂ ∧ p₁.length = n
have nil : ∀ {n : ℕ} (hn : n ≤ length.{u_1, u_2} (V := V) (a := a) nil),
  ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v a), nil = p₁.comp p₂ ∧ p₁.length = n
Tactic: induction p generalizing n with
  | nil =>
    obtain ⟨rfl⟩ : n = 0 := by simpa using hn
    exact ⟨a, Path.nil, Path.nil, by simp, rfl⟩
  | @cons _ c p' e ih =>
    rw [length_cons] at hn
    rcases (Nat.le_succ_iff).1 hn with h | rfl
    · obtain ⟨d, p₁, p₂, hp, hl⟩ := ih h
      exact ⟨d, p₁, p₂.cons e, by simp [hp], hl⟩
    · exact ⟨c, p'.cons e, Path.nil, by simp, by simp⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
n : ℕ
hn : n ≤ p.length
nil :
  ∀ {n : ℕ} (hn : n ≤ length.{u_1, u_2} (V := V) (a := a) Path.nil),
    ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v a), Path.nil = p₁.comp p₂ ∧ p₁.length = n
⊢ ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp p₂ ∧ p₁.length = n
have cons : ∀ {b c : V} (p' : Path.{u_2, u_1} a b) (e : b ⟶ c)
  (ih :
    ∀ {n : ℕ} (hn : n ≤ p'.length),
      ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b), p' = p₁.comp p₂ ∧ p₁.length = n)
  {n : ℕ} (hn : n ≤ (p'.cons e).length),
  ∃ (v : V), ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), p'.cons e = p₁.comp p₂ ∧ p₁.length = n
Tactic: induction p generalizing n with
  | nil =>
    obtain ⟨rfl⟩ : n = 0 := by simpa using hn
    exact ⟨a, Path.nil, Path.nil, by simp, rfl⟩
  | @cons _ c p' e ih =>
    rw [length_cons] at hn
    rcases (Nat.le_succ_iff).1 hn with h | rfl
    · obtain ⟨d, p₁, p₂, hp, hl⟩ := ih h
      exact ⟨d, p₁, p₂.cons e, by simp [hp], hl⟩
    · exact ⟨c, p'.cons e, Path.nil, by simp, by simp⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
n : ℕ
hn : n < p.vertices.length
⊢ n ≤ p.length
have hn₁ : n < p.length + 1
Tactic: rw [vertices_length] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
n : ℕ
hn : n < p.vertices.length
⊢ ∃ (v : V),
    ∃ (p₁ : Path.{u_2, u_1} a v),
      ∃ (p₂ : Path.{u_2, u_1} v b),
        p = p₁.comp p₂ ∧
          p₁.length = n ∧ v = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn
have hn_le_len : n ≤ p.length
Tactic: have hn_le_len : n ≤ p.length := by
    rw [vertices_length] at hn
    exact Nat.le_of_lt_succ hn
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
n : ℕ
hn : n < p.vertices.length
hn_le_len : n ≤ p.length
⊢ ∃ (v : V),
    ∃ (p₁ : Path.{u_2, u_1} a v),
      ∃ (p₂ : Path.{u_2, u_1} v b),
        p = p₁.comp p₂ ∧
          p₁.length = n ∧ v = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn
have obtain : ∀ (v : V) (p₁ : Path.{u_2, u_1} a v) (p₂ : Path.{u_2, u_1} v b) (hn : p₁.length < (p₁.comp p₂).vertices.length)
  (hn_le_len : p₁.length ≤ (p₁.comp p₂).length),
  ∃ (v_1 : V),
    ∃ (p₁_1 : Path.{u_2, u_1} a v_1),
      ∃ (p₂_1 : Path.{u_2, u_1} v_1 b),
        p₁.comp p₂ = p₁_1.comp p₂_1 ∧
          p₁_1.length = p₁.length ∧
            v_1 = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (p₁.comp p₂).vertices p₁.length hn
Tactic: obtain ⟨v, p₁, p₂, rfl, rfl⟩ := p.exists_eq_comp_of_le_length hn_le_len
Cleared hypotheses: p, n, hn, hn_le_len
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
v : V
hv : v ∈ p.vertices
⊢ ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp p₂
have obtain : ∀ (n : ℕ) (hn : n < p.vertices.length)
  (hv : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn ∈ p.vertices),
  ∃ (p₁ : Path.{u_2, u_1} a (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn)),
    ∃ (p₂ : Path.{u_2, u_1} (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn) b),
      p = p₁.comp p₂
Tactic: obtain ⟨n, hn, rfl⟩ : ∃ n, ∃ hn : n < p.vertices.length, v = p.vertices[n] :=
    exists_mem_iff_getElem.mp ⟨v, hv, rfl⟩
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
n : ℕ
hn : n < p.vertices.length
hv : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn ∈ p.vertices
⊢ ∃ (p₁ : Path.{u_2, u_1} a (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn)),
    ∃ (p₂ : Path.{u_2, u_1} (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn) b),
      p = p₁.comp p₂
have obtain : ∀ (p₁ : Path.{u_2, u_1} a (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn))
  (p₂ : Path.{u_2, u_1} (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn) b)
  (hp : p = p₁.comp p₂) (hv : p₁.length = n),
  ∃ (p₁ : Path.{u_2, u_1} a (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn)),
    ∃ (p₂ : Path.{u_2, u_1} (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn) b),
      p = p₁.comp p₂
Tactic: obtain ⟨v, p₁, p₂, hp, hv, rfl⟩ := p.exists_eq_comp_and_length_eq_of_lt_length n hn
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
v : V
hv : Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := a) nil) v
⊢ ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v a), nil = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
have hxa : v = a
Tactic: have hxa : v = a := by
      simpa [vertices_nil, List.mem_singleton] using hv
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
v : V
hv : Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := a) nil) v
hxa : v = a
⊢ ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v a), nil = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
have nil : ∀ (p : Path.{u_2, u_1} v b) (hv : Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := v) nil) v),
  ∃ (p₁ : Path.{u_2, u_1} v v), ∃ (p₂ : Path.{u_2, u_1} v v), nil = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
Tactic: subst hxa
Cleared hypotheses: a, p, hv, hxa
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
v b_1 c : V
pPrev : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih :
  ∀ (hv : v ∈ pPrev.vertices),
    ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b_1), pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
⊢ ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
have hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
Tactic: have hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end := by
      simpa using (mem_vertices_cons pPrev e).1 hv
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
v b_1 c : V
pPrev : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih :
  ∀ (hv : v ∈ pPrev.vertices),
    ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b_1), pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
⊢ ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
have h_case₁ : v = (pPrev.cons e).end →
  ∃ (p₁ : Path.{u_2, u_1} a v),
    ∃ (p₂ : Path.{u_2, u_1} v (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
Tactic: 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]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
v b_1 c : V
pPrev : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih :
  ∀ (hv : v ∈ pPrev.vertices),
    ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b_1), pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ :
  v = (pPrev.cons e).end →
    ∃ (p₁ : Path.{u_2, u_1} a v),
      ∃ (p₂ : Path.{u_2, u_1} v (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hxPrev : v ∈ pPrev.vertices
hxe_ne : v ≠ (pPrev.cons e).end
⊢ ∃ (p₁ : Path.{u_2, u_1} a v),
    ∃ (p₂ : Path.{u_2, u_1} v (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
have obtain : ∀ (q₁ : Path.{u_2, u_1} a v) (q₂ : Path.{u_2, u_1} v b_1) (h_prev : pPrev = q₁.comp q₂)
  (h_not_tail : ¬v ∈ q₂.vertices.tail),
  ∃ (p₁ : Path.{u_2, u_1} a v),
    ∃ (p₂ : Path.{u_2, u_1} v (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
Tactic: obtain ⟨q₁, q₂, h_prev, h_not_tail⟩ := ih hxPrev