awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ p₂ : Path.{u_1, u} a b
b_1 c_1 : V
q₁ : Path.{u_1, u} b b_1
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₂
q₂ : Path.{u_1, u} b c_1
hq : (q₁.cons f₁).length = q₂.length
h : p₁.comp (q₁.cons f₁) = p₂.comp q₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂
have cons : ∀ (f₁ : b_1 ⟶ b) (hq : (q₁.cons f₁).length = length.{u, u_1} (V := V) (a := b) nil)
  (h : p₁.comp (q₁.cons f₁) = p₂.comp nil), p₁ = p₂ ∧ q₁.cons f₁ = nil
Tactic: rcases q₂ with _ | ⟨q₂, f₂⟩
Cleared hypotheses: c_1, f₁, q₂, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ p₂ : Path.{u_1, u} a b
b_1 c_1 : V
q₁ : Path.{u_1, u} b b_1
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₂
q₂ : Path.{u_1, u} b c_1
hq : (q₁.cons f₁).length = q₂.length
h : p₁.comp (q₁.cons f₁) = p₂.comp q₂
cons :
  ∀ (f₁ : b_1 ⟶ b) (hq : (q₁.cons f₁).length = length.{u, u_1} (V := V) (a := b) nil)
    (h : p₁.comp (q₁.cons f₁) = p₂.comp nil), p₁ = p₂ ∧ q₁.cons f₁ = nil
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂
have cons₁ : ∀ {b_2 : V} (q₂ : Path.{u_1, u} b b_2) (f₂ : b_2 ⟶ c_1) (hq : (q₁.cons f₁).length = (q₂.cons f₂).length)
  (h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)), p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂
Tactic: rcases q₂ with _ | ⟨q₂, f₂⟩
Cleared hypotheses: q₂, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (hypothesis)
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ p₂ : Path.{u_1, u} a b
b_1 c_1 : V
q₁ : Path.{u_1, u} b b_1
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₂
b_2 : V
q₂ : Path.{u_1, u} b b_2
f₂ : b_2 ⟶ c_1
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂
have h₁ : b_1 = b_2 ∧ p₁.comp q₁ ≍ p₂.comp q₂ ∧ f₁ ≍ f₂
Tactic: simp only [comp_cons, cons.injEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ p₂ : Path.{u_1, u} a b
b_1 c_1 : V
q₁ : Path.{u_1, u} b b_1
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₂
b_2 : V
q₂ : Path.{u_1, u} b b_2
f₂ : b_2 ⟶ c_1
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : b_1 = b_2 ∧ p₁.comp q₁ ≍ p₂.comp q₂ ∧ f₁ ≍ f₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂
have cons : ∀ (q₂ : Path.{u_1, u} b b_1) (f₂ : b_1 ⟶ c_1) (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: obtain rfl := h.1
Cleared hypotheses: b_2, q₂, f₂, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c : V
p₁ p₂ : Path.{u_1, u} a b
b_1 c_1 : V
q₁ : Path.{u_1, u} b b_1
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₂
q₂ : Path.{u_1, u} b b_1
f₂ : b_1 ⟶ c_1
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₂
have cons : ∀ (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: obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq
Cleared hypotheses: p₂, ih, q₂, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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₂
have cons : p₁ = p₁ ∧ q₁.cons f₂ = q₁.cons f₂
Tactic: rw [h.2.2.eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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₂
⊢ p₁ = p₂ ∧ q₁ = q₂
have nil : ∀ {q₂ : Path.{u_1, u} b b} (hq : length.{u, u_1} (V := V) (a := b) nil = q₂.length) (h : p₁.comp nil = p₂.comp q₂),
  p₁ = p₂ ∧ nil = 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⟩
Cleared hypotheses: q₁, q₂, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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₂
⊢ p₁ = p₂ ∧ q₁ = q₂
have 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₂
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⟩
Cleared hypotheses: q₁, q₂, hq, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ ∃ (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
have 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
Tactic: cases n
Cleared hypotheses: n, hp
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ ∃ (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
have 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
Tactic: cases n
Cleared hypotheses: n, hp
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (hypothesis)
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
⊢ ∃ (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
have hp₁ : p.length = 0
Tactic: rw [length_cons, Nat.zero_add, Nat.add_eq_right] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain rfl := eq_of_length_zero p hp
Cleared hypotheses: c, p, q, h, hp
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ ∃ (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
have 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), cons nil q = f.toPath.comp q_1
Tactic: obtain rfl := eq_nil_of_length_zero p hp
Cleared hypotheses: p, h, hp
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (hypothesis)
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
⊢ ∃ (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
have hp₁ : p.length = n + 1
Tactic: rw [length_cons, Nat.add_right_cancel_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨x, q'', p'', hl, rfl⟩ := h hp
Cleared hypotheses: p, h, hp
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Path.{u_1, u} c b), ∃ (x : q.length = n), p = f.toPath.comp q
have nil : ∀ {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: 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⟩
Cleared hypotheses: p, n, hp
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Path.{u_1, u} c b), ∃ (x : q.length = n), p = f.toPath.comp q
have 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
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⟩
Cleared hypotheses: p, n, hp
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
have 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
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (hypothesis)
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
⊢ ∃ (c : V), ∃ (e : a ⟶ c), ∃ (p' : Path.{u_3, u_1} c b), p = e.toPath.comp p' ∧ p.length = p'.length + 1
have h_len : p.length = p.length - 1 + 1
Tactic: have h_len : p.length = (p.length - 1) + 1 := by lia
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ ∃ (c : V), ∃ (e : a ⟶ c), ∃ (p' : Path.{u_3, u_1} c b), p = e.toPath.comp p' ∧ p.length = p'.length + 1
have 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
Tactic: obtain ⟨c, e, p', hp', rfl⟩ := Path.eq_toPath_comp_of_length_eq_succ p h_len
Cleared hypotheses: p, h, h_len
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
have refine_1 : ∀ (h : p.length ≠ 0), ∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ b), p = p'.cons e
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ p.length ≠ 0 ↔ ∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ b), p = p'.cons e
have refine_2 : (∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ b), p = p'.cons e) → p.length ≠ 0
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ ∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ b), p = p'.cons e
have 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
Tactic: cases p with
    | nil => simp at h
    | cons p' e => exact ⟨_, p', e, rfl⟩
Cleared hypotheses: b, p, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ ∃ (c : V), ∃ (p' : Path.{u_3, u_1} a c), ∃ (e : c ⟶ b), p = p'.cons e
have 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
Tactic: cases p with
    | nil => simp at h
    | cons p' e => exact ⟨_, p', e, rfl⟩
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (hypothesis)
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
⊢ p.cons f = C.cons D
have h₁ : c = t ∧ p.toList = C.toList
Tactic: simp only [toList, List.cons.injEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ p.cons f = C.cons D
have obtain : ∀ (C : Path.{u_1, u} a c) (D : c ⟶ x) (hAC : p.toList = C.toList), p.cons f = C.cons D
Tactic: obtain ⟨rfl, hAC⟩ := h
Cleared hypotheses: t, C, D, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
hq' : q'.length ≤ n
h'' :
  Eq (α := { p : Path.{u_2, u_1} a_1 a_2 // p.length ≤ n })
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 a_2) ↦ p.length ≤ n) p' hp')
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 a_2) ↦ p.length ≤ n) q' hq')
⊢ Eq (α := BoundedPaths.{u_1, u_2} a_1 x (n + 1))
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ n + 1) (p'.cons α) hp)
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ n + 1) (q'.cons β) hq)
have a₁ : (↑(Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ n + 1) (p'.cons α) hp) : Path a_1 x) =
  (↑(Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ n + 1) (q'.cons β) hq) : Path a_1 x)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
hq' : q'.length ≤ n
h'' :
  Eq (α := { p : Path.{u_2, u_1} a_1 a_2 // p.length ≤ n })
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 a_2) ↦ p.length ≤ n) p' hp')
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 a_2) ↦ p.length ≤ n) q' hq')
⊢ p'.cons α = q'.cons β
have a₁ : p'.cons β = q'.cons β
Tactic: rw [h, show p' = q' from Subtype.mk.inj h'']
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
hq' : q'.length ≤ n
h'' :
  Eq (α := { p : Path.{u_2, u_1} a_1 a_2 // p.length ≤ n })
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 a_2) ↦ p.length ≤ n) p' hp')
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 a_2) ↦ p.length ≤ n) q' hq')
a₁ : p'.cons β = q'.cons β
⊢ p'.cons α = q'.cons β
have a₂ : q'.cons β = q'.cons β
Tactic: rw [h, show p' = q' from Subtype.mk.inj h'']
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F : Prefunctor.{v₁, v₂, u₁, u₂} V W
a b : V
p : Path.{v₁, u₁} a b
c b_1 : V
q : Path.{v₁, u₁} b b_1
e : b_1 ⟶ c
⊢ (F.mapPath (p.comp q)).cons (F.map e) = ((F.mapPath p).comp (F.mapPath q)).cons (F.map e)
have rw : ((F.mapPath p).comp (F.mapPath q)).cons (F.map e) = ((F.mapPath p).comp (F.mapPath q)).cons (F.map e)
Tactic: rw [mapPath_comp p q]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
a b_1 b b_2 : V
q : Path.{v₁, u₁} a b_2
e : b_2 ⟶ b
⊢ mapPath (𝟭q V) (q.cons e) = q.cons e
have dsimp : Path.cons (mapPath (𝟭q V) q) e = q.cons e
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
a b_1 b b_2 : V
q : Path.{v₁, u₁} a b_2
e : b_2 ⟶ b
⊢ Path.cons (mapPath (𝟭q V) q) e = q.cons e
have rw : q.cons e = q.cons e
Tactic: rw [mapPath_id q]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F : Prefunctor.{v₁, v₂, u₁, u₂} V W
U : Type u₃
inst_2 : Quiver.{v₃, u₃} U
G : Prefunctor.{v₂, v₃, u₂, u₃} W U
a b : V
p : Path.{v₁, u₁} a b
⊢ (F ⋙q G).mapPath p = G.mapPath (F.mapPath p)
have nil : Eq (α := Path.{v₃, u₃} ((F ⋙q G).obj a) ((F ⋙q G).obj a)) ((F ⋙q G).mapPath Path.nil) (G.mapPath (F.mapPath Path.nil))
Tactic: induction p with
  | nil => rfl
  | cons x y h => simp [h]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F : Prefunctor.{v₁, v₂, u₁, u₂} V W
U : Type u₃
inst_2 : Quiver.{v₃, u₃} U
G : Prefunctor.{v₂, v₃, u₂, u₃} W U
a b : V
p : Path.{v₁, u₁} a b
nil :
  Eq (α := Path.{v₃, u₃} ((F ⋙q G).obj a) ((F ⋙q G).obj a)) ((F ⋙q G).mapPath Path.nil) (G.mapPath (F.mapPath Path.nil))
⊢ (F ⋙q G).mapPath p = G.mapPath (F.mapPath p)
have cons : ∀ {b c : V} (x : Path.{v₁, u₁} a b) (y : b ⟶ c) (h : (F ⋙q G).mapPath x = G.mapPath (F.mapPath x)),
  (F ⋙q G).mapPath (x.cons y) = G.mapPath (F.mapPath (x.cons y))
Tactic: induction p with
  | nil => rfl
  | cons x y h => simp [h]
Cleared hypotheses: p