awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
v b_1 c : V
pPrev : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih :
  ∀ (hv : v ∈ pPrev.vertices),
    ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b_1), pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ :
  v = (pPrev.cons e).end →
    ∃ (p₁ : Path.{u_2, u_1} a v),
      ∃ (p₂ : Path.{u_2, u_1} v (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hxPrev : v ∈ pPrev.vertices
hxe_ne : v ≠ (pPrev.cons e).end
q₁ : Path.{u_2, u_1} a v
q₂ : Path.{u_2, u_1} v b_1
h_prev : pPrev = q₁.comp q₂
h_not_tail : ¬v ∈ q₂.vertices.tail
q₂' : Path.{u_2, u_1} v (pPrev.cons e).end := q₂.cons e
⊢ ∃ (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
have h_no_tail : ¬v ∈ q₂'.vertices.tail
Tactic: have h_no_tail : v ∉ q₂'.vertices.tail := by grind [vertices_cons, end_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (hypothesis)
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
⊢ ∃ (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
have 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
Tactic: have h_case₂ : v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end →
        ∃ (p₁ : Path a v) (p₂ : Path v (pPrev.cons e).end),
          pPrev.cons e = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail := by
      intro hxPrev hxe_ne
      obtain ⟨q₁, q₂, h_prev, h_not_tail⟩ := ih hxPrev
      let q₂' : Path v (pPrev.cons e).end := q₂.cons e
      have h_no_tail : v ∉ q₂'.vertices.tail := by grind [vertices_cons, end_cons]
      exact ⟨q₁, q₂', by simp [q₂', h_prev], h_no_tail⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
v b_1 c : V
pPrev : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih :
  ∀ (hv : v ∈ pPrev.vertices),
    ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b_1), pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
h_case₁ :
  v = (pPrev.cons e).end →
    ∃ (p₁ : Path.{u_2, u_1} a v),
      ∃ (p₂ : Path.{u_2, u_1} v (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_case₂ :
  v ∈ pPrev.vertices →
    v ≠ (pPrev.cons e).end →
      ∃ (p₁ : Path.{u_2, u_1} a v),
        ∃ (p₂ : Path.{u_2, u_1} v (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_in_prefix : v ∈ pPrev.vertices
⊢ ∃ (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
have pos : ∀ (h_eq_end : v = (pPrev.cons e).end),
  ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
Tactic: by_cases h_eq_end : v = (pPrev.cons e).end
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
v b_1 c : V
pPrev : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih :
  ∀ (hv : v ∈ pPrev.vertices),
    ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b_1), pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
h_case₁ :
  v = (pPrev.cons e).end →
    ∃ (p₁ : Path.{u_2, u_1} a v),
      ∃ (p₂ : Path.{u_2, u_1} v (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_case₂ :
  v ∈ pPrev.vertices →
    v ≠ (pPrev.cons e).end →
      ∃ (p₁ : Path.{u_2, u_1} a v),
        ∃ (p₂ : Path.{u_2, u_1} v (pPrev.cons e).end), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_in_prefix : v ∈ pPrev.vertices
pos :
  ∀ (h_eq_end : v = (pPrev.cons e).end),
    ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
⊢ ∃ (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
have neg : ∀ (h_eq_end : ¬v = (pPrev.cons e).end),
  ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v c), pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
Tactic: by_cases h_eq_end : v = (pPrev.cons e).end
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
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
⊢ ∃ (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
have 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
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
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
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
⊢ ∃ (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
have 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
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
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
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
⊢ ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
have nil : ∀ (hv : Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := a) nil) v),
  ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v a), nil = 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
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
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
⊢ ∃ (p₁ : Path.{u_2, u_1} a v), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
have 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
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
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Weight (goal)
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
⊢ weightOfEPs w (p.cons e) = weightOfEPs w p * w b c
have 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
Tactic: unfold weightOfEPs
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Weight (goal)
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
⊢ 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)
have nil : 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: induction q with
  | nil => simp
  | cons _ _ ih => simp [ih, mul_assoc]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Weight (goal)
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)
⊢ 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)
have 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))
Tactic: induction q with
  | nil => simp
  | cons _ _ ih => simp [ih, mul_assoc]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Weight (hypothesis)
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)
⊢ LT.lt.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) (p.cons e))
have he : 0 < w e
Tactic: have he : 0 < w e := hw e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Weight (goal)
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
⊢ LT.lt.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)
have nil : LT.lt.{u_2} (α := R) 0 (weight.{u_1, u_2, u_3} fun {i j : V} ↦ w (i := i) nil)
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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Weight (goal)
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)
⊢ LT.lt.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)
have 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))
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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Weight (hypothesis)
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)
⊢ LE.le.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) (p.cons e))
have he : 0 ≤ w e
Tactic: have he : 0 ≤ w e := hw e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Weight (goal)
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
⊢ LE.le.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)
have nil : LE.le.{u_2} (α := R) 0 (weight.{u_1, u_2, u_3} fun {i j : V} ↦ w (i := i) nil)
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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Weight (goal)
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)
⊢ LE.le.{u_2} (α := R) 0 (weight (fun {i j : V} ↦ w) p)
have 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))
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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Weight (goal)
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
⊢ 0 < weightOfEPs w p
have hw₁ : ∀ {i j : V} (e : i ⟶ j), 0 < w i j
Tactic: apply weight_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Weight (goal)
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
⊢ 0 ≤ weightOfEPs w p
have hw₁ : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w i j
Tactic: apply weight_nonneg
-- 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
hzero : p.length = 0
⊢ a = b
have nil : ∀ (hzero : length.{u, u_1} (V := V) (a := a) nil = 0), a = a
Tactic: cases p
Cleared hypotheses: b, p, hzero
-- 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
hzero : p.length = 0
nil : ∀ (hzero : length.{u, u_1} (V := V) (a := a) Path.nil = 0), a = a
⊢ a = b
have 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
Tactic: cases p
Cleared hypotheses: p, hzero
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
Goal:
V : Type u
inst : Quiver.{u_1, u} V
a : V
p : Path.{u_1, u} a a
hzero : p.length = 0
⊢ p = nil
have nil : ∀ (hzero : length.{u, u_1} (V := V) (a := a) nil = 0), Eq (α := Path.{u_1, u} a a) nil nil
Tactic: cases p
Cleared hypotheses: p, hzero
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ p = Path.nil
have 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
Tactic: cases p
Cleared hypotheses: p, hzero
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ comp nil (p.cons a_1) = p.cons a_1
have rw : (comp nil p).cons a_1 = p.cons a_1
Tactic: rw [comp_cons, nil_comp p]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ comp nil (p.cons a_1) = p.cons a_1
have rw₁ : p.cons a_1 = p.cons a_1
Tactic: rw [comp_cons, nil_comp p]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ (p.comp q).comp (r.cons a_1) = p.comp (q.comp (r.cons a_1))
have rw : ((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]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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))
⊢ (p.comp q).comp (r.cons a_1) = p.comp (q.comp (r.cons a_1))
have rw₁ : ((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]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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)
⊢ (p.comp q).comp (r.cons a_1) = p.comp (q.comp (r.cons a_1))
have rw₂ : ((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]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path (goal)
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
⊢ (p.comp q).comp (r.cons a_1) = p.comp (q.comp (r.cons a_1))
have rw₃ : (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]
-- 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
⊢ p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂
have refine : ∀ (h : p₁.comp q₁ = p₂.comp q₂), p₁ = p₂ ∧ q₁ = q₂
Tactic: refine ⟨fun h => ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- 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₂ : 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₂
have nil : ∀ (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: rcases q₂ with _ | ⟨q₂, f₂⟩
Cleared hypotheses: 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₂ : 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
⊢ p₁ = p₂ ∧ Path.nil = q₂
have 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₂
Tactic: rcases q₂ with _ | ⟨q₂, f₂⟩
Cleared hypotheses: q₂, hq, h