awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ : Path.{u_1, u} a b
b_1 c_1 : V
q₁ : Path.{u_1, u} b b_1
f₁ f₂ : b_1 ⟶ c_1
ih : ∀ {q₂ : Path.{u_1, u} b b_1} (hq : q₁.length = q₂.length) (h : p₁.comp q₁ = p₁.comp q₂), p₁ = p₁ ∧ q₁ = q₂
hq : (q₁.cons f₁).length = (q₁.cons f₂).length
h : b_1 = b_1 ∧ p₁.comp q₁ ≍ p₁.comp q₁ ∧ f₁ ≍ f₂
cons : p₁ = p₁ ∧ q₁.cons f₂ = q₁.cons f₂
⊢ p₁ = p₁ ∧ q₁.cons f₁ = q₁.cons f₂

Tactic:
rw [h.2.2.eq]

Premises used: And.right, HEq.eq
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ : Path.{u_1, u} a b
b_1 c_1 : V
q₁ : Path.{u_1, u} b b_1
f₁ f₂ : b_1 ⟶ c_1
ih : ∀ {q₂ : Path.{u_1, u} b b_1} (hq : q₁.length = q₂.length) (h : p₁.comp q₁ = p₁.comp q₂), p₁ = p₁ ∧ q₁ = q₂
hq : (q₁.cons f₁).length = (q₁.cons f₂).length
h : b_1 = b_1 ∧ p₁.comp q₁ ≍ p₁.comp q₁ ∧ f₁ ≍ f₂
⊢ p₁ = p₁ ∧ q₁.cons f₂ = q₁.cons f₂

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ : Path.{u_1, u} a b
b_1 c_1 : V
q₁ : Path.{u_1, u} b b_1
f₁ f₂ : b_1 ⟶ c_1
ih : ∀ {q₂ : Path.{u_1, u} b b_1} (hq : q₁.length = q₂.length) (h : p₁.comp q₁ = p₁.comp q₂), p₁ = p₁ ∧ q₁ = q₂
hq : (q₁.cons f₁).length = (q₁.cons f₂).length
h : b_1 = b_1 ∧ p₁.comp q₁ ≍ p₁.comp q₁ ∧ f₁ ≍ f₂
⊢ p₁ = p₁ ∧ q₁.cons f₂ = q₁.cons f₂

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ p₂ : Path.{u_1, u} a b
q₁ q₂ : Path.{u_1, u} b c
hq : q₁.length = q₂.length
h : p₁.comp q₁ = p₂.comp q₂
nil :
  ∀ {q₂ : Path.{u_1, u} b b} (hq : length.{u, u_1} (V := V) (a := b) Path.nil = q₂.length)
    (h : p₁.comp Path.nil = p₂.comp q₂), p₁ = p₂ ∧ Path.nil = q₂
cons :
  ∀ {b_1 c : V} (q₁ : Path.{u_1, u} b b_1) (f₁ : b_1 ⟶ c)
    (ih : ∀ {q₂ : Path.{u_1, u} b b_1} (hq : q₁.length = q₂.length) (h : p₁.comp q₁ = p₂.comp q₂), p₁ = p₂ ∧ q₁ = q₂)
    {q₂ : Path.{u_1, u} b c} (hq : (q₁.cons f₁).length = q₂.length) (h : p₁.comp (q₁.cons f₁) = p₂.comp q₂),
    p₁ = p₂ ∧ q₁.cons f₁ = q₂
⊢ p₁ = p₂ ∧ q₁ = q₂

Tactic:
induction q₁ with
  | nil =>
    rcases q₂ with _ | ⟨q₂, f₂⟩
    · exact ⟨h, rfl⟩
    · cases hq
  | cons q₁ f₁ ih =>
    rcases q₂ with _ | ⟨q₂, f₂⟩
    · cases hq
    · simp only [comp_cons, cons.injEq] at h
      obtain rfl := h.1
      obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq
      rw [h.2.2.eq]
      exact ⟨rfl, rfl⟩

Premises used: Quiver.Path.nil, Quiver.Path.cons, Quiver.Path.cons.injEq, Quiver.Path.comp_cons, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ p₂ : Path.{u_1, u} a b
q₁ q₂ : Path.{u_1, u} b c
h : p₁.length = p₂.length
h_eq : p₁.comp q₁ = p₂.comp q₂
⊢ p₂.length + q₁.length = p₂.length + q₂.length

Tactic:
simpa [h] using congr_arg length h_eq

Premises used: congr_arg, Quiver.Path.length
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ : Path.{u_1, u} a b
q₁ : Path.{u_1, u} b c
h : p₁.length = p₁.length
⊢ p₁.comp q₁ = p₁.comp q₁

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
q : Path.{u_1, u} b c
⊢ Injective (β := Path.{u_1, u} a c) fun (p : Path.{u_1, u} a b) ↦ p.comp q

Tactic:
fun _ _ h => ((comp_inj rfl).1 h).1

Premises used: Quiver.Path.comp_inj, And.left, Iff.mp, Function.Injective, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p : Path.{u_1, u} a b
⊢ Injective (α := Path.{u_1, u} b c) p.comp

Tactic:
fun _ _ h => ((comp_inj' rfl).1 h).2

Premises used: Quiver.Path.comp_inj', And.right, Iff.mp, Function.Injective, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ p₂ : Path.{u_1, u} a b
q : Path.{u_1, u} b c
⊢ p₁.comp q = p₂.comp q ↔ p₁ = p₂

Tactic:
q.comp_injective_left.eq_iff

Premises used: Function.Injective.eq_iff, Quiver.Path.comp_injective_left
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p : Path.{u_1, u} a b
q₁ q₂ : Path.{u_1, u} b c
⊢ p.comp q₁ = p.comp q₂ ↔ q₁ = q₂

Tactic:
p.comp_injective_right.eq_iff

Premises used: Function.Injective.eq_iff, Quiver.Path.comp_injective_right
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b : V
n : ℕ
hp : length.{u, u_1} (V := V) (a := a) nil = n + 1
⊢ ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Path.{u_1, u} c a), ∃ (x : q.length = n), nil = f.toPath.comp q

Tactic:
simp at hp
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c d : V
p : Path.{u_1, u} a c
q : c ⟶ d
h :
  ∀ {n : ℕ} (hp : p.length = n + 1),
    ∃ (c_1 : V), ∃ (f : a ⟶ c_1), ∃ (q : Path.{u_1, u} c_1 c), ∃ (x : q.length = n), p = f.toPath.comp q
n : ℕ
hp : (p.cons q).length = n + 1
cons :
  ∀ (hp : (p.cons q).length = HAdd.hAdd (α := ℕ) 0 1),
    ∃ (c_1 : V), ∃ (f : a ⟶ c_1), ∃ (q_1 : Path.{u_1, u} c_1 d), ∃ (x : q_1.length = 0), p.cons q = f.toPath.comp q_1
cons₁ :
  ∀ (n : ℕ) (hp : (p.cons q).length = n + 1 + 1),
    ∃ (c_1 : V),
      ∃ (f : a ⟶ c_1), ∃ (q_1 : Path.{u_1, u} c_1 d), ∃ (x : q_1.length = n + 1), p.cons q = f.toPath.comp q_1
⊢ ∃ (c_1 : V), ∃ (f : a ⟶ c_1), ∃ (q_1 : Path.{u_1, u} c_1 d), ∃ (x : q_1.length = n), p.cons q = f.toPath.comp q_1

Tactic:
cases n
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c d : V
p : Path.{u_1, u} a c
q : c ⟶ d
h :
  ∀ {n : ℕ} (hp : p.length = n + 1),
    ∃ (c_1 : V), ∃ (f : a ⟶ c_1), ∃ (q : Path.{u_1, u} c_1 c), ∃ (x : q.length = n), p = f.toPath.comp q
hp : (p.cons q).length = HAdd.hAdd (α := ℕ) 0 1
⊢ p.length = 0

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

Premises used: Quiver.Path.length_cons, Nat.add_eq_right, Nat.zero_add
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c d : V
p : Path.{u_1, u} a c
q : c ⟶ d
h :
  ∀ {n : ℕ} (hp : p.length = n + 1),
    ∃ (c_1 : V), ∃ (f : a ⟶ c_1), ∃ (q : Path.{u_1, u} c_1 c), ∃ (x : q.length = n), p = f.toPath.comp q
hp : p.length = 0
cons :
  ∀ (p : Path.{u_1, u} a a) (q : a ⟶ d)
    (h :
      ∀ {n : ℕ} (hp : p.length = n + 1),
        ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Path.{u_1, u} c a), ∃ (x : q.length = n), p = f.toPath.comp q)
    (hp : p.length = 0),
    ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q_1 : Path.{u_1, u} c d), ∃ (x : q_1.length = 0), p.cons q = f.toPath.comp q_1
⊢ ∃ (c_1 : V), ∃ (f : a ⟶ c_1), ∃ (q_1 : Path.{u_1, u} c_1 d), ∃ (x : q_1.length = 0), p.cons q = f.toPath.comp q_1

Tactic:
obtain rfl := eq_of_length_zero p hp

Premises used: Quiver.Path.eq_of_length_zero, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b d : V
p : Path.{u_1, u} a a
q : a ⟶ d
h :
  ∀ {n : ℕ} (hp : p.length = n + 1),
    ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Path.{u_1, u} c a), ∃ (x : q.length = n), p = f.toPath.comp q
hp : p.length = 0
cons :
  ∀
    (h :
      ∀ {n : ℕ} (hp : length.{u, u_1} (V := V) (a := a) nil = n + 1),
        ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Path.{u_1, u} c a), ∃ (x : q.length = n), nil = f.toPath.comp q)
    (hp : length.{u, u_1} (V := V) (a := a) nil = 0),
    ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q_1 : Path.{u_1, u} c d), ∃ (x : q_1.length = 0), Path.cons nil q = f.toPath.comp q_1
⊢ ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q_1 : Path.{u_1, u} c d), ∃ (x : q_1.length = 0), p.cons q = f.toPath.comp q_1

Tactic:
obtain rfl := eq_nil_of_length_zero p hp

Premises used: Quiver.Path.eq_nil_of_length_zero, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b d : V
q : a ⟶ d
h :
  ∀ {n : ℕ} (hp : length.{u, u_1} (V := V) (a := a) nil = n + 1),
    ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Path.{u_1, u} c a), ∃ (x : q.length = n), nil = f.toPath.comp q
hp : length.{u, u_1} (V := V) (a := a) nil = 0
⊢ ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q_1 : Path.{u_1, u} c d), ∃ (x : q_1.length = 0), cons nil q = f.toPath.comp q_1

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

Premises used: Quiver.Path.nil, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b d : V
q : a ⟶ d
h :
  ∀ {n : ℕ} (hp : length.{u, u_1} (V := V) (a := a) nil = n + 1),
    ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Path.{u_1, u} c a), ∃ (x : q.length = n), nil = f.toPath.comp q
hp : length.{u, u_1} (V := V) (a := a) nil = 0
⊢ ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q_1 : Path.{u_1, u} c d), ∃ (x : q_1.length = 0), cons nil q = f.toPath.comp q_1

Tactic:
exact ⟨d, q, nil, rfl, rfl⟩
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c d : V
p : Path.{u_1, u} a c
q : c ⟶ d
h :
  ∀ {n : ℕ} (hp : p.length = n + 1),
    ∃ (c_1 : V), ∃ (f : a ⟶ c_1), ∃ (q : Path.{u_1, u} c_1 c), ∃ (x : q.length = n), p = f.toPath.comp q
n : ℕ
hp : (p.cons q).length = n + 1 + 1
⊢ p.length = n + 1

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

Premises used: Nat.add_right_cancel_iff, Quiver.Path.length_cons
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c d : V
p : Path.{u_1, u} a c
q : c ⟶ d
h :
  ∀ {n : ℕ} (hp : p.length = n + 1),
    ∃ (c_1 : V), ∃ (f : a ⟶ c_1), ∃ (q : Path.{u_1, u} c_1 c), ∃ (x : q.length = n), p = f.toPath.comp q
n : ℕ
hp : p.length = n + 1
cons :
  ∀ (x : V) (q'' : a ⟶ x) (p'' : Path.{u_1, u} x c) (hl : p''.length = n)
    (h :
      ∀ {n : ℕ} (hp : (q''.toPath.comp p'').length = n + 1),
        ∃ (c_1 : V),
          ∃ (f : a ⟶ c_1), ∃ (q : Path.{u_1, u} c_1 c), ∃ (x_1 : q.length = n), q''.toPath.comp p'' = f.toPath.comp q)
    (hp : (q''.toPath.comp p'').length = n + 1),
    ∃ (c_1 : V),
      ∃ (f : a ⟶ c_1),
        ∃ (q_1 : Path.{u_1, u} c_1 d), ∃ (x_1 : q_1.length = n + 1), (q''.toPath.comp p'').cons q = f.toPath.comp q_1
⊢ ∃ (c_1 : V), ∃ (f : a ⟶ c_1), ∃ (q_1 : Path.{u_1, u} c_1 d), ∃ (x : q_1.length = n + 1), p.cons q = f.toPath.comp q_1

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

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c d : V
q : c ⟶ d
n : ℕ
x : V
q'' : a ⟶ x
p'' : Path.{u_1, u} x c
hl : p''.length = n
h :
  ∀ {n : ℕ} (hp : (q''.toPath.comp p'').length = n + 1),
    ∃ (c_1 : V),
      ∃ (f : a ⟶ c_1), ∃ (q : Path.{u_1, u} c_1 c), ∃ (x_1 : q.length = n), q''.toPath.comp p'' = f.toPath.comp q
hp : (q''.toPath.comp p'').length = n + 1
⊢ (p''.cons q).length = n + 1

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c d : V
q : c ⟶ d
n : ℕ
x : V
q'' : a ⟶ x
p'' : Path.{u_1, u} x c
hl : p''.length = n
h :
  ∀ {n : ℕ} (hp : (q''.toPath.comp p'').length = n + 1),
    ∃ (c_1 : V),
      ∃ (f : a ⟶ c_1), ∃ (q : Path.{u_1, u} c_1 c), ∃ (x_1 : q.length = n), q''.toPath.comp p'' = f.toPath.comp q
hp : (q''.toPath.comp p'').length = n + 1
⊢ ∃ (c_1 : V),
    ∃ (f : a ⟶ c_1),
      ∃ (q_1 : Path.{u_1, u} c_1 d), ∃ (x_1 : q_1.length = n + 1), (q''.toPath.comp p'').cons q = f.toPath.comp q_1

Tactic:
exact ⟨x, q'', p''.cons q, by simpa, rfl⟩
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b : V
p : Path.{u_1, u} a b
n : ℕ
hp : p.length = n + 1
nil :
  ∀ {n : ℕ} (hp : length.{u, u_1} (V := V) (a := a) Path.nil = n + 1),
    ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Path.{u_1, u} c a), ∃ (x : q.length = n), Path.nil = f.toPath.comp q
cons :
  ∀ {c d : V} (p : Path.{u_1, u} a c) (q : c ⟶ d)
    (h :
      ∀ {n : ℕ} (hp : p.length = n + 1),
        ∃ (c_1 : V), ∃ (f : a ⟶ c_1), ∃ (q : Path.{u_1, u} c_1 c), ∃ (x : q.length = n), p = f.toPath.comp q)
    {n : ℕ} (hp : (p.cons q).length = n + 1),
    ∃ (c_1 : V), ∃ (f : a ⟶ c_1), ∃ (q_1 : Path.{u_1, u} c_1 d), ∃ (x : q_1.length = n), p.cons q = f.toPath.comp q_1
⊢ ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Path.{u_1, u} c b), ∃ (x : q.length = n), p = f.toPath.comp q

Tactic:
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⟩

Premises used: Nat.add_right_cancel_iff, Quiver.Path.length_cons, Nat.add_eq_right, Quiver.Path.nil, Quiver.Path.cons, Nat.zero_add, Quiver.Path.eq_nil_of_length_zero, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b : V
p : Path.{u_3, u_1} a b
⊢ p.length ≠ 0 ↔ ∃ (c : V), ∃ (e : a ⟶ c), ∃ (p' : Path.{u_3, u_1} c b), p = e.toPath.comp p' ∧ p.length = p'.length + 1

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b : V
p : Path.{u_3, u_1} a b
refine_1 :
  ∀ (h : p.length ≠ 0),
    ∃ (c : V), ∃ (e : a ⟶ c), ∃ (p' : Path.{u_3, u_1} c b), p = e.toPath.comp p' ∧ p.length = p'.length + 1
refine_2 :
  (∃ (c : V), ∃ (e : a ⟶ c), ∃ (p' : Path.{u_3, u_1} c b), p = e.toPath.comp p' ∧ p.length = p'.length + 1) →
    p.length ≠ 0
⊢ p.length ≠ 0 ↔ ∃ (c : V), ∃ (e : a ⟶ c), ∃ (p' : Path.{u_3, u_1} c b), p = e.toPath.comp p' ∧ p.length = p'.length + 1

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b : V
p : Path.{u_3, u_1} a b
h : p.length ≠ 0
⊢ p.length = p.length - 1 + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b : V
p : Path.{u_3, u_1} a b
h : p.length ≠ 0
⊢ p.length = p.length - 1 + 1

Tactic:
have h_len : p.length = (p.length - 1) + 1 := by lia
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b : V
p : Path.{u_3, u_1} a b
h : p.length ≠ 0
h_len : p.length = p.length - 1 + 1
refine_1 :
  ∀ (c : V) (e : a ⟶ c) (p' : Path.{u_3, u_1} c b) (h : (e.toPath.comp p').length ≠ 0)
    (h_len : (e.toPath.comp p').length = (e.toPath.comp p').length - 1 + 1)
    (hp' : p'.length = (e.toPath.comp p').length - 1),
    ∃ (c_1 : V),
      ∃ (e_1 : a ⟶ c_1),
        ∃ (p'_1 : Path.{u_3, u_1} c_1 b),
          e.toPath.comp p' = e_1.toPath.comp p'_1 ∧ (e.toPath.comp p').length = p'_1.length + 1
⊢ ∃ (c : V), ∃ (e : a ⟶ c), ∃ (p' : Path.{u_3, u_1} c b), p = e.toPath.comp p' ∧ p.length = p'.length + 1

Tactic:
obtain ⟨c, e, p', hp', rfl⟩ := Path.eq_toPath_comp_of_length_eq_succ p h_len

Premises used: Quiver.Path.eq_toPath_comp_of_length_eq_succ, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b c : V
e : a ⟶ c
p' : Path.{u_3, u_1} c b
h : (e.toPath.comp p').length ≠ 0
h_len : (e.toPath.comp p').length = (e.toPath.comp p').length - 1 + 1
hp' : p'.length = (e.toPath.comp p').length - 1
⊢ ∃ (c_1 : V),
    ∃ (e_1 : a ⟶ c_1),
      ∃ (p'_1 : Path.{u_3, u_1} c_1 b),
        e.toPath.comp p' = e_1.toPath.comp p'_1 ∧ (e.toPath.comp p').length = p'_1.length + 1

Tactic:
exact ⟨c, e, p', rfl, by lia⟩
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b c : V
p' : a ⟶ c
e : Path.{u_3, u_1} c b
h : (p'.toPath.comp e).length = e.length + 1
⊢ (p'.toPath.comp e).length ≠ 0

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b : V
p : Path.{u_3, u_1} a b
⊢ p.length ≠ 0 ↔ ∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ b), p = p'.cons e

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b : V
p : Path.{u_3, u_1} a b
refine_1 : ∀ (h : p.length ≠ 0), ∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ b), p = p'.cons e
refine_2 : (∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ b), p = p'.cons e) → p.length ≠ 0
⊢ p.length ≠ 0 ↔ ∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ b), p = p'.cons e

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a : V
h : length.{u_1, u_3} (V := V) (a := a) nil ≠ 0
⊢ ∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ a), nil = p'.cons e

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b b_1 : V
p' : Path.{u_3, u_1} a b_1
e : b_1 ⟶ b
h : (p'.cons e).length ≠ 0
⊢ ∃ (c : V), ∃ (p'_1 : Path.{u_3, u_1} a c), ∃ (e_1 : c ⟶ b), p'.cons e = p'_1.cons e_1

Tactic:
⟨_, p', e, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b b_1 : V
p' : Path.{u_3, u_1} a b_1
e : b_1 ⟶ b
h : (p'.cons e).length ≠ 0
⊢ ∃ (c : V), ∃ (p'_1 : Path.{u_3, u_1} a c), ∃ (e_1 : c ⟶ b), p'.cons e = p'_1.cons e_1

Tactic:
exact ⟨_, p', e, rfl⟩
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b : V
p : Path.{u_3, u_1} a b
h : p.length ≠ 0
refine_1 :
  ∀ (h : length.{u_1, u_3} (V := V) (a := a) nil ≠ 0),
    ∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ a), nil = p'.cons e
refine_1₁ :
  ∀ {b_1 : V} (p' : Path.{u_3, u_1} a b_1) (e : b_1 ⟶ b) (h : (p'.cons e).length ≠ 0),
    ∃ (c : V), ∃ (p'_1 : Path.{u_3, u_1} a c), ∃ (e_1 : c ⟶ b), p'.cons e = p'_1.cons e_1
⊢ ∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ b), p = p'.cons e

Tactic:
cases p with
    | nil => simp at h
    | cons p' e => exact ⟨_, p', e, rfl⟩

Premises used: Quiver.Path.nil, Quiver.Path.cons
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b c : V
p' : Path.{u_3, u_1} a c
e : c ⟶ b
⊢ (p'.cons e).length ≠ 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
a b c : V
p : Path.{u_3, u_1} a b
e : b ⟶ c
⊢ p.comp e.toPath = p.cons e

Tactic:
rfl

Premises used: Quiver.Hom.toPath, Quiver.Path.comp, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b : V
p : Path.{u_1, u} a b
⊢ (p.comp nil).toList = toList.{u, u_1} (a := b) nil ++ p.toList

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b : V
p : Path.{u_1, u} a b
x d : V
q : Path.{u_1, u} b d
a_1 : d ⟶ x
⊢ (p.comp (q.cons a_1)).toList = (q.cons a_1).toList ++ p.toList

Tactic:
simp [toList_comp]
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
inst_1 : ∀ (a b : V), Subsingleton.{u_1 + 1} (a ⟶ b)
a c : V
p : Path.{u_1, u} a c
f : c ⟶ a
h : toList.{u, u_1} (a := a) nil = (p.cons f).toList
⊢ nil = p.cons f

Tactic:
cases h
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
inst_1 : ∀ (a b : V), Subsingleton.{u_1 + 1} (a ⟶ b)
a c : V
p : Path.{u_1, u} a c
f : c ⟶ a
h : (p.cons f).toList = toList.{u, u_1} (a := a) nil
⊢ p.cons f = nil

Tactic:
cases h
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
inst_1 : ∀ (a b : V), Subsingleton.{u_1 + 1} (a ⟶ b)
a x c : V
p : Path.{u_1, u} a c
f : c ⟶ x
t : V
C : Path.{u_1, u} a t
D : t ⟶ x
h : (p.cons f).toList = (C.cons D).toList
⊢ c = t ∧ p.toList = C.toList

Tactic:
simp only [toList, List.cons.injEq] at h

Premises used: Quiver.Path.toList, List.cons.injEq
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
inst_1 : ∀ (a b : V), Subsingleton.{u_1 + 1} (a ⟶ b)
a x c : V
p : Path.{u_1, u} a c
f : c ⟶ x
t : V
C : Path.{u_1, u} a t
D : t ⟶ x
h : c = t ∧ p.toList = C.toList
obtain : ∀ (C : Path.{u_1, u} a c) (D : c ⟶ x) (hAC : p.toList = C.toList), p.cons f = C.cons D
⊢ p.cons f = C.cons D

Tactic:
obtain ⟨rfl, hAC⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
inst_1 : ∀ (a b : V), Subsingleton.{u_1 + 1} (a ⟶ b)
a x c : V
p : Path.{u_1, u} a c
f : c ⟶ x
C : Path.{u_1, u} a c
D : c ⟶ x
hAC : p.toList = C.toList
⊢ p.cons f = C.cons D

Tactic:
simp [toList_injective _ _ hAC, eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b : V
inst_1 : ∀ (a b : V), Subsingleton.{u_1 + 1} (a ⟶ b)
p q : Path.{u_1, u} a b
⊢ p.toList = q.toList ↔ p = q

Tactic:
(toList_injective _ _).eq_iff

Premises used: Function.Injective.eq_iff, Quiver.Path.toList_injective
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V_1 : Type u
inst : Quiver V_1
a b c d : V_1
inst_1 : ∀ (a b : V_1), Subsingleton (a ⟶ b)
V : Type u_1
inst_2 : Quiver.{u_2, u_1} V
v w : V
p q : Path.{u_2, u_1} v w
a_1 x b_1 : V
a_2 : Path.{u_2, u_1} a_1 b_1
a_3 : b_1 ⟶ x
x_1 : Path.{u_2, u_1} a_1 x
x_2 x_3 : BoundedPaths.{u_1, u_2} a_1 x 0
hp : (a_2.cons a_3).length ≤ 0
hq : x_1.length ≤ 0
⊢ Eq (α := BoundedPaths.{u_1, u_2} a_1 x 0)
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ 0) (a_2.cons a_3) hp)
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ 0) x_1 hq)

Tactic:
simp [Quiver.Path.length] at hp

Premises used: Quiver.Path.length
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V_1 : Type u
inst : Quiver V_1
a b c d : V_1
inst_1 : ∀ (a b : V_1), Subsingleton (a ⟶ b)
V : Type u_1
inst_2 : Quiver.{u_2, u_1} V
v w : V
p q : Path.{u_2, u_1} v w
a_1 x : V
x_1 : Path.{u_2, u_1} a_1 x
b_1 : V
a_2 : Path.{u_2, u_1} a_1 b_1
a_3 : b_1 ⟶ x
x_2 x_3 : BoundedPaths.{u_1, u_2} a_1 x 0
hp : x_1.length ≤ 0
hq : (a_2.cons a_3).length ≤ 0
⊢ Eq (α := BoundedPaths.{u_1, u_2} a_1 x 0) (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ 0) x_1 hp)
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ 0) (a_2.cons a_3) hq)

Tactic:
simp [Quiver.Path.length] at hq

Premises used: Quiver.Path.length
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V_1 : Type u
inst : Quiver V_1
a b c d : V_1
inst_1 : ∀ (a b : V_1), Subsingleton (a ⟶ b)
V : Type u_1
inst_2 : Quiver.{u_2, u_1} V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths.{u_1, u_2} v w n)
v w : V
p q : Path.{u_2, u_1} v w
a_1 x v' v'' : V
x_1 x_2 : BoundedPaths.{u_1, u_2} a_1 x (n + 1)
a_2 : V
p' : Path.{u_2, u_1} a_1 a_2
α : a_2 ⟶ x
q' : Path.{u_2, u_1} a_1 a_2
β : a_2 ⟶ x
hp : (p'.cons α).length ≤ n + 1
hq : (q'.cons β).length ≤ n + 1
h : α = β
⊢ p'.length ≤ n

Tactic:
simp [Quiver.Path.length] at hp

Premises used: Quiver.Path.length
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V_1 : Type u
inst : Quiver V_1
a b c d : V_1
inst_1 : ∀ (a b : V_1), Subsingleton (a ⟶ b)
V : Type u_1
inst_2 : Quiver.{u_2, u_1} V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths.{u_1, u_2} v w n)
v w : V
p q : Path.{u_2, u_1} v w
a_1 x v' v'' : V
x_1 x_2 : BoundedPaths.{u_1, u_2} a_1 x (n + 1)
a_2 : V
p' : Path.{u_2, u_1} a_1 a_2
α : a_2 ⟶ x
q' : Path.{u_2, u_1} a_1 a_2
β : a_2 ⟶ x
hq : (q'.cons β).length ≤ n + 1
h : α = β
hp : p'.length ≤ n
⊢ p'.length ≤ n

Tactic:
lia
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V_1 : Type u
inst : Quiver V_1
a b c d : V_1
inst_1 : ∀ (a b : V_1), Subsingleton (a ⟶ b)
V : Type u_1
inst_2 : Quiver.{u_2, u_1} V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths.{u_1, u_2} v w n)
v w : V
p q : Path.{u_2, u_1} v w
a_1 x v' v'' : V
x_1 x_2 : BoundedPaths.{u_1, u_2} a_1 x (n + 1)
a_2 : V
p' : Path.{u_2, u_1} a_1 a_2
α : a_2 ⟶ x
q' : Path.{u_2, u_1} a_1 a_2
β : a_2 ⟶ x
hp : (p'.cons α).length ≤ n + 1
hq : (q'.cons β).length ≤ n + 1
h : α = β
hp' : p'.length ≤ n
⊢ q'.length ≤ n

Tactic:
simp [Quiver.Path.length] at hq

Premises used: Quiver.Path.length
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V_1 : Type u
inst : Quiver V_1
a b c d : V_1
inst_1 : ∀ (a b : V_1), Subsingleton (a ⟶ b)
V : Type u_1
inst_2 : Quiver.{u_2, u_1} V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths.{u_1, u_2} v w n)
v w : V
p q : Path.{u_2, u_1} v w
a_1 x v' v'' : V
x_1 x_2 : BoundedPaths.{u_1, u_2} a_1 x (n + 1)
a_2 : V
p' : Path.{u_2, u_1} a_1 a_2
α : a_2 ⟶ x
q' : Path.{u_2, u_1} a_1 a_2
β : a_2 ⟶ x
hp : (p'.cons α).length ≤ n + 1
h : α = β
hp' : p'.length ≤ n
hq : q'.length ≤ n
⊢ q'.length ≤ n

Tactic:
lia