awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b 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 = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (p₁.comp p₂).vertices p₁.length hn

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b 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:
exact ⟨v, p₁, p₂, rfl, rfl, by simp⟩
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
⊢ ∃ (n : ℕ),
    ∃ (hn : n < p.vertices.length), v = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices n hn

Tactic:
exists_mem_iff_getElem.mp ⟨v, hv, rfl⟩

Premises used: List.exists_mem_iff_getElem, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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₂
⊢ ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v 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⟩

Premises used: List.exists_mem_iff_getElem, And.intro, Exists.intro, Iff.mp, List.length, rfl, Quiver.Path.vertices
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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₂
⊢ ∃ (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

Premises used: Quiver.Path.exists_eq_comp_and_length_eq_of_lt_length, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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_1 : 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
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:
⟨p₁, p₂, hp⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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_1 : 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
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:
exact ⟨p₁, p₂, hp⟩
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
⊢ v = a

Tactic:
simpa [vertices_nil, List.mem_singleton] using hv

Premises used: List.mem_singleton, Quiver.Path.vertices_nil
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
⊢ v = a

Tactic:
have hxa : v = a := by
      simpa [vertices_nil, List.mem_singleton] using hv
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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) Path.nil) v
hxa : v = a
nil :
  ∀ (p : Path.{u_2, u_1} v b) (hv : Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := v) Path.nil) v),
    ∃ (p₁ : Path.{u_2, u_1} v v), ∃ (p₂ : Path.{u_2, u_1} v v), Path.nil = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
⊢ ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v a), Path.nil = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
subst hxa
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
b v : V
p : Path.{u_2, u_1} v b
hv : Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := v) nil) v
⊢ Eq (α := Path.{u_2, u_1} v v) nil (comp nil nil)

Tactic:
simp only [comp_nil]

Premises used: Quiver.Path.comp_nil
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
b v : V
p : Path.{u_2, u_1} v b
hv : Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := v) nil) v
⊢ ¬Membership.mem (γ := List V) (tail (vertices.{u_1, u_2} (a := v) nil)) v

Tactic:
simp only [vertices_nil, tail_cons, not_mem_nil, not_false_eq_true]

Premises used: List.tail_cons, not_false_eq_true, Quiver.Path.vertices_nil, List.not_mem_nil
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
b v : V
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:
exact ⟨Path.nil, Path.nil, by simp only [comp_nil],
      by simp only [vertices_nil, tail_cons, not_mem_nil, not_false_eq_true]⟩
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
⊢ v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end

Tactic:
simpa using (mem_vertices_cons pPrev e).1 hv

Premises used: Iff.mp, Quiver.Path.mem_vertices_cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
⊢ 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
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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 : V
pPrev : Path.{u_2, u_1} a b_1
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
e : b_1 ⟶ v
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
⊢ pPrev.cons e = (pPrev.cons e).comp nil

Tactic:
simp [comp_nil]

Premises used: Quiver.Path.comp_nil
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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 : V
pPrev : Path.{u_2, u_1} a b_1
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
e : b_1 ⟶ v
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
⊢ ¬Membership.mem (γ := List V) (tail (vertices.{u_1, u_2} (a := v) nil)) v

Tactic:
simp [vertices_nil]

Premises used: Quiver.Path.vertices_nil
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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 : V
pPrev : Path.{u_2, u_1} a b_1
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
e : b_1 ⟶ v
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 (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
exact ⟨pPrev.cons e, Path.nil, by simp [comp_nil], by simp [vertices_nil]⟩
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
⊢ 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]⟩
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
⊢ ∃ (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
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
q₂' : Path.{u_2, u_1} v (pPrev.cons e).end := q₂.cons e
⊢ ¬v ∈ q₂'.vertices.tail

Tactic:
grind [vertices_cons, end_cons]

Premises used: Quiver.Path.vertices_cons, Quiver.Path.end_cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
q₂' : Path.{u_2, u_1} v (pPrev.cons e).end := q₂.cons e
⊢ ¬v ∈ q₂'.vertices.tail

Tactic:
have h_no_tail : v ∉ q₂'.vertices.tail := by grind [vertices_cons, end_cons]
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
q₂' : Path.{u_2, u_1} v (pPrev.cons e).end := q₂.cons e
h_no_tail : ¬v ∈ q₂'.vertices.tail
⊢ pPrev.cons e = q₁.comp q₂'

Tactic:
simp [q₂', h_prev]
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
q₂' : Path.{u_2, u_1} v (pPrev.cons e).end := q₂.cons e
h_no_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:
exact ⟨q₁, q₂', by simp [q₂', h_prev], h_no_tail⟩
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
⊢ v ∈ pPrev.vertices →
    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.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 grind [vertices_cons, end_cons]
      exact ⟨q₁, q₂', by simp [q₂', h_prev], h_no_tail⟩
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
h_case₂ :
  v ∈ pPrev.vertices →
    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
h_in_prefix : v ∈ pPrev.vertices
pos :
  ∀ (h_eq_end : 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
neg :
  ∀ (h_eq_end : ¬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
⊢ ∃ (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

Tactic:
by_cases h_eq_end : v = (pPrev.cons e).end

Premises used: Quiver.Path.cons, Quiver.Path.end
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
h_case₂ :
  v ∈ pPrev.vertices →
    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
h_in_prefix : v ∈ pPrev.vertices
h_eq_end : 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

Tactic:
h_case₁ h_eq_end

Premises used: Quiver.Path.end
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
h_case₂ :
  v ∈ pPrev.vertices →
    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
h_in_prefix : v ∈ pPrev.vertices
h_eq_end : 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

Tactic:
exact h_case₁ h_eq_end
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
h_case₂ :
  v ∈ pPrev.vertices →
    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
h_in_prefix : v ∈ pPrev.vertices
h_eq_end : ¬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

Tactic:
h_case₂ h_in_prefix h_eq_end

Premises used: Quiver.Path.end
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
h_case₂ :
  v ∈ pPrev.vertices →
    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
h_in_prefix : v ∈ pPrev.vertices
h_eq_end : ¬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

Tactic:
exact h_case₂ h_in_prefix h_eq_end
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
h_case₂ :
  v ∈ pPrev.vertices →
    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
h_eq_end : 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

Tactic:
h_case₁ h_eq_end

Premises used: Quiver.Path.end
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
h_case₂ :
  v ∈ pPrev.vertices →
    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
h_eq_end : 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

Tactic:
exact h_case₁ h_eq_end