Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: David WΓ€rn, Scott Morrison
Ported by: JoΓ«l Riou

! This file was ported from Lean 3 source module combinatorics.quiver.path
! leanprover-community/mathlib commit 18a5306c091183ac90884daa9373fa3b178e8607
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Combinatorics.Quiver.Basic
import Mathlib.Logic.Lemmas

/-!
# Paths in quivers

Given a quiver `V`, we define the type of paths from `a : V` to `b : V` as an inductive
family. We define composition of paths and the action of prefunctors on paths.
-/

open Function

universe v vβ vβ u uβ uβ

namespace Quiver

/-- `Path a b` is the type of paths from `a` to `b` through the arrows of `G`. -/
inductive Path: {V : Type u} β [inst : Quiver V] β V β V β Sort (max(u+1)v)Path {V: Type uV : Type u: Type (u+1)Type u} [Quiver: Type ?u.4 β Type (max?u.4v)Quiver.{v} V: Type uV] (a: Va : V: Type uV) : V: Type uV β Sort max (u + 1) v: Type (max(u+1)v)SortSort max (u + 1) v: Type (max(u+1)v) Sort max (u + 1) v: Type (max(u+1)v)maxSort max (u + 1) v: Type (max(u+1)v) (u + 1) v
| nil: {V : Type u} β [inst : Quiver V] β {a : V} β Path a anil : Path: {V : Type u} β [inst : Quiver V] β V β V β Sort (max(u+1)v)Path a: Va a: Va
| cons: {V : Type u} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons : β {b: Vb c: Vc : V: Type uV}, Path: {V : Type u} β [inst : Quiver V] β V β V β Sort (max(u+1)v)Path a: Va b: Vb β (b: Vb βΆ c: Vc) β Path: {V : Type u} β [inst : Quiver V] β V β V β Sort (max(u+1)v)Path a: Va c: Vc
#align quiver.path Quiver.Path: {V : Type u} β [inst : Quiver V] β V β V β Sort (max(u+1)v)Quiver.Path

-- See issue lean4#2049
compile_inductive% Path: {V : Type u} β [inst : Quiver V] β V β V β Sort (max(u+1)v)Path

/-- An arrow viewed as a path of length one. -/
def Hom.toPath: {V : Type u_1} β [inst : Quiver V] β {a b : V} β (a βΆ b) β Path a bHom.toPath {V: Type ?u.1485V} [Quiver: Type ?u.1485 β Type (max?u.1485?u.1486)Quiver V: ?m.1482V] {a: Va b: Vb : V: ?m.1482V} (e: a βΆ be : a: Va βΆ b: Vb) : Path: {V : Type ?u.1508} β [inst : Quiver V] β V β V β Sort (max(?u.1508+1)?u.1509)Path a: Va b: Vb :=
Path.nil: {V : Type ?u.1526} β [inst : Quiver V] β {a : V} β Path a aPath.nil.cons: {V : Type ?u.1536} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e: a βΆ be
#align quiver.hom.to_path Quiver.Hom.toPath: {V : Type u_1} β [inst : Quiver V] β {a b : V} β (a βΆ b) β Path a bQuiver.Hom.toPath

namespace Path

variable {V: Type uV : Type u: Type (u+1)Type u} [Quiver: Type ?u.3675 β Type (max?u.3675?u.3676)Quiver V: Type uV] {a: Va b: Vb c: Vc d: Vd : V: Type uV}

lemma nil_ne_cons: β (p : Path a b) (e : b βΆ a), nil β  cons p enil_ne_cons (p: Path a bp : Path: {V : Type ?u.1638} β [inst : Quiver V] β V β V β Sort (max(?u.1638+1)?u.1639)Path a: Va b: Vb) (e: b βΆ ae : b: Vb βΆ a: Va) : Path.nil: {V : Type ?u.1669} β [inst : Quiver V] β {a : V} β Path a aPath.nil β  p: Path a bp.cons: {V : Type ?u.1683} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e: b βΆ ae :=
fun h: ?m.1715h => byGoals accomplished! π V: Type uinstβ: Quiver Va, b, c, d: Vp: Path a be: b βΆ ah: nil = cons p eFalseinjection h: nil = cons p ehGoals accomplished! π
#align quiver.path.nil_ne_cons Quiver.Path.nil_ne_cons: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b) (e : b βΆ a), nil β  cons p eQuiver.Path.nil_ne_cons

lemma cons_ne_nil: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b) (e : b βΆ a), cons p e β  nilcons_ne_nil (p: Path a bp : Path: {V : Type ?u.1743} β [inst : Quiver V] β V β V β Sort (max(?u.1743+1)?u.1744)Path a: Va b: Vb) (e: b βΆ ae : b: Vb βΆ a: Va) : p: Path a bp.cons: {V : Type ?u.1774} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e: b βΆ ae β  Path.nil: {V : Type ?u.1799} β [inst : Quiver V] β {a : V} β Path a aPath.nil :=
fun h: ?m.1816h => byGoals accomplished! π V: Type uinstβ: Quiver Va, b, c, d: Vp: Path a be: b βΆ ah: cons p e = nilFalseinjection h: cons p e = nilhGoals accomplished! π
#align quiver.path.cons_ne_nil Quiver.Path.cons_ne_nil: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b) (e : b βΆ a), cons p e β  nilQuiver.Path.cons_ne_nil

lemma obj_eq_of_cons_eq_cons: β {V : Type u} [inst : Quiver V] {a b c d : V} {p : Path a b} {p' : Path a c} {e : b βΆ d} {e' : c βΆ d},
cons p e = cons p' e' β b = cobj_eq_of_cons_eq_cons {p: Path a bp : Path: {V : Type ?u.1844} β [inst : Quiver V] β V β V β Sort (max(?u.1844+1)?u.1845)Path a: Va b: Vb} {p': Path a cp' : Path: {V : Type ?u.1859} β [inst : Quiver V] β V β V β Sort (max(?u.1859+1)?u.1860)Path a: Va c: Vc}
{e: b βΆ de : b: Vb βΆ d: Vd} {e': c βΆ de' : c: Vc βΆ d: Vd} (h: cons p e = cons p' e'h : p: Path a bp.cons: {V : Type ?u.1902} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e: b βΆ de = p': Path a cp'.cons: {V : Type ?u.1927} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e': c βΆ de') : b: Vb = c: Vc := byGoals accomplished! π V: Type uinstβ: Quiver Va, b, c, d: Vp: Path a bp': Path a ce: b βΆ de': c βΆ dh: cons p e = cons p' e'b = cinjection h: cons p e = cons p' e'hGoals accomplished! π
#align quiver.path.obj_eq_of_cons_eq_cons Quiver.Path.obj_eq_of_cons_eq_cons: β {V : Type u} [inst : Quiver V] {a b c d : V} {p : Path a b} {p' : Path a c} {e : b βΆ d} {e' : c βΆ d},
cons p e = cons p' e' β b = cQuiver.Path.obj_eq_of_cons_eq_cons

lemma heq_of_cons_eq_cons: β {V : Type u} [inst : Quiver V] {a b c d : V} {p : Path a b} {p' : Path a c} {e : b βΆ d} {e' : c βΆ d},
cons p e = cons p' e' β HEq p p'heq_of_cons_eq_cons {p: Path a bp : Path: {V : Type ?u.2015} β [inst : Quiver V] β V β V β Sort (max(?u.2015+1)?u.2016)Path a: Va b: Vb} {p': Path a cp' : Path: {V : Type ?u.2030} β [inst : Quiver V] β V β V β Sort (max(?u.2030+1)?u.2031)Path a: Va c: Vc}
{e: b βΆ de : b: Vb βΆ d: Vd} {e': c βΆ de' : c: Vc βΆ d: Vd} (h: cons p e = cons p' e'h : p: Path a bp.cons: {V : Type ?u.2073} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e: b βΆ de = p': Path a cp'.cons: {V : Type ?u.2098} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e': c βΆ de') : HEq: {Ξ± : Sort ?u.2116} β Ξ± β {Ξ² : Sort ?u.2116} β Ξ² β PropHEq p: Path a bp p': Path a cp' := byGoals accomplished! π V: Type uinstβ: Quiver Va, b, c, d: Vp: Path a bp': Path a ce: b βΆ de': c βΆ dh: cons p e = cons p' e'HEq p p'injection h: cons p e = cons p' e'hGoals accomplished! π
#align quiver.path.heq_of_cons_eq_cons Quiver.Path.heq_of_cons_eq_cons: β {V : Type u} [inst : Quiver V] {a b c d : V} {p : Path a b} {p' : Path a c} {e : b βΆ d} {e' : c βΆ d},
cons p e = cons p' e' β HEq p p'Quiver.Path.heq_of_cons_eq_cons

lemma hom_heq_of_cons_eq_cons: β {V : Type u} [inst : Quiver V] {a b c d : V} {p : Path a b} {p' : Path a c} {e : b βΆ d} {e' : c βΆ d},
cons p e = cons p' e' β HEq e e'hom_heq_of_cons_eq_cons {p: Path a bp : Path: {V : Type ?u.2188} β [inst : Quiver V] β V β V β Sort (max(?u.2188+1)?u.2189)Path a: Va b: Vb} {p': Path a cp' : Path: {V : Type ?u.2203} β [inst : Quiver V] β V β V β Sort (max(?u.2203+1)?u.2204)Path a: Va c: Vc}
{e: b βΆ de : b: Vb βΆ d: Vd} {e': c βΆ de' : c: Vc βΆ d: Vd} (h: cons p e = cons p' e'h : p: Path a bp.cons: {V : Type ?u.2246} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e: b βΆ de = p': Path a cp'.cons: {V : Type ?u.2271} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e': c βΆ de') : HEq: {Ξ± : Sort ?u.2289} β Ξ± β {Ξ² : Sort ?u.2289} β Ξ² β PropHEq e: b βΆ de e': c βΆ de' := byGoals accomplished! π V: Type uinstβ: Quiver Va, b, c, d: Vp: Path a bp': Path a ce: b βΆ de': c βΆ dh: cons p e = cons p' e'HEq e e'injection h: cons p e = cons p' e'hGoals accomplished! π
#align quiver.path.hom_heq_of_cons_eq_cons Quiver.Path.hom_heq_of_cons_eq_cons: β {V : Type u} [inst : Quiver V] {a b c d : V} {p : Path a b} {p' : Path a c} {e : b βΆ d} {e' : c βΆ d},
cons p e = cons p' e' β HEq e e'Quiver.Path.hom_heq_of_cons_eq_cons

/-- The length of a path is the number of arrows it uses. -/
def length: {a b : V} β Path a b β βlength {a: Va : V: Type uV} : β {b: Vb : V: Type uV}, Path: {V : Type ?u.2363} β [inst : Quiver V] β V β V β Sort (max(?u.2363+1)?u.2364)Path a: Va b: Vb β β: Typeβ
| _, nil: {V : Type ?u.2387} β [inst : Quiver V] β {a : V} β Path a anil => 0: ?m.24200
| _, cons: {V : Type ?u.2430} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons p: Path a bβp _ => p: Path a bβp.length: {a b : V} β Path a b β βlength + 1: ?m.25001
#align quiver.path.length Quiver.Path.length: {V : Type u} β [inst : Quiver V] β {a b : V} β Path a b β βQuiver.Path.length

instance: {V : Type u} β [inst : Quiver V] β {a : V} β Inhabited (Path a a)instance {a: Va : V: Type uV} : Inhabited: Sort ?u.3244 β Sort (max1?u.3244)Inhabited (Path: {V : Type ?u.3245} β [inst : Quiver V] β V β V β Sort (max(?u.3245+1)?u.3246)Path a: Va a: Va) :=
β¨nil: {V : Type ?u.3265} β [inst : Quiver V] β {a : V} β Path a anilβ©

@[simp]
theorem length_nil: β {a : V}, length nil = 0length_nil {a: Va : V: Type uV} : (nil: {V : Type ?u.3359} β [inst : Quiver V] β {a : V} β Path a anil : Path: {V : Type ?u.3346} β [inst : Quiver V] β V β V β Sort (max(?u.3346+1)?u.3347)Path a: Va a: Va).length: {V : Type ?u.3377} β [inst : Quiver V] β {a b : V} β Path a b β βlength = 0: ?m.33890 :=
rfl: β {Ξ± : Sort ?u.3415} {a : Ξ±}, a = arfl
#align quiver.path.length_nil Quiver.Path.length_nil: β {V : Type u} [inst : Quiver V] {a : V}, length nil = 0Quiver.Path.length_nil

@[simp]
theorem length_cons: β {V : Type u} [inst : Quiver V] (a b c : V) (p : Path a b) (e : b βΆ c), length (cons p e) = length p + 1length_cons (a: Va b: Vb c: Vc : V: Type uV) (p: Path a bp : Path: {V : Type ?u.3472} β [inst : Quiver V] β V β V β Sort (max(?u.3472+1)?u.3473)Path a: Va b: Vb) (e: b βΆ ce : b: Vb βΆ c: Vc) : (p: Path a bp.cons: {V : Type ?u.3502} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e: b βΆ ce).length: {V : Type ?u.3528} β [inst : Quiver V] β {a b : V} β Path a b β βlength = p: Path a bp.length: {V : Type ?u.3543} β [inst : Quiver V] β {a b : V} β Path a b β βlength + 1: ?m.35551 :=
rfl: β {Ξ± : Sort ?u.3620} {a : Ξ±}, a = arfl
#align quiver.path.length_cons Quiver.Path.length_cons: β {V : Type u} [inst : Quiver V] (a b c : V) (p : Path a b) (e : b βΆ c), length (cons p e) = length p + 1Quiver.Path.length_cons

theorem eq_of_length_zero: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b), length p = 0 β a = beq_of_length_zero (p: Path a bp : Path: {V : Type ?u.3687} β [inst : Quiver V] β V β V β Sort (max(?u.3687+1)?u.3688)Path a: Va b: Vb) (hzero: length p = 0hzero : p: Path a bp.length: {V : Type ?u.3704} β [inst : Quiver V] β {a b : V} β Path a b β βlength = 0: ?m.37220) : a: Va = b: Vb := byGoals accomplished! π
V: Type uinstβ: Quiver Va, b, c, d: Vp: Path a bhzero: length p = 0a = bcases p: Path a bpV: Type uinstβ: Quiver Va, c, d: Vhzero: length nil = 0nila = aV: Type uinstβ: Quiver Va, b, c, d, bβ: VaβΒΉ: Path a bβaβ: bβ βΆ bhzero: length (cons aβΒΉ aβ) = 0consa = b
V: Type uinstβ: Quiver Va, b, c, d: Vp: Path a bhzero: length p = 0a = bΒ·V: Type uinstβ: Quiver Va, c, d: Vhzero: length nil = 0nila = a V: Type uinstβ: Quiver Va, c, d: Vhzero: length nil = 0nila = aV: Type uinstβ: Quiver Va, b, c, d, bβ: VaβΒΉ: Path a bβaβ: bβ βΆ bhzero: length (cons aβΒΉ aβ) = 0consa = brflGoals accomplished! π
V: Type uinstβ: Quiver Va, b, c, d: Vp: Path a bhzero: length p = 0a = bΒ·V: Type uinstβ: Quiver Va, b, c, d, bβ: VaβΒΉ: Path a bβaβ: bβ βΆ bhzero: length (cons aβΒΉ aβ) = 0consa = b V: Type uinstβ: Quiver Va, b, c, d, bβ: VaβΒΉ: Path a bβaβ: bβ βΆ bhzero: length (cons aβΒΉ aβ) = 0consa = bcases Nat.succ_ne_zero: β (n : β), Nat.succ n β  0Nat.succ_ne_zero _: β_ hzero: length (cons aβΒΉ aβ) = 0hzeroGoals accomplished! π
#align quiver.path.eq_of_length_zero Quiver.Path.eq_of_length_zero: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b), length p = 0 β a = bQuiver.Path.eq_of_length_zero

/-- Composition of paths. -/
def comp: {a b c : V} β Path a b β Path b c β Path a ccomp {a: Va b: Vb : V: Type uV} : β {c: ?m.3997c}, Path: {V : Type ?u.4001} β [inst : Quiver V] β V β V β Sort (max(?u.4001+1)?u.4002)Path a: Va b: Vb β Path: {V : Type ?u.4016} β [inst : Quiver V] β V β V β Sort (max(?u.4016+1)?u.4017)Path b: Vb c: ?m.3997c β Path: {V : Type ?u.4029} β [inst : Quiver V] β V β V β Sort (max(?u.4029+1)?u.4030)Path a: Va c: ?m.3997c
| _, p: Path a bp, nil: {V : Type ?u.4055} β [inst : Quiver V] β {a : V} β Path a anil => p: Path a bp
| _, p: Path a bp, cons: {V : Type ?u.4096} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons q: Path b bβq e: bβ βΆ xβe => (p: Path a bp.comp: {a b c : V} β Path a b β Path b c β Path a ccomp q: Path b bβq).cons: {V : Type ?u.4174} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e: bβ βΆ xβe
#align quiver.path.comp Quiver.Path.comp: {V : Type u} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a cQuiver.Path.comp

@[simp]
theorem comp_cons: β {V : Type u} [inst : Quiver V] {a b c d : V} (p : Path a b) (q : Path b c) (e : c βΆ d),
comp p (cons q e) = cons (comp p q) ecomp_cons {a: Va b: Vb c: Vc d: Vd : V: Type uV} (p: Path a bp : Path: {V : Type ?u.4986} β [inst : Quiver V] β V β V β Sort (max(?u.4986+1)?u.4987)Path a: Va b: Vb) (q: Path b cq : Path: {V : Type ?u.5001} β [inst : Quiver V] β V β V β Sort (max(?u.5001+1)?u.5002)Path b: Vb c: Vc) (e: c βΆ de : c: Vc βΆ d: Vd) :
p: Path a bp.comp: {V : Type ?u.5031} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp (q: Path b cq.cons: {V : Type ?u.5049} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e: c βΆ de) = (p: Path a bp.comp: {V : Type ?u.5071} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp q: Path b cq).cons: {V : Type ?u.5085} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons e: c βΆ de :=
rfl: β {Ξ± : Sort ?u.5109} {a : Ξ±}, a = arfl
#align quiver.path.comp_cons Quiver.Path.comp_cons: β {V : Type u} [inst : Quiver V] {a b c d : V} (p : Path a b) (q : Path b c) (e : c βΆ d),
comp p (cons q e) = cons (comp p q) eQuiver.Path.comp_cons

@[simp]
theorem comp_nil: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b), comp p nil = pcomp_nil {a: Va b: Vb : V: Type uV} (p: Path a bp : Path: {V : Type ?u.5190} β [inst : Quiver V] β V β V β Sort (max(?u.5190+1)?u.5191)Path a: Va b: Vb) : p: Path a bp.comp: {V : Type ?u.5207} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp Path.nil: {V : Type ?u.5225} β [inst : Quiver V] β {a : V} β Path a aPath.nil = p: Path a bp :=
rfl: β {Ξ± : Sort ?u.5243} {a : Ξ±}, a = arfl
#align quiver.path.comp_nil Quiver.Path.comp_nil: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b), comp p nil = pQuiver.Path.comp_nil

@[simp]
theorem nil_comp: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b), comp nil p = pnil_comp {a: Va : V: Type uV} : β {b: ?m.5307b} (p: Path a bp : Path: {V : Type ?u.5310} β [inst : Quiver V] β V β V β Sort (max(?u.5310+1)?u.5311)Path a: Va b: ?m.5307b), Path.nil: {V : Type ?u.5326} β [inst : Quiver V] β {a : V} β Path a aPath.nil.comp: {V : Type ?u.5337} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp p: Path a bp = p: Path a bp
| _, nil: {V : Type ?u.5377} β [inst : Quiver V] β {a : V} β Path a anil => rfl: β {Ξ± : Sort ?u.5414} {a : Ξ±}, a = arfl
| _, cons: {V : Type ?u.5435} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons p: Path a bβp _ => byGoals accomplished! π V: Type uinstβ: Quiver VaβΒΉ, b, c, d, a, xβ, bβ: Vp: Path a bβaβ: bβ βΆ xβcomp nil (cons p aβ) = cons p aβrw [V: Type uinstβ: Quiver VaβΒΉ, b, c, d, a, xβ, bβ: Vp: Path a bβaβ: bβ βΆ xβcomp nil (cons p aβ) = cons p aβcomp_cons: β {V : Type ?u.5739} [inst : Quiver V] {a b c d : V} (p : Path a b) (q : Path b c) (e : c βΆ d),
comp p (cons q e) = cons (comp p q) ecomp_cons,V: Type uinstβ: Quiver VaβΒΉ, b, c, d, a, xβ, bβ: Vp: Path a bβaβ: bβ βΆ xβcons (comp nil p) aβ = cons p aβ V: Type uinstβ: Quiver VaβΒΉ, b, c, d, a, xβ, bβ: Vp: Path a bβaβ: bβ βΆ xβcomp nil (cons p aβ) = cons p aβnil_comp: β {a b : V} (p : Path a b), comp nil p = pnil_comp p: Path a bβpV: Type uinstβ: Quiver VaβΒΉ, b, c, d, a, xβ, bβ: Vp: Path a bβaβ: bβ βΆ xβcons p aβ = cons p aβ]Goals accomplished! π
#align quiver.path.nil_comp Quiver.Path.nil_comp: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b), comp nil p = pQuiver.Path.nil_comp

@[simp]
theorem comp_assoc: β {V : Type u} [inst : Quiver V] {a b c d : V} (p : Path a b) (q : Path b c) (r : Path c d),
comp (comp p q) r = comp p (comp q r)comp_assoc {a: Va b: Vb c: Vc : V: Type uV} :
β {d: ?m.5922d} (p: Path a bp : Path: {V : Type ?u.5925} β [inst : Quiver V] β V β V β Sort (max(?u.5925+1)?u.5926)Path a: Va b: Vb) (q: Path b cq : Path: {V : Type ?u.5940} β [inst : Quiver V] β V β V β Sort (max(?u.5940+1)?u.5941)Path b: Vb c: Vc) (r: Path c dr : Path: {V : Type ?u.5954} β [inst : Quiver V] β V β V β Sort (max(?u.5954+1)?u.5955)Path c: Vc d: ?m.5922d), (p: Path a bp.comp: {V : Type ?u.5970} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp q: Path b cq).comp: {V : Type ?u.5991} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp r: Path c dr = p: Path a bp.comp: {V : Type ?u.6006} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp (q: Path b cq.comp: {V : Type ?u.6021} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp r: Path c dr)
| _, _, _, nil: {V : Type ?u.6054} β [inst : Quiver V] β {a : V} β Path a anil => rfl: β {Ξ± : Sort ?u.6105} {a : Ξ±}, a = arfl
| _, p: Path a bp, q: Path b cq, cons: {V : Type ?u.6153} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons r: Path c bβr _ => byGoals accomplished! π V: Type uinstβ: Quiver VaβΒΉ, bβΒΉ, cβ, d, a, b, c, xβ: Vp: Path a bq: Path b cbβ: Vr: Path c bβaβ: bβ βΆ xβcomp (comp p q) (cons r aβ) = comp p (comp q (cons r aβ))rw [V: Type uinstβ: Quiver VaβΒΉ, bβΒΉ, cβ, d, a, b, c, xβ: Vp: Path a bq: Path b cbβ: Vr: Path c bβaβ: bβ βΆ xβcomp (comp p q) (cons r aβ) = comp p (comp q (cons r aβ))comp_cons: β {V : Type ?u.6523} [inst : Quiver V] {a b c d : V} (p : Path a b) (q : Path b c) (e : c βΆ d),
comp p (cons q e) = cons (comp p q) ecomp_cons,V: Type uinstβ: Quiver VaβΒΉ, bβΒΉ, cβ, d, a, b, c, xβ: Vp: Path a bq: Path b cbβ: Vr: Path c bβaβ: bβ βΆ xβcons (comp (comp p q) r) aβ = comp p (comp q (cons r aβ)) V: Type uinstβ: Quiver VaβΒΉ, bβΒΉ, cβ, d, a, b, c, xβ: Vp: Path a bq: Path b cbβ: Vr: Path c bβaβ: bβ βΆ xβcomp (comp p q) (cons r aβ) = comp p (comp q (cons r aβ))comp_cons: β {V : Type ?u.6573} [inst : Quiver V] {a b c d : V} (p : Path a b) (q : Path b c) (e : c βΆ d),
comp p (cons q e) = cons (comp p q) ecomp_cons,V: Type uinstβ: Quiver VaβΒΉ, bβΒΉ, cβ, d, a, b, c, xβ: Vp: Path a bq: Path b cbβ: Vr: Path c bβaβ: bβ βΆ xβcons (comp (comp p q) r) aβ = comp p (cons (comp q r) aβ) V: Type uinstβ: Quiver VaβΒΉ, bβΒΉ, cβ, d, a, b, c, xβ: Vp: Path a bq: Path b cbβ: Vr: Path c bβaβ: bβ βΆ xβcomp (comp p q) (cons r aβ) = comp p (comp q (cons r aβ))comp_cons: β {V : Type ?u.6600} [inst : Quiver V] {a b c d : V} (p : Path a b) (q : Path b c) (e : c βΆ d),
comp p (cons q e) = cons (comp p q) ecomp_cons,V: Type uinstβ: Quiver VaβΒΉ, bβΒΉ, cβ, d, a, b, c, xβ: Vp: Path a bq: Path b cbβ: Vr: Path c bβaβ: bβ βΆ xβcons (comp (comp p q) r) aβ = cons (comp p (comp q r)) aβ V: Type uinstβ: Quiver VaβΒΉ, bβΒΉ, cβ, d, a, b, c, xβ: Vp: Path a bq: Path b cbβ: Vr: Path c bβaβ: bβ βΆ xβcomp (comp p q) (cons r aβ) = comp p (comp q (cons r aβ))comp_assoc: β {a b c d : V} (p : Path a b) (q : Path b c) (r : Path c d), comp (comp p q) r = comp p (comp q r)comp_assoc p: Path a bp q: Path b cq r: Path c bβrV: Type uinstβ: Quiver VaβΒΉ, bβΒΉ, cβ, d, a, b, c, xβ: Vp: Path a bq: Path b cbβ: Vr: Path c bβaβ: bβ βΆ xβcons (comp p (comp q r)) aβ = cons (comp p (comp q r)) aβ]Goals accomplished! π
#align quiver.path.comp_assoc Quiver.Path.comp_assoc: β {V : Type u} [inst : Quiver V] {a b c d : V} (p : Path a b) (q : Path b c) (r : Path c d),
comp (comp p q) r = comp p (comp q r)Quiver.Path.comp_assoc

@[simp]
theorem length_comp: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b) {c : V} (q : Path b c),
length (comp p q) = length p + length qlength_comp (p: Path a bp : Path: {V : Type ?u.6971} β [inst : Quiver V] β V β V β Sort (max(?u.6971+1)?u.6972)Path a: Va b: Vb) : β {c: ?m.6987c} (q: Path b cq : Path: {V : Type ?u.6990} β [inst : Quiver V] β V β V β Sort (max(?u.6990+1)?u.6991)Path b: Vb c: ?m.6987c), (p: Path a bp.comp: {V : Type ?u.7006} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp q: Path b cq).length: {V : Type ?u.7027} β [inst : Quiver V] β {a b : V} β Path a b β βlength = p: Path a bp.length: {V : Type ?u.7042} β [inst : Quiver V] β {a b : V} β Path a b β βlength + q: Path b cq.length: {V : Type ?u.7054} β [inst : Quiver V] β {a b : V} β Path a b β βlength
| _, nil: {V : Type ?u.7111} β [inst : Quiver V] β {a : V} β Path a anil => rfl: β {Ξ± : Sort ?u.7148} {a : Ξ±}, a = arfl
| _, cons: {V : Type ?u.7224} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons _ _ => congr_arg: β {Ξ± : Sort ?u.7285} {Ξ² : Sort ?u.7284} {aβ aβ : Ξ±} (f : Ξ± β Ξ²), aβ = aβ β f aβ = f aβcongr_arg Nat.succ: β β βNat.succ (length_comp: β (p : Path a b) {c : V} (q : Path b c), length (comp p q) = length p + length qlength_comp _: Path a b_ _: Path b ?m.7315_)
#align quiver.path.length_comp Quiver.Path.length_comp: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b) {c : V} (q : Path b c),
length (comp p q) = length p + length qQuiver.Path.length_comp

theorem comp_inj: β {pβ pβ : Path a b} {qβ qβ : Path b c}, length qβ = length qβ β (comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβ)comp_inj {pβ: Path a bpβ pβ: Path a bpβ : Path: {V : Type ?u.7718} β [inst : Quiver V] β V β V β Sort (max(?u.7718+1)?u.7719)Path a: Va b: Vb} {qβ: Path b cqβ qβ: Path b cqβ : Path: {V : Type ?u.7761} β [inst : Quiver V] β V β V β Sort (max(?u.7761+1)?u.7762)Path b: Vb c: Vc} (hq: length qβ = length qβhq : qβ: Path b cqβ.length: {V : Type ?u.7777} β [inst : Quiver V] β {a b : V} β Path a b β βlength = qβ: Path b cqβ.length: {V : Type ?u.7795} β [inst : Quiver V] β {a b : V} β Path a b β βlength) :
pβ: Path a bpβ.comp: {V : Type ?u.7811} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp qβ: Path b cqβ = pβ: Path a bpβ.comp: {V : Type ?u.7826} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp qβ: Path b cqβ β pβ: Path a bpβ = pβ: Path a bpβ β§ qβ: Path b cqβ = qβ: Path b cqβ := byGoals accomplished! π
V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβcomp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβrefine' β¨fun h: ?m.7862h => _: ?m.7858_, V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβcomp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβbyGoals accomplished! π V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβpβ = pβ β§ qβ = qβ β comp pβ qβ = comp pβ qβrintro β¨rfl, rflβ©: pβ = pβ β§ qβ = qββ¨rfl: pβ = pβrflβ¨rfl, rflβ©: pβ = pβ β§ qβ = qβ, rfl: qβ = qβrflβ¨rfl, rflβ©: pβ = pβ β§ qβ = qββ©V: Type uinstβ: Quiver Va, b, c, d: Vpβ: Path a bqβ: Path b chq: length qβ = length qβintrocomp pβ qβ = comp pβ qβ;V: Type uinstβ: Quiver Va, b, c, d: Vpβ: Path a bqβ: Path b chq: length qβ = length qβintrocomp pβ qβ = comp pβ qβ V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβpβ = pβ β§ qβ = qβ β comp pβ qβ = comp pβ qβrflGoals accomplished! πβ©V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβh: comp pβ qβ = comp pβ qβpβ = pβ β§ qβ = qβ
V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβcomp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβinduction' qβ: Path b cqβ with dβ: ?m.7954dβ eβ: ?m.7954eβ qβ: Path ?m.7956 dβqβ fβ: dβ βΆ eβfβ ih: ?m.7957 dβ qβihV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qββ: Path b chqβ: length qβ = length qββhβ: comp pβ qβ = comp pβ qββqβ: Path b bhq: length nil = length qβh: comp pβ nil = comp pβ qβnilpβ = pβ β§ nil = qβV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβqβ: Path b eβhq: length (cons qβ fβ) = length qβh: comp pβ (cons qβ fβ) = comp pβ qβconspβ = pβ β§ cons qβ fβ = qβ V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβh: comp pβ qβ = comp pβ qβpβ = pβ β§ qβ = qβ<;>V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qββ: Path b chqβ: length qβ = length qββhβ: comp pβ qβ = comp pβ qββqβ: Path b bhq: length nil = length qβh: comp pβ nil = comp pβ qβnilpβ = pβ β§ nil = qβV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβqβ: Path b eβhq: length (cons qβ fβ) = length qβh: comp pβ (cons qβ fβ) = comp pβ qβconspβ = pβ β§ cons qβ fβ = qβ V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβh: comp pβ qβ = comp pβ qβpβ = pβ β§ qβ = qβobtain _ | β¨qβ, fββ©: Path b b_ | β¨qβ: Path b bβqβ_ | β¨qβ, fββ©: Path b b, fβ: bβ βΆ bfβ_ | β¨qβ, fββ©: Path b bβ© := qβ: Path b eβqβV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chqβ: length qβ = length qβhβ: comp pβ qβ = comp pβ qβhq: length nil = length nilh: comp pβ nil = comp pβ nilnil.nilpβ = pβ β§ nil = nilV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qββ: Path b chqβ: length qβ = length qββhβ: comp pβ qβ = comp pβ qββbβ: Vqβ: Path b bβfβ: bβ βΆ bhq: length nil = length (cons qβ fβ)h: comp pβ nil = comp pβ (cons qβ fβ)nil.conspβ = pβ β§ nil = cons qβ fβ
V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβcomp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβΒ·V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chqβ: length qβ = length qβhβ: comp pβ qβ = comp pβ qβhq: length nil = length nilh: comp pβ nil = comp pβ nilnil.nilpβ = pβ β§ nil = nil V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chqβ: length qβ = length qβhβ: comp pβ qβ = comp pβ qβhq: length nil = length nilh: comp pβ nil = comp pβ nilnil.nilpβ = pβ β§ nil = nilV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qββ: Path b chqβ: length qβ = length qββhβ: comp pβ qβ = comp pβ qββbβ: Vqβ: Path b bβfβ: bβ βΆ bhq: length nil = length (cons qβ fβ)h: comp pβ nil = comp pβ (cons qβ fβ)nil.conspβ = pβ β§ nil = cons qβ fβV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qβ: Path b chqβ: length qββ = length qβhβ: comp pβ qββ = comp pβ qβdβ: Vqβ: Path b dβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβfβ: dβ βΆ bhq: length (cons qβ fβ) = length nilh: comp pβ (cons qβ fβ) = comp pβ nilcons.nilpβ = pβ β§ cons qβ fβ = nilV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβbβ: Vqβ: Path b bβfβ: bβ βΆ eβhq: length (cons qβ fβ) = length (cons qβ fβ)h: comp pβ (cons qβ fβ) = comp pβ (cons qβ fβ)cons.conspβ = pβ β§ cons qβ fβ = cons qβ fβexact β¨h: comp pβ nil = comp pβ nilh, rfl: β {Ξ± : Sort ?u.8278} {a : Ξ±}, a = arflβ©Goals accomplished! π
V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβcomp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβΒ·V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qββ: Path b chqβ: length qβ = length qββhβ: comp pβ qβ = comp pβ qββbβ: Vqβ: Path b bβfβ: bβ βΆ bhq: length nil = length (cons qβ fβ)h: comp pβ nil = comp pβ (cons qβ fβ)nil.conspβ = pβ β§ nil = cons qβ fβ V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qββ: Path b chqβ: length qβ = length qββhβ: comp pβ qβ = comp pβ qββbβ: Vqβ: Path b bβfβ: bβ βΆ bhq: length nil = length (cons qβ fβ)h: comp pβ nil = comp pβ (cons qβ fβ)nil.conspβ = pβ β§ nil = cons qβ fβV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qβ: Path b chqβ: length qββ = length qβhβ: comp pβ qββ = comp pβ qβdβ: Vqβ: Path b dβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβfβ: dβ βΆ bhq: length (cons qβ fβ) = length nilh: comp pβ (cons qβ fβ) = comp pβ nilcons.nilpβ = pβ β§ cons qβ fβ = nilV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβbβ: Vqβ: Path b bβfβ: bβ βΆ eβhq: length (cons qβ fβ) = length (cons qβ fβ)h: comp pβ (cons qβ fβ) = comp pβ (cons qβ fβ)cons.conspβ = pβ β§ cons qβ fβ = cons qβ fβcases hq: length nil = length (cons qβ fβ)hqGoals accomplished! π
V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβcomp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβΒ·V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qβ: Path b chqβ: length qββ = length qβhβ: comp pβ qββ = comp pβ qβdβ: Vqβ: Path b dβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβfβ: dβ βΆ bhq: length (cons qβ fβ) = length nilh: comp pβ (cons qβ fβ) = comp pβ nilcons.nilpβ = pβ β§ cons qβ fβ = nil V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qβ: Path b chqβ: length qββ = length qβhβ: comp pβ qββ = comp pβ qβdβ: Vqβ: Path b dβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβfβ: dβ βΆ bhq: length (cons qβ fβ) = length nilh: comp pβ (cons qβ fβ) = comp pβ nilcons.nilpβ = pβ β§ cons qβ fβ = nilV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβbβ: Vqβ: Path b bβfβ: bβ βΆ eβhq: length (cons qβ fβ) = length (cons qβ fβ)h: comp pβ (cons qβ fβ) = comp pβ (cons qβ fβ)cons.conspβ = pβ β§ cons qβ fβ = cons qβ fβcases hq: length (cons qβ fβ) = length nilhqGoals accomplished! π
V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b chq: length qβ = length qβcomp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβΒ·V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβbβ: Vqβ: Path b bβfβ: bβ βΆ eβhq: length (cons qβ fβ) = length (cons qβ fβ)h: comp pβ (cons qβ fβ) = comp pβ (cons qβ fβ)cons.conspβ = pβ β§ cons qβ fβ = cons qβ fβ V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβbβ: Vqβ: Path b bβfβ: bβ βΆ eβhq: length (cons qβ fβ) = length (cons qβ fβ)h: comp pβ (cons qβ fβ) = comp pβ (cons qβ fβ)cons.conspβ = pβ β§ cons qβ fβ = cons qβ fβsimp only [comp_cons: β {V : Type ?u.8436} [inst : Quiver V] {a b c d : V} (p : Path a b) (q : Path b c) (e : c βΆ d),
comp p (cons q e) = cons (comp p q) ecomp_cons, cons.injEq: β {V : Type ?u.8471} [inst : Quiver V] {a b c : V} (a_1 : Path a b) (a_2 : b βΆ c) (b_1 : V) (a_3 : Path a b_1)
(a_4 : b_1 βΆ c), (cons a_1 a_2 = cons a_3 a_4) = (b = b_1 β§ HEq a_1 a_3 β§ HEq a_2 a_4)cons.injEq] at h: comp pβ (cons qβ fβ) = comp pβ (cons qβ fβ)hV: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβbβ: Vqβ: Path b bβfβ: bβ βΆ eβhq: length (cons qβ fβ) = length (cons qβ fβ)h: dβ = bβ β§ HEq (comp pβ qβ) (comp pβ qβ) β§ HEq fβ fβcons.conspβ = pβ β§ cons qβ fβ = cons qβ fβ
V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβbβ: Vqβ: Path b bβfβ: bβ βΆ eβhq: length (cons qβ fβ) = length (cons qβ fβ)h: comp pβ (cons qβ fβ) = comp pβ (cons qβ fβ)cons.conspβ = pβ β§ cons qβ fβ = cons qβ fβobtain rfl: dβ = bβrfl := h: dβ = bβ β§ HEq (comp pβ qβ) (comp pβ qβ) β§ HEq fβ fβh.1: β {a b : Prop}, a β§ b β a1V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβqβ: Path b dβfβ: dβ βΆ eβhq: length (cons qβ fβ) = length (cons qβ fβ)h: dβ = dβ β§ HEq (comp pβ qβ) (comp pβ qβ) β§ HEq fβ fβcons.conspβ = pβ β§ cons qβ fβ = cons qβ fβ
V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβbβ: Vqβ: Path b bβfβ: bβ βΆ eβhq: length (cons qβ fβ) = length (cons qβ fβ)h: comp pβ (cons qβ fβ) = comp pβ (cons qβ fβ)cons.conspβ = pβ β§ cons qβ fβ = cons qβ fβobtain β¨rfl, rflβ©: pβ = pβ β§ qβ = qββ¨rfl: pβ = pβrflβ¨rfl, rflβ©: pβ = pβ β§ qβ = qβ, rfl: qβ = qβrflβ¨rfl, rflβ©: pβ = pβ β§ qβ = qββ© := ih: ?m.7957 dβ qβih (Nat.succ.inj: β {n n_1 : β}, Nat.succ n = Nat.succ n_1 β n = n_1Nat.succ.inj hq: length (cons qβ fβ) = length (cons qβ fβ)hq) h: dβ = dβ β§ HEq (comp pβ qβ) (comp pβ qβ) β§ HEq fβ fβh.2: β {a b : Prop}, a β§ b β b2.1: β {a b : Prop}, a β§ b β a1.eq: β {Ξ± : Sort ?u.8713} {a b : Ξ±}, HEq a b β a = beqV: Type uinstβ: Quiver Va, b, c, d: Vpβ: Path a bqββ, qβ: Path b chqβ: length qββ = length qβdβ, eβ: Vqβ: Path b dβfβ, fβ: dβ βΆ eβhβ: comp pβ qββ = comp pβ qβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβhq: length (cons qβ fβ) = length (cons qβ fβ)h: dβ = dβ β§ HEq (comp pβ qβ) (comp pβ qβ) β§ HEq fβ fβcons.cons.intropβ = pβ β§ cons qβ fβ = cons qβ fβ
V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβbβ: Vqβ: Path b bβfβ: bβ βΆ eβhq: length (cons qβ fβ) = length (cons qβ fβ)h: comp pβ (cons qβ fβ) = comp pβ (cons qβ fβ)cons.conspβ = pβ β§ cons qβ fβ = cons qβ fβrw [V: Type uinstβ: Quiver Va, b, c, d: Vpβ: Path a bqββ, qβ: Path b chqβ: length qββ = length qβdβ, eβ: Vqβ: Path b dβfβ, fβ: dβ βΆ eβhβ: comp pβ qββ = comp pβ qβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβhq: length (cons qβ fβ) = length (cons qβ fβ)h: dβ = dβ β§ HEq (comp pβ qβ) (comp pβ qβ) β§ HEq fβ fβcons.cons.intropβ = pβ β§ cons qβ fβ = cons qβ fβh: dβ = dβ β§ HEq (comp pβ qβ) (comp pβ qβ) β§ HEq fβ fβh.2: β {a b : Prop}, a β§ b β b2.2: β {a b : Prop}, a β§ b β b2.eq: β {Ξ± : Sort ?u.8787} {a b : Ξ±}, HEq a b β a = beqV: Type uinstβ: Quiver Va, b, c, d: Vpβ: Path a bqββ, qβ: Path b chqβ: length qββ = length qβdβ, eβ: Vqβ: Path b dβfβ, fβ: dβ βΆ eβhβ: comp pβ qββ = comp pβ qβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβhq: length (cons qβ fβ) = length (cons qβ fβ)h: dβ = dβ β§ HEq (comp pβ qβ) (comp pβ qβ) β§ HEq fβ fβcons.cons.intropβ = pβ β§ cons qβ fβ = cons qβ fβ]V: Type uinstβ: Quiver Va, b, c, d: Vpβ: Path a bqββ, qβ: Path b chqβ: length qββ = length qβdβ, eβ: Vqβ: Path b dβfβ, fβ: dβ βΆ eβhβ: comp pβ qββ = comp pβ qβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβhq: length (cons qβ fβ) = length (cons qβ fβ)h: dβ = dβ β§ HEq (comp pβ qβ) (comp pβ qβ) β§ HEq fβ fβcons.cons.intropβ = pβ β§ cons qβ fβ = cons qβ fβ
V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqββ, qββ: Path b chqβ: length qββ = length qββhβ: comp pβ qββ = comp pβ qββdβ, eβ: Vqβ: Path b dβfβ: dβ βΆ eβih: β {qβ : Path b dβ}, length qβ = length qβ β comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβbβ: Vqβ: Path b bβfβ: bβ βΆ eβhq: length (cons qβ fβ) = length (cons qβ fβ)h: comp pβ (cons qβ fβ) = comp pβ (cons qβ fβ)cons.conspβ = pβ β§ cons qβ fβ = cons qβ fβexact β¨rfl: β {Ξ± : Sort ?u.8812} {a : Ξ±}, a = arfl, rfl: β {Ξ± : Sort ?u.8815} {a : Ξ±}, a = arflβ©Goals accomplished! π
#align quiver.path.comp_inj Quiver.Path.comp_inj: β {V : Type u} [inst : Quiver V] {a b c : V} {pβ pβ : Path a b} {qβ qβ : Path b c},
length qβ = length qβ β (comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβ)Quiver.Path.comp_inj

theorem comp_inj': β {pβ pβ : Path a b} {qβ qβ : Path b c}, length pβ = length pβ β (comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβ)comp_inj' {pβ: Path a bpβ pβ: Path a bpβ : Path: {V : Type ?u.8988} β [inst : Quiver V] β V β V β Sort (max(?u.8988+1)?u.8989)Path a: Va b: Vb} {qβ: Path b cqβ qβ: Path b cqβ : Path: {V : Type ?u.9016} β [inst : Quiver V] β V β V β Sort (max(?u.9016+1)?u.9017)Path b: Vb c: Vc} (h: length pβ = length pβh : pβ: Path a bpβ.length: {V : Type ?u.9032} β [inst : Quiver V] β {a b : V} β Path a b β βlength = pβ: Path a bpβ.length: {V : Type ?u.9050} β [inst : Quiver V] β {a b : V} β Path a b β βlength) :
pβ: Path a bpβ.comp: {V : Type ?u.9066} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp qβ: Path b cqβ = pβ: Path a bpβ.comp: {V : Type ?u.9081} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp qβ: Path b cqβ β pβ: Path a bpβ = pβ: Path a bpβ β§ qβ: Path b cqβ = qβ: Path b cqβ :=
β¨fun h_eq: ?m.9115h_eq => (comp_inj: β {V : Type ?u.9117} [inst : Quiver V] {a b c : V} {pβ pβ : Path a b} {qβ qβ : Path b c},
length qβ = length qβ β (comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβ)comp_inj <| Nat.add_left_cancel: β {n m k : β}, n + m = n + k β m = kNat.add_left_cancel <| byGoals accomplished! π V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b ch: length pβ = length pβh_eq: comp pβ qβ = comp pβ qβ?m.9161 h h_eq + length qβ = ?m.9161 h h_eq + length qβsimpa [h: length pβ = length pβh] using congr_arg: β {Ξ± : Sort ?u.9525} {Ξ² : Sort ?u.9524} {aβ aβ : Ξ±} (f : Ξ± β Ξ²), aβ = aβ β f aβ = f aβcongr_arg length: {V : Type ?u.9531} β [inst : Quiver V] β {a b : V} β Path a b β βlength h_eq: comp pβ qβ = comp pβ qβh_eqGoals accomplished! π).1: β {a b : Prop}, (a β b) β a β b1 h_eq: ?m.9115h_eq,
byGoals accomplished! π V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b ch: length pβ = length pβpβ = pβ β§ qβ = qβ β comp pβ qβ = comp pβ qβrintro β¨rfl, rflβ©: pβ = pβ β§ qβ = qββ¨rfl: pβ = pβrflβ¨rfl, rflβ©: pβ = pβ β§ qβ = qβ, rfl: qβ = qβrflβ¨rfl, rflβ©: pβ = pβ β§ qβ = qββ©V: Type uinstβ: Quiver Va, b, c, d: Vpβ: Path a bqβ: Path b ch: length pβ = length pβintrocomp pβ qβ = comp pβ qβ;V: Type uinstβ: Quiver Va, b, c, d: Vpβ: Path a bqβ: Path b ch: length pβ = length pβintrocomp pβ qβ = comp pβ qβ V: Type uinstβ: Quiver Va, b, c, d: Vpβ, pβ: Path a bqβ, qβ: Path b ch: length pβ = length pβpβ = pβ β§ qβ = qβ β comp pβ qβ = comp pβ qβrflGoals accomplished! πβ©
#align quiver.path.comp_inj' Quiver.Path.comp_inj': β {V : Type u} [inst : Quiver V] {a b c : V} {pβ pβ : Path a b} {qβ qβ : Path b c},
length pβ = length pβ β (comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβ)Quiver.Path.comp_inj'

theorem comp_injective_left: β (q : Path b c), Injective fun p => comp p qcomp_injective_left (q: Path b cq : Path: {V : Type ?u.9798} β [inst : Quiver V] β V β V β Sort (max(?u.9798+1)?u.9799)Path b: Vb c: Vc) : Injective: {Ξ± : Sort ?u.9814} β {Ξ² : Sort ?u.9813} β (Ξ± β Ξ²) β PropInjective fun p: Path a bp : Path: {V : Type ?u.9818} β [inst : Quiver V] β V β V β Sort (max(?u.9818+1)?u.9819)Path a: Va b: Vb => p: Path a bp.comp: {V : Type ?u.9832} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp q: Path b cq :=
fun _: ?m.9859_ _: ?m.9862_ h: ?m.9865h => ((comp_inj: β {V : Type ?u.9867} [inst : Quiver V] {a b c : V} {pβ pβ : Path a b} {qβ qβ : Path b c},
length qβ = length qβ β (comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβ)comp_inj rfl: β {Ξ± : Sort ?u.9878} {a : Ξ±}, a = arfl).1: β {a b : Prop}, (a β b) β a β b1 h: ?m.9865h).1: β {a b : Prop}, a β§ b β a1
#align quiver.path.comp_injective_left Quiver.Path.comp_injective_left: β {V : Type u} [inst : Quiver V] {a b c : V} (q : Path b c), Injective fun p => comp p qQuiver.Path.comp_injective_left

theorem comp_injective_right: β (p : Path a b), Injective (comp p)comp_injective_right (p: Path a bp : Path: {V : Type ?u.9958} β [inst : Quiver V] β V β V β Sort (max(?u.9958+1)?u.9959)Path a: Va b: Vb) : Injective: {Ξ± : Sort ?u.9974} β {Ξ² : Sort ?u.9973} β (Ξ± β Ξ²) β PropInjective (p: Path a bp.comp: {V : Type ?u.10005} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp : Path: {V : Type ?u.9979} β [inst : Quiver V] β V β V β Sort (max(?u.9979+1)?u.9980)Path b: Vb c: Vc β Path: {V : Type ?u.9992} β [inst : Quiver V] β V β V β Sort (max(?u.9992+1)?u.9993)Path a: Va c: Vc) :=
fun _: ?m.10033_ _: ?m.10036_ h: ?m.10039h => ((comp_inj': β {V : Type ?u.10041} [inst : Quiver V] {a b c : V} {pβ pβ : Path a b} {qβ qβ : Path b c},
length pβ = length pβ β (comp pβ qβ = comp pβ qβ β pβ = pβ β§ qβ = qβ)comp_inj' rfl: β {Ξ± : Sort ?u.10052} {a : Ξ±}, a = arfl).1: β {a b : Prop}, (a β b) β a β b1 h: ?m.10039h).2: β {a b : Prop}, a β§ b β b2
#align quiver.path.comp_injective_right Quiver.Path.comp_injective_right: β {V : Type u} [inst : Quiver V] {a b c : V} (p : Path a b), Injective (comp p)Quiver.Path.comp_injective_right

@[simp]
theorem comp_inj_left: β {pβ pβ : Path a b} {q : Path b c}, comp pβ q = comp pβ q β pβ = pβcomp_inj_left {pβ: Path a bpβ pβ: Path a bpβ : Path: {V : Type ?u.10143} β [inst : Quiver V] β V β V β Sort (max(?u.10143+1)?u.10144)Path a: Va b: Vb} {q: Path b cq : Path: {V : Type ?u.10157} β [inst : Quiver V] β V β V β Sort (max(?u.10157+1)?u.10158)Path b: Vb c: Vc} : pβ: Path a bpβ.comp: {V : Type ?u.10173} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp q: Path b cq = pβ: Path a bpβ.comp: {V : Type ?u.10194} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp q: Path b cq β pβ: Path a bpβ = pβ: Path a bpβ :=
q: Path b cq.comp_injective_left: β {V : Type ?u.10215} [inst : Quiver V] {a b c : V} (q : Path b c), Injective fun p => comp p qcomp_injective_left.eq_iff: β {Ξ± : Sort ?u.10230} {Ξ² : Sort ?u.10231} {f : Ξ± β Ξ²}, Injective f β β {a b : Ξ±}, f a = f b β a = beq_iff
#align quiver.path.comp_inj_left Quiver.Path.comp_inj_left: β {V : Type u} [inst : Quiver V] {a b c : V} {pβ pβ : Path a b} {q : Path b c}, comp pβ q = comp pβ q β pβ = pβQuiver.Path.comp_inj_left

@[simp]
theorem comp_inj_right: β {V : Type u} [inst : Quiver V] {a b c : V} {p : Path a b} {qβ qβ : Path b c}, comp p qβ = comp p qβ β qβ = qβcomp_inj_right {p: Path a bp : Path: {V : Type ?u.10327} β [inst : Quiver V] β V β V β Sort (max(?u.10327+1)?u.10328)Path a: Va b: Vb} {qβ: Path b cqβ qβ: Path b cqβ : Path: {V : Type ?u.10342} β [inst : Quiver V] β V β V β Sort (max(?u.10342+1)?u.10343)Path b: Vb c: Vc} : p: Path a bp.comp: {V : Type ?u.10372} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp qβ: Path b cqβ = p: Path a bp.comp: {V : Type ?u.10393} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp qβ: Path b cqβ β qβ: Path b cqβ = qβ: Path b cqβ :=
p: Path a bp.comp_injective_right: β {V : Type ?u.10414} [inst : Quiver V] {a b c : V} (p : Path a b), Injective (comp p)comp_injective_right.eq_iff: β {Ξ± : Sort ?u.10429} {Ξ² : Sort ?u.10430} {f : Ξ± β Ξ²}, Injective f β β {a b : Ξ±}, f a = f b β a = beq_iff
#align quiver.path.comp_inj_right Quiver.Path.comp_inj_right: β {V : Type u} [inst : Quiver V] {a b c : V} {p : Path a b} {qβ qβ : Path b c}, comp p qβ = comp p qβ β qβ = qβQuiver.Path.comp_inj_right

/-- Turn a path into a list. The list contains `a` at its head, but not `b` a priori. -/
@[simp]
def toList: {V : Type u} β [inst : Quiver V] β {a b : V} β Path a b β List VtoList : β {b: Vb : V: Type uV}, Path: {V : Type ?u.10528} β [inst : Quiver V] β V β V β Sort (max(?u.10528+1)?u.10529)Path a: Va b: Vb β List: Type ?u.10542 β Type ?u.10542List V: Type uV
| _, nil: {V : Type ?u.10552} β [inst : Quiver V] β {a : V} β Path a anil => []: List ?m.10585[]
| _, @cons: {V : Type ?u.10587} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons _: Type u_ _ _: V_ c: Vc _ p: Path a cp _ => c: Vc :: p: Path a cp.toList: {b : V} β Path a b β List VtoList
#align quiver.path.to_list Quiver.Path.toList: {V : Type u} β [inst : Quiver V] β {a b : V} β Path a b β List VQuiver.Path.toList

/-- `Quiver.Path.toList` is a contravariant functor. The inversion comes from `Quiver.Path` and
`List` having different preferred directions for adding elements. -/
@[simp]
theorem toList_comp: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b) {c : V} (q : Path b c),
toList (comp p q) = toList q ++ toList ptoList_comp (p: Path a bp : Path: {V : Type ?u.11912} β [inst : Quiver V] β V β V β Sort (max(?u.11912+1)?u.11913)Path a: Va b: Vb) : β {c: ?m.11928c} (q: Path b cq : Path: {V : Type ?u.11931} β [inst : Quiver V] β V β V β Sort (max(?u.11931+1)?u.11932)Path b: Vb c: ?m.11928c), (p: Path a bp.comp: {V : Type ?u.11947} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp q: Path b cq).toList: {V : Type ?u.11968} β [inst : Quiver V] β {a b : V} β Path a b β List VtoList = q: Path b cq.toList: {V : Type ?u.11983} β [inst : Quiver V] β {a b : V} β Path a b β List VtoList ++ p: Path a bp.toList: {V : Type ?u.11995} β [inst : Quiver V] β {a b : V} β Path a b β List VtoList
| _, nil: {V : Type ?u.12053} β [inst : Quiver V] β {a : V} β Path a anil => byGoals accomplished! π V: Type uinstβ: Quiver Va, b, c, d: Vp: Path a btoList (comp p nil) = toList nil ++ toList psimpGoals accomplished! π
| _, @cons: {V : Type ?u.12091} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons _: Type u_ _ _: V_ d: Vd _ q: Path b dq _ => byGoals accomplished! π V: Type uinstβ: Quiver Va, b, c, dβ: Vp: Path a bxβ, d: Vq: Path b daβ: d βΆ xβtoList (comp p (cons q aβ)) = toList (cons q aβ) ++ toList psimp [toList_comp: β (p : Path a b) {c : V} (q : Path b c), toList (comp p q) = toList q ++ toList ptoList_comp]Goals accomplished! π
#align quiver.path.to_list_comp Quiver.Path.toList_comp: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b) {c : V} (q : Path b c),
toList (comp p q) = toList q ++ toList pQuiver.Path.toList_comp

theorem toList_chain_nonempty: β {b : V} (p : Path a b), List.Chain (fun x y => Nonempty (y βΆ x)) b (toList p)toList_chain_nonempty :
β {b: ?m.12734b} (p: Path a bp : Path: {V : Type ?u.12737} β [inst : Quiver V] β V β V β Sort (max(?u.12737+1)?u.12738)Path a: Va b: ?m.12734b), p: Path a bp.toList: {V : Type ?u.12753} β [inst : Quiver V] β {a b : V} β Path a b β List VtoList.Chain: {Ξ± : Type ?u.12765} β (Ξ± β Ξ± β Prop) β Ξ± β List Ξ± β PropChain (fun x: ?m.12772x y: ?m.12775y => Nonempty: Sort ?u.12777 β PropNonempty (y: ?m.12775y βΆ x: ?m.12772x)) b: ?m.12734b
| _, nil: {V : Type ?u.12821} β [inst : Quiver V] β {a : V} β Path a anil => List.Chain.nil: β {Ξ± : Type ?u.12862} {R : Ξ± β Ξ± β Prop} {a : Ξ±}, List.Chain R a []List.Chain.nil
| _, cons: {V : Type ?u.12887} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons p: Path a bβp f: bβ βΆ xβf => p: Path a bβp.toList_chain_nonempty: β {b : V} (p : Path a b), List.Chain (fun x y => Nonempty (y βΆ x)) b (toList p)toList_chain_nonempty.cons: β {Ξ± : Type ?u.12947} {R : Ξ± β Ξ± β Prop} {a b : Ξ±} {l : List Ξ±}, R a b β List.Chain R b l β List.Chain R a (b :: l)cons β¨f: bβ βΆ xβfβ©
#align quiver.path.to_list_chain_nonempty Quiver.Path.toList_chain_nonempty: β {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b), List.Chain (fun x y => Nonempty (y βΆ x)) b (toList p)Quiver.Path.toList_chain_nonempty

variable [β a: Va b: Vb : V: Type uV, Subsingleton: Sort ?u.13313 β PropSubsingleton (a: Va βΆ b: Vb)]

theorem toList_injective: β (a b : V), Injective toListtoList_injective (a: Va : V: Type uV) : β b: ?m.13371b, Injective: {Ξ± : Sort ?u.13375} β {Ξ² : Sort ?u.13374} β (Ξ± β Ξ²) β PropInjective (toList: {V : Type ?u.13396} β [inst : Quiver V] β {a b : V} β Path a b β List VtoList : Path: {V : Type ?u.13380} β [inst : Quiver V] β V β V β Sort (max(?u.13380+1)?u.13381)Path a: Va b: ?m.13371b β List: Type ?u.13394 β Type ?u.13394List V: Type uV)
| _, nil: {V : Type ?u.13436} β [inst : Quiver V] β {a : V} β Path a anil, nil: {V : Type ?u.13443} β [inst : Quiver V] β {a : V} β Path a anil, _ => rfl: β {Ξ± : Sort ?u.13505} {a : Ξ±}, a = arfl
| _, nil: {V : Type ?u.13513} β [inst : Quiver V] β {a : V} β Path a anil, @cons: {V : Type ?u.13518} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons _: Type u_ _ _: V_ c: Vc _ p: Path a cp f: c βΆ af, h: toList nil = toList (cons p f)h => byGoals accomplished! π V: Type uinstβΒΉ: Quiver Vaβ, b, cβ, d: Vinstβ: β (a b : V), Subsingleton (a βΆ b)a, c: Vp: Path a cf: c βΆ ah: toList nil = toList (cons p f)nil = cons p fcases h: toList nil = toList (cons p f)hGoals accomplished! π
| _, @cons: {V : Type ?u.13594} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons _: Type u_ _ _: V_ c: Vc _ p: Path a cp f: c βΆ af, nil: {V : Type ?u.13605} β [inst : Quiver V] β {a : V} β Path a anil, h: toList (cons p f) = toList nilh => byGoals accomplished! π V: Type uinstβΒΉ: Quiver Vaβ, b, cβ, d: Vinstβ: β (a b : V), Subsingleton (a βΆ b)a, c: Vp: Path a cf: c βΆ ah: toList (cons p f) = toList nilcons p f = nilcases h: toList (cons p f) = toList nilhGoals accomplished! π
| _, @cons: {V : Type ?u.13677} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons _: Type u_ _ _: V_ c: Vc _ p: Path a cp f: c βΆ xβf, @cons: {V : Type ?u.13686} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a ccons _: Type u_ _ _: V_ t: Vt _ C: Path a tC D: t βΆ xβD, h: toList (cons p f) = toList (cons C D)h => byGoals accomplished! π
V: Type uinstβΒΉ: Quiver Vaβ, b, cβ, d: Vinstβ: β (a b : V), Subsingleton (a βΆ b)a, xβ, c: Vp: Path a cf: c βΆ xβt: VC: Path a tD: t βΆ xβh: toList (cons p f) = toList (cons C D)cons p f = cons C Dsimp only [toList: {V : Type ?u.14657} β [inst : Quiver V] β {a b : V} β Path a b β List VtoList, List.cons.injEq: β {Ξ± : Type ?u.14694} (head : Ξ±) (tail : List Ξ±) (head_1 : Ξ±) (tail_1 : List Ξ±),
(head :: tail = head_1 :: tail_1) = (head = head_1 β§ tail = tail_1)List.cons.injEq] at h: toList (cons p f) = toList (cons C D)hV: Type uinstβΒΉ: Quiver Vaβ, b, cβ, d: Vinstβ: β (a b : V), Subsingleton (a βΆ b)a, xβ, c: Vp: Path a cf: c βΆ xβt: VC: Path a tD: t βΆ xβh: c = t β§ toList p = toList Ccons p f = cons C D
V: Type uinstβΒΉ: Quiver Vaβ, b, cβ, d: Vinstβ: β (a b : V), Subsingleton (a βΆ b)a, xβ, c: Vp: Path a cf: c βΆ xβt: VC: Path a tD: t βΆ xβh: toList (cons p f) = toList (cons C D)cons p f = cons C Dobtain β¨rfl, hACβ©: c = t β§ toList p = toList Cβ¨rfl: c = trflβ¨rfl, hACβ©: c = t β§ toList p = toList C, hAC: unknown free variable '_uniq.14815'hACβ¨rfl, hACβ©: c = t β§ toList p = toList Cβ© := h: c = t β§ toList p = toList ChV: Type uinstβΒΉ: Quiver Vaβ, b, cβ, d: Vinstβ: β (a b : V), Subsingleton (a βΆ b)a, xβ, c: Vp: Path a cf: c βΆ xβC: Path a cD: c βΆ xβhAC: toList p = toList Cintrocons p f = cons C D
V: Type uinstβΒΉ: Quiver Vaβ, b, cβ, d: Vinstβ: β (a b : V), Subsingleton (a βΆ b)a, xβ, c: Vp: Path a cf: c βΆ xβt: VC: Path a tD: t βΆ xβh: toList (cons p f) = toList (cons C D)cons p f = cons C Dsimp [toList_injective: β (a b : V), Injective toListtoList_injective _: V_ _: V_ hAC: toList p = toList ChAC]Goals accomplished! π
#align quiver.path.to_list_injective Quiver.Path.toList_injective: β {V : Type u} [inst : Quiver V] [inst_1 : β (a b : V), Subsingleton (a βΆ b)] (a b : V), Injective toListQuiver.Path.toList_injective

@[simp]
theorem toList_inj: β {V : Type u} [inst : Quiver V] {a b : V} [inst_1 : β (a b : V), Subsingleton (a βΆ b)] {p q : Path a b},
toList p = toList q β p = qtoList_inj {p: Path a bp q: Path a bq : Path: {V : Type ?u.15292} β [inst : Quiver V] β V β V β Sort (max(?u.15292+1)?u.15293)Path a: Va b: Vb} : p: Path a bp.toList: {V : Type ?u.15308} β [inst : Quiver V] β {a b : V} β Path a b β List VtoList = q: Path a bq.toList: {V : Type ?u.15326} β [inst : Quiver V] β {a b : V} β Path a b β List VtoList β p: Path a bp = q: Path a bq :=
(toList_injective: β {V : Type ?u.15344} [inst : Quiver V] [inst_1 : β (a b : V), Subsingleton (a βΆ b)] (a b : V), Injective toListtoList_injective _: ?m.15346_ _: ?m.15346_).eq_iff: β {Ξ± : Sort ?u.15380} {Ξ² : Sort ?u.15381} {f : Ξ± β Ξ²}, Injective f β β {a b : Ξ±}, f a = f b β a = beq_iff
#align quiver.path.to_list_inj Quiver.Path.toList_inj: β {V : Type u} [inst : Quiver V] {a b : V} [inst_1 : β (a b : V), Subsingleton (a βΆ b)] {p q : Path a b},
toList p = toList q β p = qQuiver.Path.toList_inj

end Path

end Quiver

namespace Prefunctor

open Quiver

variable {V: Type uβV : Type uβ: Type (uβ+1)Type uβ} [Quiver: Type ?u.16904 β Type (max?u.16904vβ)Quiver.{vβ} V: Type uβV] {W: Type uβW : Type uβ: Type (uβ+1)Type uβ} [Quiver: Type ?u.16667 β Type (max?u.16667vβ)Quiver.{vβ} W: Type uβW] (F: V β₯€q WF : V: Type uβV β₯€q W: Type uβW)

/-- The image of a path under a prefunctor. -/
def mapPath: {V : Type uβ} β
[inst : Quiver V] β
{W : Type uβ} β [inst_1 : Quiver W] β (F : V β₯€q W) β {a b : V} β Path a b β Path (F.obj a) (F.obj b)mapPath {a: Va : V: Type uβV} : β {b: Vb : V: Type uβV}, Path: {V : Type ?u.15565} β [inst : Quiver V] β V β V β Sort (max(?u.15565+1)?u.15566)Path a: Va b: Vb β Path: {V : Type ?u.15579} β [inst : Quiver V] β V β V β Sort (max(?u.15579+1)?u.15580)Path (F: V β₯€q WF.obj: {V : Type ?u.15589} β [inst : Quiver V] β {W : Type ?u.15588} β [inst_1 : Quiver W] β V β₯€q W β V β Wobj a: Va) (F: V β₯€q WF.obj: {V : Type ?u.15608} β [inst : Quiver V] β {W : Type ?u.15607} β [inst_1 : Quiver W] β V β₯€q W β V β Wobj b: Vb)
| _, Path.nil: {V : Type ?u.15630} β [inst : Quiver V] β {a : V} β Path a aPath.nil => Path.nil: {V : Type ?u.15666} β [inst : Quiver V] β {a : V} β Path a aPath.nil
| _, Path.cons: {V : Type ?u.15681} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a cPath.cons p: Path a bβp e: bβ βΆ xβe => Path.cons: {V : Type ?u.15742} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a cPath.cons (mapPath: {a b : V} β Path a b β Path (F.obj a) (F.obj b)mapPath p: Path a bβp) (F: V β₯€q WF.map: {V : Type ?u.15764} β
[inst : Quiver V] β
{W : Type ?u.15763} β [inst_1 : Quiver W] β (self : V β₯€q W) β {X Y : V} β (X βΆ Y) β (self.obj X βΆ self.obj Y)map e: bβ βΆ xβe)
#align prefunctor.map_path Prefunctor.mapPath: {V : Type uβ} β
[inst : Quiver V] β
{W : Type uβ} β [inst_1 : Quiver W] β (F : V β₯€q W) β {a b : V} β Path a b β Path (F.obj a) (F.obj b)Prefunctor.mapPath

@[simp]
theorem mapPath_nil: β (a : V), mapPath F Path.nil = Path.nilmapPath_nil (a: Va : V: Type uβV) : F: V β₯€q WF.mapPath: {V : Type ?u.16496} β
[inst : Quiver V] β
{W : Type ?u.16495} β [inst_1 : Quiver W] β (F : V β₯€q W) β {a b : V} β Path a b β Path (F.obj a) (F.obj b)mapPath (Path.nil: {V : Type ?u.16533} β [inst : Quiver V] β {a : V} β Path a aPath.nil : Path: {V : Type ?u.16520} β [inst : Quiver V] β V β V β Sort (max(?u.16520+1)?u.16521)Path a: Va a: Va) = Path.nil: {V : Type ?u.16553} β [inst : Quiver V] β {a : V} β Path a aPath.nil :=
rfl: β {Ξ± : Sort ?u.16611} {a : Ξ±}, a = arfl
#align prefunctor.map_path_nil Prefunctor.mapPath_nil: β {V : Type uβ} [inst : Quiver V] {W : Type uβ} [inst_1 : Quiver W] (F : V β₯€q W) (a : V), mapPath F Path.nil = Path.nilPrefunctor.mapPath_nil

@[simp]
theorem mapPath_cons: β {a b c : V} (p : Path a b) (e : b βΆ c), mapPath F (Path.cons p e) = Path.cons (mapPath F p) (F.map e)mapPath_cons {a: Va b: Vb c: Vc : V: Type uβV} (p: Path a bp : Path: {V : Type ?u.16692} β [inst : Quiver V] β V β V β Sort (max(?u.16692+1)?u.16693)Path a: Va b: Vb) (e: b βΆ ce : b: Vb βΆ c: Vc) :
F: V β₯€q WF.mapPath: {V : Type ?u.16723} β
[inst : Quiver V] β
{W : Type ?u.16722} β [inst_1 : Quiver W] β (F : V β₯€q W) β {a b : V} β Path a b β Path (F.obj a) (F.obj b)mapPath (Path.cons: {V : Type ?u.16746} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a cPath.cons p: Path a bp e: b βΆ ce) = Path.cons: {V : Type ?u.16772} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a cPath.cons (F: V β₯€q WF.mapPath: {V : Type ?u.16780} β
[inst : Quiver V] β
{W : Type ?u.16779} β [inst_1 : Quiver W] β (F : V β₯€q W) β {a b : V} β Path a b β Path (F.obj a) (F.obj b)mapPath p: Path a bp) (F: V β₯€q WF.map: {V : Type ?u.16809} β
[inst : Quiver V] β
{W : Type ?u.16808} β [inst_1 : Quiver W] β (self : V β₯€q W) β {X Y : V} β (X βΆ Y) β (self.obj X βΆ self.obj Y)map e: b βΆ ce) :=
rfl: β {Ξ± : Sort ?u.16837} {a : Ξ±}, a = arfl
#align prefunctor.map_path_cons Prefunctor.mapPath_cons: β {V : Type uβ} [inst : Quiver V] {W : Type uβ} [inst_1 : Quiver W] (F : V β₯€q W) {a b c : V} (p : Path a b) (e : b βΆ c),
mapPath F (Path.cons p e) = Path.cons (mapPath F p) (F.map e)Prefunctor.mapPath_cons

@[simp]
theorem mapPath_comp: β {V : Type uβ} [inst : Quiver V] {W : Type uβ} [inst_1 : Quiver W] (F : V β₯€q W) {a b : V} (p : Path a b) {c : V}
(q : Path b c), mapPath F (Path.comp p q) = Path.comp (mapPath F p) (mapPath F q)mapPath_comp {a: Va b: Vb : V: Type uβV} (p: Path a bp : Path: {V : Type ?u.16932} β [inst : Quiver V] β V β V β Sort (max(?u.16932+1)?u.16933)Path a: Va b: Vb) :
β {c: Vc : V: Type uβV} (q: Path b cq : Path: {V : Type ?u.16950} β [inst : Quiver V] β V β V β Sort (max(?u.16950+1)?u.16951)Path b: Vb c: Vc), F: V β₯€q WF.mapPath: {V : Type ?u.16966} β
[inst : Quiver V] β
{W : Type ?u.16965} β [inst_1 : Quiver W] β (F : V β₯€q W) β {a b : V} β Path a b β Path (F.obj a) (F.obj b)mapPath (p: Path a bp.comp: {V : Type ?u.16990} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp q: Path b cq) = (F: V β₯€q WF.mapPath: {V : Type ?u.17014} β
[inst : Quiver V] β
{W : Type ?u.17013} β [inst_1 : Quiver W] β (F : V β₯€q W) β {a b : V} β Path a b β Path (F.obj a) (F.obj b)mapPath p: Path a bp).comp: {V : Type ?u.17034} β [inst : Quiver V] β {a b c : V} β Path a b β Path b c β Path a ccomp (F: V β₯€q WF.mapPath: {V : Type ?u.17053} β
[inst : Quiver V] β
{W : Type ?u.17052} β [inst_1 : Quiver W] β (F : V β₯€q W) β {a b : V} β Path a b β Path (F.obj a) (F.obj b)mapPath q: Path b cq)
| _, Path.nil: {V : Type ?u.17091} β [inst : Quiver V] β {a : V} β Path a aPath.nil => rfl: β {Ξ± : Sort ?u.17127} {a : Ξ±}, a = arfl
| c: Vc, Path.cons: {V : Type ?u.17198} β [inst : Quiver V] β {a b c : V} β Path a b β (b βΆ c) β Path a cPath.cons q: Path b bβq e: bβ βΆ ce => byGoals accomplished! π V: Type uβinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF: V β₯€q Wa, b: Vp: Path a bc, bβ: Vq: Path b bβe: bβ βΆ cmapPath F (Path.comp p (Path.cons q e)) = Path.comp (mapPath F p) (mapPath F (Path.cons q e))dsimpV: Type uβinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF: V β₯€q Wa, b: Vp: Path a bc, bβ: Vq: Path b bβe: bβ βΆ cPath.cons (mapPath F (Path.comp p q)) (F.map e) = Path.cons (Path.comp (mapPath F p) (mapPath F q)) (F.map e);V: Type uβinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF: V β₯€q Wa, b: Vp: Path a bc, bβ: Vq: Path b bβe: bβ βΆ cPath.cons (mapPath F (Path.comp p q)) (F.map e) = Path.cons (Path.comp (mapPath F p) (mapPath F q)) (F.map e) V: Type uβinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF: V β₯€q Wa, b: Vp: Path a bc, bβ: Vq: Path b bβe: bβ βΆ cmapPath F (Path.comp p (Path.cons q e)) = Path.comp (mapPath F p) (mapPath F (Path.cons q e))rw [V: Type uβinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF: V β₯€q Wa, b: Vp: Path a bc, bβ: Vq: Path b bβe: bβ βΆ cPath.cons (mapPath F (Path.comp p q)) (F.map e) = Path.cons (Path.comp (mapPath F p) (mapPath F q)) (F.map e)mapPath_comp: β {a b : V} (p : Path a b) {c : V} (q : Path b c), mapPath F (Path.comp p q) = Path.comp (mapPath F p) (mapPath F q)mapPath_comp p: Path a bp q: Path b bβqV: Type uβinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF: V β₯€q Wa, b: Vp: Path a bc, bβ: Vq: Path b bβe: bβ βΆ cPath.cons (Path.comp (mapPath F p) (mapPath F q)) (F.map e) =   Path.cons (Path.comp (mapPath F p) (mapPath F q)) (F.map e)]Goals accomplished! π
#align prefunctor.map_path_comp Prefunctor.mapPath_comp: β {V : Type uβ} [inst : Quiver V] {W : Type uβ} [inst_1 : Quiver W] (F : V β₯€q W) {a b : V} (p : Path a b) {c : V}
(q : Path b c), mapPath F (Path.comp p q) = Path.comp (mapPath F p) (mapPath F q)Prefunctor.mapPath_comp

@[simp]
theorem mapPath_toPath: β {a b : V} (f : a βΆ b), mapPath F (Hom.toPath f) = Hom.toPath (F.map f)mapPath_toPath {a: Va b: Vb : V: Type uβV} (f: a βΆ bf : a: Va βΆ b: Vb) : F: V β₯€q WF.mapPath: {V : Type ?u.17780} β
[inst : Quiver V] β
{W : Type ?u.17779} β [inst_1 : Quiver W] β (F : V β₯€q W) β {a b : V} β Path a b β Path (F.obj a) (F.obj b)mapPath f: a βΆ bf.toPath: {V : Type ?u.17804} β [inst : Quiver V] β {a b : V} β (a βΆ b) β Path a btoPath = (F: V β₯€q WF.map: {V : Type ?u.17829} β
[inst : Quiver V] β
{W : Type ?u.17828} β [inst_1 : Quiver W] β (self : V β₯€q W) β {X Y : V} β (X βΆ Y) β (self.obj X βΆ self.obj Y)map f: a βΆ bf).toPath: {V : Type ?u.17841} β [inst : Quiver V] β {a b : V} β (a βΆ b) β Path a btoPath :=
rfl: β {Ξ± : Sort ?u.17865} {a : Ξ±}, a = arfl
#align prefunctor.map_path_to_path Prefunctor.mapPath_toPath: β {V : Type uβ} [inst : Quiver V] {W : Type uβ} [inst_1 : Quiver W] (F : V β₯€q W) {a b : V} (f : a βΆ b),
mapPath F (Hom.toPath f) = Hom.toPath (F.map f)Prefunctor.mapPath_toPath

end Prefunctor
```