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
p : Path.{u_2, u_1} a b
nil : head? (vertices.{u_1, u_2} (a := a) Path.nil) = some a
cons :
  ∀ {b c : V} (p' : Path.{u_2, u_1} a b) (e : b ⟶ c) (ih : p'.vertices.head? = some a),
    (p'.cons e).vertices.head? = some a
⊢ p.vertices.head? = some a

Tactic:
induction p with
  | nil => simp only [vertices_nil, head?_cons]
  | cons p' e ih => simp [ih]

Premises used: Quiver.Path.nil, Quiver.Path.cons, List.head?_cons, 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
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:
simp only [vertices_nil, head_cons]

Premises used: List.head_cons, Quiver.Path.vertices_nil
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b b_1 c : V
p' : Path.{u_2, u_1} a b_1
a_1 : b_1 ⟶ 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:
simp [head_append_of_ne_nil (vertices_ne_nil p'), ih]

Premises used: Quiver.Path.vertices_ne_nil, List.head_append_of_ne_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
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
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
⊢ p.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]

Premises used: Quiver.Path.nil, List.head_cons, Quiver.Path.cons, 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
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (vertices.{u_1, u_2} (a := a) nil) 0 ⋯ = a

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b b_1 c : V
p' : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p'.vertices 0 ⋯ = a
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (p'.cons e).vertices 0 ⋯ = a

Tactic:
simp [ih]
-- 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
nil : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (vertices.{u_1, u_2} (a := a) Path.nil) 0 ⋯ = a
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 ⋯ = a),
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (p'.cons e).vertices 0 ⋯ = a
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.vertices 0 ⋯ = a

Tactic:
induction p with
  | nil => simp
  | cons p' e ih => simp [ih]

Premises used: Quiver.Path.nil, Quiver.Path.cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
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:
simp only [vertices_nil, getLast_singleton]

Premises used: List.getLast_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 b_1 c : V
p' : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih : ∀ (h : p'.vertices ≠ []), p'.vertices.getLast h = b_1
h : (p'.cons e).vertices ≠ []
⊢ (p'.cons e).vertices.getLast h = c

Tactic:
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
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
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
⊢ p.vertices.getLast h = b

Tactic:
induction p with
  | nil => simp only [vertices_nil, getLast_singleton]
  | cons p' e ih => simp

Premises used: Quiver.Path.nil, Quiver.Path.cons, List.getLast_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
simp_rw : p.vertices.dropLast ++ [p.vertices.getLast ⋯] = p.vertices
⊢ p.vertices.dropLast ++ [b] = p.vertices

Tactic:
simp_rw [← p.vertices_getLast p.vertices_ne_nil, dropLast_concat_getLast]

Premises used: List.dropLast_concat_getLast, Quiver.Path.vertices_ne_nil, Quiver.Path.vertices_getLast
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b c : V
p : Path.{u_2, u_1} a b
⊢ (p.comp nil).vertices = p.vertices.dropLast ++ vertices.{u_1, u_2} (a := b) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b c : V
p : Path.{u_2, u_1} a b
b_1 c_1 : V
q' : Path.{u_2, u_1} b b_1
e : b_1 ⟶ c_1
ih : (p.comp q').vertices = p.vertices.dropLast ++ q'.vertices
⊢ (p.comp (q'.cons e)).vertices = p.vertices.dropLast ++ (q'.cons e).vertices

Tactic:
simp [ih]
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
⊢ (p.comp q).vertices = p.vertices.dropLast ++ q.vertices

Tactic:
induction q with
  | nil => simp
  | cons q' e ih => simp [ih]

Premises used: Quiver.Path.nil, Quiver.Path.cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
⊢ p.length = 0 ↔ p = Path.nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
nil₂ nil₃ 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
nil₅ nil₆ 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
nil₈ nil₉ 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
nil₁₁ nil₁₂ 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
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
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
⊢ length.{u_1, u_2} (V := V) (a := a) Path.nil = 0 ↔ Eq (α := Path.{u_2, u_1} a a) Path.nil Path.nil

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
cons₁ : a_1.cons a_2 = nil → (a_1.cons a_2).length = 0
cons₂ : (a_1.cons a_2).length = 0 → a_1.cons a_2 = nil
cons₃ : a_1.cons a_2 = nil → (a_1.cons a_2).length = 0
⊢ (a_1.cons a_2).length = 0 ↔ a_1.cons a_2 = nil

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b c : V
p₁ : Path.{u_2, u_1} a c
p₂ : Path.{u_2, u_1} c b
h : p₁.length < (p₁.comp p₂).vertices.length
⊢ (p₁.comp p₂).vertices.get (⟨p₁.length, h⟩ : Fin (p₁.comp p₂).vertices.length) = c

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
i j : V
e : i ⟶ j
⊢ (cons nil e).vertices = [i, j]

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
i j : V
e : i ⟶ j
⊢ e.toPath.vertices.tail = [j]

Tactic:
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
q : Path.{u_2, u_1} b a
h : p.comp q = nil
⊢ (p.comp q).length = 0

Tactic:
simpa using congrArg Path.length h

Premises used: congrArg, Quiver.Path.length
-- 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
q : Path.{u_2, u_1} b a
h : p.comp q = nil
⊢ (p.comp q).length = 0

Tactic:
have hlen : (p.comp q).length = 0 := by
    simpa using congrArg Path.length h
-- 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
q : Path.{u_2, u_1} b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
⊢ p.length + q.length = 0

Tactic:
simpa [length_comp] using hlen

Premises used: Quiver.Path.length_comp
-- 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
q : Path.{u_2, u_1} b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
⊢ p.length + q.length = 0

Tactic:
have : p.length + q.length = 0 := by
    simpa [length_comp] using hlen
-- 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
q : Path.{u_2, u_1} b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
this : p.length + q.length = 0
⊢ p.length = 0

Tactic:
Nat.eq_zero_of_add_eq_zero_right this

Premises used: Nat.eq_zero_of_add_eq_zero_right
-- 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
q : Path.{u_2, u_1} b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
this : p.length + q.length = 0
⊢ p.length = 0

Tactic:
exact Nat.eq_zero_of_add_eq_zero_right this

Premises used: Nat.eq_zero_of_add_eq_zero_right
-- 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
q : Path.{u_2, u_1} b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
this : p.length + q.length = 0
⊢ q.length = 0

Tactic:
Nat.eq_zero_of_add_eq_zero_left this

Premises used: Nat.eq_zero_of_add_eq_zero_left
-- 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
q : Path.{u_2, u_1} b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
this : p.length + q.length = 0
⊢ q.length = 0

Tactic:
exact Nat.eq_zero_of_add_eq_zero_left this

Premises used: Nat.eq_zero_of_add_eq_zero_left
-- 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
q : Path.{u_2, u_1} b a
⊢ p.comp q = nil ↔ p.length = 0 ∧ q.length = 0

Tactic:
⟨fun h ↦ ⟨nil_of_comp_eq_nil_left h, nil_of_comp_eq_nil_right h⟩, fun ⟨hp, hq⟩ ↦ ?_⟩

Premises used: Quiver.Path.nil, _private.0.Quiver.Path.comp_eq_nil_iff.match_1, Quiver.Path.nil_of_comp_eq_nil_right, Quiver.Path.nil_of_comp_eq_nil_left, And.intro, Iff.intro, Quiver.Path.comp, Eq
-- 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
q : Path.{u_2, u_1} b a
refine : p.length = 0 ∧ q.length = 0 → ∀ (hp : p.length = 0) (hq : q.length = 0), p.comp q = nil
⊢ p.comp q = nil ↔ p.length = 0 ∧ q.length = 0

Tactic:
refine ⟨fun h ↦ ⟨nil_of_comp_eq_nil_left h, nil_of_comp_eq_nil_right h⟩, fun ⟨hp, hq⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
q : Path.{u_2, u_1} a a
h : 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:
simpa using (length_eq_zero_iff q).mp hq

Premises used: Quiver.Path.length_eq_zero_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b b_1 c : V
p' : Path.{u_2, u_1} a b_1
a_1 : b_1 ⟶ c
ihp :
  ∀ {q : Path.{u_2, u_1} b_1 a},
    p'.length = 0 ∧ q.length = 0 → ∀ (hp : p'.length = 0) (hq : q.length = 0), p'.comp q = nil
q : Path.{u_2, u_1} c a
h : (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 = nil

Tactic:
simp at 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
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
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
⊢ p.comp q = Path.nil

Tactic:
induction p with
  | nil => simpa using (length_eq_zero_iff q).mp hq
  | cons p' _ ihp => simp at hp

Premises used: Quiver.Path.nil, Quiver.Path.cons, Quiver.Path.length_eq_zero_iff, Iff.mp
-- 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
⊢ p.vertices.getLast ⋯ = b

Tactic:
have h₁ : p.vertices.getLast (vertices_ne_nil p) = b :=
    vertices_getLast p (vertices_ne_nil p)
-- 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
h₁ : p.vertices.getLast ⋯ = b
⊢ p.vertices.getLast ⋯ ∈ p.vertices

Tactic:
have h₂ := getLast_mem (l := p.vertices) (vertices_ne_nil p)
-- 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
h₁ : p.vertices.getLast ⋯ = b
h₂ : p.vertices.getLast ⋯ ∈ p.vertices
⊢ b ∈ p.vertices

Tactic:
simpa [h₁] using h₂
-- 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 ≤ length.{u_1, u_2} (V := V) (a := a) nil
⊢ n = 0

Tactic:
simpa using hn
-- 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 ≤ length.{u_1, u_2} (V := V) (a := a) Path.nil
nil :
  ∀ (hn : 0 ≤ 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 = 0
⊢ ∃ (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

Tactic:
obtain ⟨rfl⟩ : n = 0 := by simpa using hn

Premises used: 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
hn : 0 ≤ length.{u_1, u_2} (V := V) (a := a) nil
⊢ Eq (α := Path.{u_2, u_1} a a) nil (comp nil nil)

Tactic:
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
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:
exact ⟨a, Path.nil, Path.nil, by simp, 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
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
⊢ n ≤ p'.length + 1

Tactic:
rw [length_cons] at hn

Premises used: Quiver.Path.length_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
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
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
⊢ ∃ (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

Premises used: Nat.le_succ_iff, 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
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
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
⊢ ∃ (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
-- 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
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
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
⊢ p'.cons e = p₁.comp (p₂.cons e)

Tactic:
simp [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
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
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:
exact ⟨d, p₁, p₂.cons e, by simp [hp], hl⟩
-- 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
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
hn : p'.length.succ ≤ p'.length + 1
⊢ p'.cons e = (p'.cons e).comp nil

Tactic:
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
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
hn : p'.length.succ ≤ p'.length + 1
⊢ (p'.cons e).length = p'.length.succ

Tactic:
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
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
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:
exact ⟨c, p'.cons e, Path.nil, by simp, 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
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
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
⊢ ∃ (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

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⟩

Premises used: Quiver.Path.length_cons, Quiver.Path.nil, Nat.le_succ_iff, Quiver.Path.cons, 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
n : ℕ
hn : n < p.vertices.length
⊢ n < p.length + 1

Tactic:
rw [vertices_length] at hn

Premises used: Quiver.Path.vertices_length
-- 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.length + 1
⊢ n ≤ p.length

Tactic:
Nat.le_of_lt_succ hn

Premises used: Nat.le_of_lt_succ
-- 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.length + 1
⊢ n ≤ p.length

Tactic:
exact Nat.le_of_lt_succ hn

Premises used: Nat.le_of_lt_succ
-- 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
⊢ n ≤ p.length

Tactic:
have hn_le_len : n ≤ p.length := by
    rw [vertices_length] at hn
    exact Nat.le_of_lt_succ hn
-- 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
hn_le_len : n ≤ p.length
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
⊢ ∃ (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

Tactic:
obtain ⟨v, p₁, p₂, rfl, rfl⟩ := p.exists_eq_comp_of_le_length hn_le_len

Premises used: Quiver.Path.exists_eq_comp_of_le_length, rfl