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
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
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
cons :
  ∀ (h_in_prefix : v ∈ pPrev.vertices),
    ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
cons₁ :
  ∀ (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:
cases hv' with
    | inl h_in_prefix =>
      by_cases h_eq_end : v = (pPrev.cons e).end
      · exact h_case₁ h_eq_end
      · exact h_case₂ h_in_prefix h_eq_end
    | inr h_eq_end => exact h_case₁ h_eq_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 : V
hv : v ∈ p.vertices
nil :
  ∀ (hv : Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := a) Path.nil) v),
    ∃ (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
cons :
  ∀ {b c : V} (pPrev : Path.{u_2, u_1} a b) (e : b ⟶ c)
    (ih :
      ∀ (hv : v ∈ pPrev.vertices),
        ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b), pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail)
    (hv : v ∈ (pPrev.cons e).vertices),
    ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
⊢ ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
induction p with
  | nil =>
    have hxa : v = a := by
      simpa [vertices_nil, List.mem_singleton] using hv
    subst hxa
    exact ⟨Path.nil, Path.nil, by simp only [comp_nil],
      by simp only [vertices_nil, tail_cons, not_mem_nil, not_false_eq_true]⟩
  | cons pPrev e ih =>
    have hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end := by
      simpa using (mem_vertices_cons pPrev e).1 hv
    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]⟩
    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⟩
    cases hv' with
    | inl h_in_prefix =>
      by_cases h_eq_end : v = (pPrev.cons e).end
      · exact h_case₁ h_eq_end
      · exact h_case₂ h_in_prefix h_eq_end
    | inr h_eq_end => exact h_case₁ h_eq_end

Premises used: Quiver.Path.nil, Quiver.Path.cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Monoid R
w : {i j : V} → (i ⟶ j) → R
a : V
⊢ Eq.{u_2 + 1} (α := R) (weight.{u_1, u_2, u_3} fun {i j : V} ↦ w (i := a) nil) 1

Tactic:
simp [weight]

Premises used: Quiver.Path.weight
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Monoid R
w : {i j : V} → (i ⟶ j) → R
a b c : V
p : Path.{u_3, u_1} a b
e : b ⟶ c
⊢ weight (fun {i j : V} ↦ w) (p.cons e) = weight (fun {i j : V} ↦ w) p * w e

Tactic:
simp [weight]

Premises used: Quiver.Path.weight
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Monoid R
w : V → V → R
a : V
⊢ weightOfEPs.{u_1, u_2, u_3} w (i := a) nil = 1

Tactic:
simp [weightOfEPs]

Premises used: Quiver.Path.weightOfEPs
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Monoid R
w : V → V → R
a b c : V
p : Path.{u_3, u_1} a b
e : b ⟶ c
unfold : weight (fun {i j : V} (x : i ⟶ j) ↦ w i j) (p.cons e) = weight (fun {i j : V} (x : i ⟶ j) ↦ w i j) p * w b c
⊢ weightOfEPs w (p.cons e) = weightOfEPs w p * w b c

Tactic:
unfold weightOfEPs

Premises used: Quiver.Path.weightOfEPs
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Monoid R
w : V → V → R
a b c : V
p : Path.{u_3, u_1} a b
e : b ⟶ c
⊢ weight (fun {i j : V} (x : i ⟶ j) ↦ w i j) (p.cons e) = weight (fun {i j : V} (x : i ⟶ j) ↦ w i j) p * w b c

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Monoid R
w : {i j : V} → (i ⟶ j) → R
a b c : V
p : Path.{u_3, u_1} a b
⊢ weight (fun {i j : V} ↦ w) (p.comp nil) =
    HMul.hMul (α := R) (weight (fun {i j : V} ↦ w) p) (weight.{u_1, u_2, u_3} fun {i j : V} ↦ w (i := b) nil)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Monoid R
w : {i j : V} → (i ⟶ j) → R
a b c : V
p : Path.{u_3, u_1} a b
b_1 c_1 : V
a_1 : Path.{u_3, u_1} b b_1
a_2 : b_1 ⟶ c_1
ih :
  weight (fun {i j : V} ↦ w) (p.comp a_1) =
    HMul.hMul (α := R) (weight (fun {i j : V} ↦ w) p) (weight (fun {i j : V} ↦ w) a_1)
⊢ weight (fun {i j : V} ↦ w) (p.comp (a_1.cons a_2)) =
    HMul.hMul (α := R) (weight (fun {i j : V} ↦ w) p) (weight (fun {i j : V} ↦ w) (a_1.cons a_2))

Tactic:
simp [ih, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Monoid R
w : {i j : V} → (i ⟶ j) → R
a b c : V
p : Path.{u_3, u_1} a b
q : Path.{u_3, u_1} b c
nil :
  weight (fun {i j : V} ↦ w) (p.comp Path.nil) =
    HMul.hMul (α := R) (weight (fun {i j : V} ↦ w) p) (weight.{u_1, u_2, u_3} fun {i j : V} ↦ w (i := b) Path.nil)
cons :
  ∀ {b_1 c : V} (a_1 : Path.{u_3, u_1} b b_1) (a_2 : b_1 ⟶ c)
    (ih :
      weight (fun {i j : V} ↦ w) (p.comp a_1) =
        HMul.hMul (α := R) (weight (fun {i j : V} ↦ w) p) (weight (fun {i j : V} ↦ w) a_1)),
    weight (fun {i j : V} ↦ w) (p.comp (a_1.cons a_2)) =
      HMul.hMul (α := R) (weight (fun {i j : V} ↦ w) p) (weight (fun {i j : V} ↦ w) (a_1.cons a_2))
⊢ weight (fun {i j : V} ↦ w) (p.comp q) =
    HMul.hMul (α := R) (weight (fun {i j : V} ↦ w) p) (weight (fun {i j : V} ↦ w) q)

Tactic:
induction q with
  | nil => simp
  | cons _ _ ih => simp [ih, mul_assoc]

Premises used: Quiver.Path.nil, mul_assoc, Quiver.Path.cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Monoid R
w : V → V → R
a b c : V
p : Path.{u_3, u_1} a b
q : Path.{u_3, u_1} b c
⊢ weightOfEPs w (p.comp q) = weightOfEPs w p * weightOfEPs w q

Tactic:
simp [weightOfEPs, weight_comp]

Premises used: Quiver.Path.weightOfEPs, Quiver.Path.weight_comp
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 < w e
i j : V
⊢ LT.lt.{u_2} (α := R) 0 (weight.{u_1, u_2, u_3} fun {i j : V} ↦ w (i := i) nil)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 < w e
i j b c : V
p : Path.{u_3, u_1} i b
e : b ⟶ c
ih : LT.lt.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)
⊢ 0 < w e

Tactic:
have he : 0 < w e := hw e
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 < w e
i j b c : V
p : Path.{u_3, u_1} i b
e : b ⟶ c
ih : LT.lt.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)
he : 0 < w e
⊢ LT.lt.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) (p.cons e))

Tactic:
simpa [weight_cons] using mul_pos ih he

Premises used: mul_pos, Quiver.Path.weight_cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 < w e
i j : V
p : Path.{u_3, u_1} i j
nil : LT.lt.{u_2} (α := R) 0 (weight.{u_1, u_2, u_3} fun {i j : V} ↦ w (i := i) Path.nil)
cons :
  ∀ {b c : V} (p : Path.{u_3, u_1} i b) (e : b ⟶ c) (ih : LT.lt.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)),
    LT.lt.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) (p.cons e))
⊢ LT.lt.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)

Tactic:
induction p with
  | nil =>
      simp
  | cons p e ih =>
      have he : 0 < w e := hw e
      simpa [weight_cons] using mul_pos ih he

Premises used: Quiver.Path.nil, Quiver.Path.cons, Quiver.Path.weight_cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w e
i j : V
⊢ LE.le.{u_2} (α := R) 0 (weight.{u_1, u_2, u_3} fun {i j : V} ↦ w (i := i) nil)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w e
i j b c : V
p : Path.{u_3, u_1} i b
e : b ⟶ c
ih : LE.le.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)
⊢ 0 ≤ w e

Tactic:
have he : 0 ≤ w e := hw e
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w e
i j b c : V
p : Path.{u_3, u_1} i b
e : b ⟶ c
ih : LE.le.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)
he : 0 ≤ w e
⊢ LE.le.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) (p.cons e))

Tactic:
simpa [weight_cons] using mul_nonneg ih he

Premises used: mul_nonneg, Quiver.Path.weight_cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w e
i j : V
p : Path.{u_3, u_1} i j
nil : LE.le.{u_2} (α := R) 0 (weight.{u_1, u_2, u_3} fun {i j : V} ↦ w (i := i) Path.nil)
cons :
  ∀ {b c : V} (p : Path.{u_3, u_1} i b) (e : b ⟶ c) (ih : LE.le.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)),
    LE.le.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) (p.cons e))
⊢ LE.le.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)

Tactic:
induction p with
  | nil =>
      simp
  | cons p e ih =>
      have he : 0 ≤ w e := hw e
      simpa [weight_cons] using mul_nonneg ih he

Premises used: Quiver.Path.nil, Quiver.Path.cons, Quiver.Path.weight_cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : V → V → R
hw : ∀ (i j : V), 0 < w i j
i j : V
p : Path.{u_3, u_1} i j
hw₁ : ∀ {i j : V} (e : i ⟶ j), 0 < w i j
⊢ 0 < weightOfEPs w p

Tactic:
apply weight_pos

Premises used: Quiver.Path.weight_pos
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : V → V → R
hw : ∀ (i j : V), 0 < w i j
i_1 j_1 : V
p : Path.{u_3, u_1} i_1 j_1
i j : V
e : i ⟶ j
⊢ 0 < w i j

Tactic:
hw _ _
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : V → V → R
hw : ∀ (i j : V), 0 < w i j
i_1 j_1 : V
p : Path.{u_3, u_1} i_1 j_1
i j : V
e : i ⟶ j
⊢ 0 < w i j

Tactic:
exact hw _ _
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : V → V → R
hw : ∀ (i j : V), 0 ≤ w i j
i j : V
p : Path.{u_3, u_1} i j
hw₁ : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w i j
⊢ 0 ≤ weightOfEPs w p

Tactic:
apply weight_nonneg

Premises used: Quiver.Path.weight_nonneg
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : V → V → R
hw : ∀ (i j : V), 0 ≤ w i j
i_1 j_1 : V
p : Path.{u_3, u_1} i_1 j_1
i j : V
e : i ⟶ j
⊢ 0 ≤ w i j

Tactic:
hw _ _
-- Module: Mathlib.Combinatorics.Quiver.Path.Weight
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
R : Type u_2
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
w : V → V → R
hw : ∀ (i j : V), 0 ≤ w i j
i_1 j_1 : V
p : Path.{u_3, u_1} i_1 j_1
i j : V
e : i ⟶ j
⊢ 0 ≤ w i j

Tactic:
exact hw _ _
-- 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
e : b ⟶ a
h : nil = p.cons e
⊢ False

Tactic:
injection h
-- 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
e : b ⟶ a
h : p.cons e = nil
⊢ False

Tactic:
injection h
-- 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 b
p' : Path.{u_1, u} a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ b = c

Tactic:
injection h
-- 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 b
p' : Path.{u_1, u} a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ p ≍ p'

Tactic:
injection h
-- 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 b
p' : Path.{u_1, u} a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ e ≍ e'

Tactic:
injection h
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a : V
⊢ length.{u, u_1} (V := V) (a := a) nil = 0

Tactic:
rfl

Premises used: Quiver.Path.length, 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
e : b ⟶ c
⊢ (p.cons e).length = p.length + 1

Tactic:
rfl

Premises used: Quiver.Path.length, 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
hzero : p.length = 0
nil : ∀ (hzero : length.{u, u_1} (V := V) (a := a) Path.nil = 0), a = a
cons : ∀ {b_1 : V} (a_1 : Path.{u_1, u} a b_1) (a_2 : b_1 ⟶ b) (hzero : (a_1.cons a_2).length = 0), a = b
⊢ a = b

Tactic:
cases p
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a : V
hzero : length.{u, u_1} (V := V) (a := a) nil = 0
⊢ a = a

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b b_1 : V
a_1 : Path.{u_1, u} a b_1
a_2 : b_1 ⟶ b
hzero : (a_1.cons a_2).length = 0
⊢ a = b

Tactic:
cases Nat.succ_ne_zero _ hzero

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a : V
p : Path.{u_1, u} a a
hzero : p.length = 0
nil : ∀ (hzero : length.{u, u_1} (V := V) (a := a) Path.nil = 0), Eq (α := Path.{u_1, u} a a) Path.nil Path.nil
cons : ∀ {b : V} (a_1 : Path.{u_1, u} a b) (a_2 : b ⟶ a) (hzero : (a_1.cons a_2).length = 0), a_1.cons a_2 = Path.nil
⊢ p = Path.nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a : V
hzero : length.{u, u_1} (V := V) (a := a) nil = 0
⊢ Eq (α := Path.{u_1, u} a a) nil nil

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b : V
a_1 : Path.{u_1, u} a b
a_2 : b ⟶ a
hzero : (a_1.cons a_2).length = 0
⊢ a_1.cons a_2 = nil

Tactic:
simp at hzero
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b : V
e : a ⟶ b
⊢ e.toPath.length = 1

Tactic:
rfl

Premises used: Quiver.Hom.toPath, Quiver.Path.length, 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 b
q : Path.{u_1, u} b c
e : c ⟶ d
⊢ p.comp (q.cons e) = (p.comp q).cons e

Tactic:
rfl

Premises used: 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 = p

Tactic:
rfl

Premises used: Quiver.Path.comp, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a x b : V
p : Path.{u_1, u} a b
a_1 : b ⟶ x
rw : (comp nil p).cons a_1 = p.cons a_1
rw₁ rw₂ : p.cons a_1 = p.cons a_1
⊢ comp nil (p.cons a_1) = p.cons a_1

Tactic:
rw [comp_cons, nil_comp p]

Premises used: Quiver.Path.comp_cons
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a b c x : V
p : Path.{u_1, u} a b
q : Path.{u_1, u} b c
b_1 : V
r : Path.{u_1, u} c b_1
a_1 : b_1 ⟶ x
rw : ((p.comp q).comp r).cons a_1 = p.comp (q.comp (r.cons a_1))
rw₁ : ((p.comp q).comp r).cons a_1 = p.comp ((q.comp r).cons a_1)
rw₂ : ((p.comp q).comp r).cons a_1 = (p.comp (q.comp r)).cons a_1
rw₃ rw₄ : (p.comp (q.comp r)).cons a_1 = (p.comp (q.comp r)).cons a_1
⊢ (p.comp q).comp (r.cons a_1) = p.comp (q.comp (r.cons a_1))

Tactic:
rw [comp_cons, comp_cons, comp_cons, comp_assoc p q r]

Premises used: Quiver.Path.comp_cons
-- 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
hq : q₁.length = q₁.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
p₁ p₂ : Path.{u_1, u} a b
q₁ q₂ : Path.{u_1, u} b c
hq : q₁.length = q₂.length
refine : ∀ (h : p₁.comp q₁ = p₂.comp q₂), p₁ = p₂ ∧ q₁ = q₂
⊢ p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂

Tactic:
refine ⟨fun h => ?_, by rintro ⟨rfl, 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₂ : 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₂
nil :
  ∀ (hq : length.{u, u_1} (V := V) (a := b) Path.nil = length.{u, u_1} (V := V) (a := b) Path.nil)
    (h : p₁.comp Path.nil = p₂.comp Path.nil), p₁ = p₂ ∧ Eq (α := Path.{u_1, u} b b) Path.nil Path.nil
nil₁ :
  ∀ {b_1 : V} (q₂ : Path.{u_1, u} b b_1) (f₂ : b_1 ⟶ b)
    (hq : length.{u, u_1} (V := V) (a := b) Path.nil = (q₂.cons f₂).length)
    (h : p₁.comp Path.nil = p₂.comp (q₂.cons f₂)), p₁ = p₂ ∧ Path.nil = q₂.cons f₂
⊢ p₁ = p₂ ∧ Path.nil = q₂

Tactic:
rcases q₂ with _ | ⟨q₂, f₂⟩
-- 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
hq : length.{u, u_1} (V := V) (a := b) nil = length.{u, u_1} (V := V) (a := b) nil
h : p₁.comp nil = p₂.comp nil
⊢ p₁ = p₂ ∧ Eq (α := Path.{u_1, u} b b) nil nil

Tactic:
⟨h, 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₁ p₂ : Path.{u_1, u} a b
hq : length.{u, u_1} (V := V) (a := b) nil = length.{u, u_1} (V := V) (a := b) nil
h : p₁.comp nil = p₂.comp nil
⊢ p₁ = p₂ ∧ Eq (α := Path.{u_1, u} b b) nil nil

Tactic:
exact ⟨h, 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
b_1 : V
q₂ : Path.{u_1, u} b b_1
f₂ : b_1 ⟶ b
hq : length.{u, u_1} (V := V) (a := b) nil = (q₂.cons f₂).length
h : p₁.comp nil = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ nil = q₂.cons f₂

Tactic:
cases hq
-- 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
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
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₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂

Tactic:
rcases q₂ with _ | ⟨q₂, f₂⟩
-- 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
b_1 : V
q₁ : Path.{u_1, u} b b_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₂
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:
cases hq
-- 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
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₂)
⊢ b_1 = b_2 ∧ p₁.comp q₁ ≍ p₂.comp q₂ ∧ f₁ ≍ f₂

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

Premises used: Quiver.Path.cons.injEq, Quiver.Path.comp_cons
-- 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
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₂
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₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Tactic:
obtain rfl := h.1

Premises used: And.left, 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
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₂
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₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Tactic:
obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq

Premises used: Nat.succ.inj, And.right, And.left, HEq.eq, rfl