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. 
/-
Copyright (c) 2021 David WΓ€rn,. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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 u
V : 
Type u: Type (u+1)
Type u} [
Quiver: Type ?u.4 β†’ Type (max?u.4v)
Quiver.{v} 
V: Type u
V] (
a: V
a : 
V: Type u
V) : 
V: Type u
V β†’ 
Sort max (u + 1) v: Type (max(u+1)v)
Sort
Sort max (u + 1) v: Type (max(u+1)v)
 
Sort max (u + 1) v: Type (max(u+1)v)
max
Sort max (u + 1) v: Type (max(u+1)v)
 (u + 1) v
  | 
nil: {V : Type u} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil : 
Path: {V : Type u} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(u+1)v)
Path 
a: V
a 
a: V
a
  | 
cons: {V : Type u} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons : βˆ€ {
b: V
b 
c: V
c : 
V: Type u
V}, 
Path: {V : Type u} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(u+1)v)
Path 
a: V
a 
b: V
b β†’ (
b: V
b ⟢ 
c: V
c) β†’ 
Path: {V : Type u} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(u+1)v)
Path 
a: V
a 
c: V
c
#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 b
Hom.toPath {
V: Type ?u.1485
V} [
Quiver: Type ?u.1485 β†’ Type (max?u.1485?u.1486)
Quiver 
V: ?m.1482
V] {
a: V
a 
b: V
b : 
V: ?m.1482
V} (
e: a ⟢ b
e : 
a: V
a ⟢ 
b: V
b) : 
Path: {V : Type ?u.1508} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.1508+1)?u.1509)
Path 
a: V
a 
b: V
b :=
  
Path.nil: {V : Type ?u.1526} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
Path.nil.
cons: {V : Type ?u.1536} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e: a ⟢ b
e
#align quiver.hom.to_path 
Quiver.Hom.toPath: {V : Type u_1} β†’ [inst : Quiver V] β†’ {a b : V} β†’ (a ⟢ b) β†’ Path a b
Quiver.Hom.toPath

namespace Path

variable {
V: Type u
V : 
Type u: Type (u+1)
Type u} [
Quiver: Type ?u.3675 β†’ Type (max?u.3675?u.3676)
Quiver 
V: Type u
V] {
a: V
a 
b: V
b 
c: V
c 
d: V
d : 
V: Type u
V}

lemma 
nil_ne_cons: βˆ€ (p : Path a b) (e : b ⟢ a), nil β‰  cons p e
nil_ne_cons (
p: Path a b
p : 
Path: {V : Type ?u.1638} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.1638+1)?u.1639)
Path 
a: V
a 
b: V
b) (
e: b ⟢ a
e : 
b: V
b ⟢ 
a: V
a) : 
Path.nil: {V : Type ?u.1669} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
Path.nil β‰  
p: Path a b
p.
cons: {V : Type ?u.1683} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e: b ⟢ a
e :=
fun 
h: ?m.1715
h => 
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p: Path a b

e: b ⟢ a

h: nil = cons p e

False
Goals 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 e
Quiver.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 β‰  nil
cons_ne_nil (
p: Path a b
p : 
Path: {V : Type ?u.1743} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.1743+1)?u.1744)
Path 
a: V
a 
b: V
b) (
e: b ⟢ a
e : 
b: V
b ⟢ 
a: V
a) : 
p: Path a b
p.
cons: {V : Type ?u.1774} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e: b ⟢ a
e β‰  
Path.nil: {V : Type ?u.1799} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
Path.nil :=
fun 
h: ?m.1816
h => 
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p: Path a b

e: b ⟢ a

h: cons p e = nil

False
Goals 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 β‰  nil
Quiver.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 = c
obj_eq_of_cons_eq_cons {
p: Path a b
p : 
Path: {V : Type ?u.1844} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.1844+1)?u.1845)
Path 
a: V
a 
b: V
b} {
p': Path a c
p' : 
Path: {V : Type ?u.1859} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.1859+1)?u.1860)
Path 
a: V
a 
c: V
c}
  {
e: b ⟢ d
e : 
b: V
b ⟢ 
d: V
d} {
e': c ⟢ d
e' : 
c: V
c ⟢ 
d: V
d} (
h: cons p e = cons p' e'
h : 
p: Path a b
p.
cons: {V : Type ?u.1902} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e: b ⟢ d
e = 
p': Path a c
p'.
cons: {V : Type ?u.1927} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e': c ⟢ d
e') : 
b: V
b = 
c: V
c := 
Goals accomplished! πŸ™
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

h: cons p e = cons p' e'

b = c
Goals 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 = c
Quiver.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 b
p : 
Path: {V : Type ?u.2015} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.2015+1)?u.2016)
Path 
a: V
a 
b: V
b} {
p': Path a c
p' : 
Path: {V : Type ?u.2030} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.2030+1)?u.2031)
Path 
a: V
a 
c: V
c}
  {
e: b ⟢ d
e : 
b: V
b ⟢ 
d: V
d} {
e': c ⟢ d
e' : 
c: V
c ⟢ 
d: V
d} (
h: cons p e = cons p' e'
h : 
p: Path a b
p.
cons: {V : Type ?u.2073} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e: b ⟢ d
e = 
p': Path a c
p'.
cons: {V : Type ?u.2098} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e': c ⟢ d
e') : 
HEq: {Ξ± : Sort ?u.2116} β†’ Ξ± β†’ {Ξ² : Sort ?u.2116} β†’ Ξ² β†’ Prop
HEq 
p: Path a b
p 
p': Path a c
p' := 
Goals accomplished! πŸ™
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

h: cons p e = cons p' e'

HEq p p'
Goals 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 b
p : 
Path: {V : Type ?u.2188} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.2188+1)?u.2189)
Path 
a: V
a 
b: V
b} {
p': Path a c
p' : 
Path: {V : Type ?u.2203} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.2203+1)?u.2204)
Path 
a: V
a 
c: V
c}
  {
e: b ⟢ d
e : 
b: V
b ⟢ 
d: V
d} {
e': c ⟢ d
e' : 
c: V
c ⟢ 
d: V
d} (
h: cons p e = cons p' e'
h : 
p: Path a b
p.
cons: {V : Type ?u.2246} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e: b ⟢ d
e = 
p': Path a c
p'.
cons: {V : Type ?u.2271} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e': c ⟢ d
e') : 
HEq: {Ξ± : Sort ?u.2289} β†’ Ξ± β†’ {Ξ² : Sort ?u.2289} β†’ Ξ² β†’ Prop
HEq 
e: b ⟢ d
e 
e': c ⟢ d
e' := 
Goals accomplished! πŸ™
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

h: cons p e = cons p' e'

HEq e e'
Goals 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: V
a : 
V: Type u
V} : βˆ€ {
b: V
b : 
V: Type u
V}, 
Path: {V : Type ?u.2363} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.2363+1)?u.2364)
Path 
a: V
a 
b: V
b β†’ 
β„•: Type
β„•
  | _, 
nil: {V : Type ?u.2387} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil => 
0: ?m.2420
0
  | _, 
cons: {V : Type ?u.2430} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
p: Path a b✝
p _ => 
p: Path a b✝
p.
length: {a b : V} β†’ Path a b β†’ β„•
length + 
1: ?m.2500
1
#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: V
a : 
V: Type u
V} : 
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: V
a 
a: V
a) :=
  ⟨
nil: {V : Type ?u.3265} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil⟩

@[simp]
theorem 
length_nil: βˆ€ {a : V}, length nil = 0
length_nil {
a: V
a : 
V: Type u
V} : (
nil: {V : Type ?u.3359} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil : 
Path: {V : Type ?u.3346} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.3346+1)?u.3347)
Path 
a: V
a 
a: V
a).
length: {V : Type ?u.3377} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ β„•
length = 
0: ?m.3389
0 :=
  
rfl: βˆ€ {Ξ± : Sort ?u.3415} {a : Ξ±}, a = a
rfl
#align quiver.path.length_nil 
Quiver.Path.length_nil: βˆ€ {V : Type u} [inst : Quiver V] {a : V}, length nil = 0
Quiver.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 + 1
length_cons (
a: V
a 
b: V
b 
c: V
c : 
V: Type u
V) (
p: Path a b
p : 
Path: {V : Type ?u.3472} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.3472+1)?u.3473)
Path 
a: V
a 
b: V
b) (
e: b ⟢ c
e : 
b: V
b ⟢ 
c: V
c) : (
p: Path a b
p.
cons: {V : Type ?u.3502} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e: b ⟢ c
e).
length: {V : Type ?u.3528} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ β„•
length = 
p: Path a b
p.
length: {V : Type ?u.3543} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ β„•
length + 
1: ?m.3555
1 :=
  
rfl: βˆ€ {Ξ± : Sort ?u.3620} {a : Ξ±}, a = a
rfl
#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 + 1
Quiver.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 = b
eq_of_length_zero (
p: Path a b
p : 
Path: {V : Type ?u.3687} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.3687+1)?u.3688)
Path 
a: V
a 
b: V
b) (
hzero: length p = 0
hzero : 
p: Path a b
p.
length: {V : Type ?u.3704} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ β„•
length = 
0: ?m.3722
0) : 
a: V
a = 
b: V
b := 
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p: Path a b

hzero: length p = 0

a = b
V: Type u

inst✝: Quiver V

a, c, d: V

hzero: length nil = 0

nil
a = a
V: Type u

inst✝: Quiver V

a, b, c, d, b✝: V

a✝¹: Path a b✝

a✝: b✝ ⟢ b

hzero: length (cons a✝¹ a✝) = 0

cons
a = b
V: Type u

inst✝: Quiver V

a, b, c, d: V

p: Path a b

hzero: length p = 0

a = b
V: Type u

inst✝: Quiver V

a, c, d: V

hzero: length nil = 0

nil
a = a
V: Type u

inst✝: Quiver V

a, c, d: V

hzero: length nil = 0

nil
a = a
V: Type u

inst✝: Quiver V

a, b, c, d, b✝: V

a✝¹: Path a b✝

a✝: b✝ ⟢ b

hzero: length (cons a✝¹ a✝) = 0

cons
a = b
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p: Path a b

hzero: length p = 0

a = b
V: Type u

inst✝: Quiver V

a, b, c, d, b✝: V

a✝¹: Path a b✝

a✝: b✝ ⟢ b

hzero: length (cons a✝¹ a✝) = 0

cons
a = b
V: Type u

inst✝: Quiver V

a, b, c, d, b✝: V

a✝¹: Path a b✝

a✝: b✝ ⟢ b

hzero: length (cons a✝¹ a✝) = 0

cons
a = b
Goals 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 = b
Quiver.Path.eq_of_length_zero

/-- Composition of paths. -/
def 
comp: {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp {
a: V
a 
b: V
b : 
V: Type u
V} : βˆ€ {
c: ?m.3997
c}, 
Path: {V : Type ?u.4001} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.4001+1)?u.4002)
Path 
a: V
a 
b: V
b β†’ 
Path: {V : Type ?u.4016} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.4016+1)?u.4017)
Path 
b: V
b 
c: ?m.3997
c β†’ 
Path: {V : Type ?u.4029} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.4029+1)?u.4030)
Path 
a: V
a 
c: ?m.3997
c
  | _, 
p: Path a b
p, 
nil: {V : Type ?u.4055} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil => 
p: Path a b
p
  | _, 
p: Path a b
p, 
cons: {V : Type ?u.4096} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
q: Path b b✝
q 
e: b✝ ⟢ x✝
e => (
p: Path a b
p.
comp: {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q: Path b b✝
q).
cons: {V : Type ?u.4174} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
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 c
Quiver.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) e
comp_cons {
a: V
a 
b: V
b 
c: V
c 
d: V
d : 
V: Type u
V} (
p: Path a b
p : 
Path: {V : Type ?u.4986} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.4986+1)?u.4987)
Path 
a: V
a 
b: V
b) (
q: Path b c
q : 
Path: {V : Type ?u.5001} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.5001+1)?u.5002)
Path 
b: V
b 
c: V
c) (
e: c ⟢ d
e : 
c: V
c ⟢ 
d: V
d) :
    
p: Path a b
p.
comp: {V : Type ?u.5031} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp (
q: Path b c
q.
cons: {V : Type ?u.5049} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e: c ⟢ d
e) = (
p: Path a b
p.
comp: {V : Type ?u.5071} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q: Path b c
q).
cons: {V : Type ?u.5085} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
e: c ⟢ d
e :=
  
rfl: βˆ€ {Ξ± : Sort ?u.5109} {a : Ξ±}, a = a
rfl
#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) e
Quiver.Path.comp_cons

@[simp]
theorem 
comp_nil: βˆ€ {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b), comp p nil = p
comp_nil {
a: V
a 
b: V
b : 
V: Type u
V} (
p: Path a b
p : 
Path: {V : Type ?u.5190} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.5190+1)?u.5191)
Path 
a: V
a 
b: V
b) : 
p: Path a b
p.
comp: {V : Type ?u.5207} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
Path.nil: {V : Type ?u.5225} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
Path.nil = 
p: Path a b
p :=
  
rfl: βˆ€ {Ξ± : Sort ?u.5243} {a : Ξ±}, a = a
rfl
#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 = p
Quiver.Path.comp_nil

@[simp]
theorem 
nil_comp: βˆ€ {V : Type u} [inst : Quiver V] {a b : V} (p : Path a b), comp nil p = p
nil_comp {
a: V
a : 
V: Type u
V} : βˆ€ {
b: ?m.5307
b} (
p: Path a b
p : 
Path: {V : Type ?u.5310} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.5310+1)?u.5311)
Path 
a: V
a 
b: ?m.5307
b), 
Path.nil: {V : Type ?u.5326} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
Path.nil.
comp: {V : Type ?u.5337} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
p: Path a b
p = 
p: Path a b
p
  | _, 
nil: {V : Type ?u.5377} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil => 
rfl: βˆ€ {Ξ± : Sort ?u.5414} {a : Ξ±}, a = a
rfl
  | _, 
cons: {V : Type ?u.5435} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
p: Path a b✝
p _ => 
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a✝¹, b, c, d, a, x✝, b✝: V

p: Path a b✝

a✝: b✝ ⟢ x✝

comp nil (cons p a✝) = cons p a✝
V: Type u

inst✝: Quiver V

a✝¹, b, c, d, a, x✝, b✝: V

p: Path a b✝

a✝: b✝ ⟢ x✝

comp nil (cons p a✝) = cons p a✝
V: Type u

inst✝: Quiver V

a✝¹, b, c, d, a, x✝, b✝: V

p: Path a b✝

a✝: b✝ ⟢ x✝

cons (comp nil p) a✝ = cons p a✝
V: Type u

inst✝: Quiver V

a✝¹, b, c, d, a, x✝, b✝: V

p: Path a b✝

a✝: b✝ ⟢ x✝

comp nil (cons p a✝) = cons p a✝
V: Type u

inst✝: Quiver V

a✝¹, b, c, d, a, x✝, b✝: V

p: 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 = p
Quiver.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: V
a 
b: V
b 
c: V
c : 
V: Type u
V} :
    βˆ€ {
d: ?m.5922
d} (
p: Path a b
p : 
Path: {V : Type ?u.5925} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.5925+1)?u.5926)
Path 
a: V
a 
b: V
b) (
q: Path b c
q : 
Path: {V : Type ?u.5940} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.5940+1)?u.5941)
Path 
b: V
b 
c: V
c) (
r: Path c d
r : 
Path: {V : Type ?u.5954} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.5954+1)?u.5955)
Path 
c: V
c 
d: ?m.5922
d), (
p: Path a b
p.
comp: {V : Type ?u.5970} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q: Path b c
q).
comp: {V : Type ?u.5991} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
r: Path c d
r = 
p: Path a b
p.
comp: {V : Type ?u.6006} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp (
q: Path b c
q.
comp: {V : Type ?u.6021} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
r: Path c d
r)
  | _, _, _, 
nil: {V : Type ?u.6054} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil => 
rfl: βˆ€ {Ξ± : Sort ?u.6105} {a : Ξ±}, a = a
rfl
  | _, 
p: Path a b
p, 
q: Path b c
q, 
cons: {V : Type ?u.6153} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
r: Path c b✝
r _ => 
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a✝¹, b✝¹, c✝, d, a, b, c, x✝: V

p: Path a b

q: Path b c

b✝: V

r: Path c b✝

a✝: b✝ ⟢ x✝

comp (comp p q) (cons r a✝) = comp p (comp q (cons r a✝))
V: Type u

inst✝: Quiver V

a✝¹, b✝¹, c✝, d, a, b, c, x✝: V

p: Path a b

q: Path b c

b✝: V

r: Path c b✝

a✝: b✝ ⟢ x✝

comp (comp p q) (cons r a✝) = comp p (comp q (cons r a✝))
V: Type u

inst✝: Quiver V

a✝¹, b✝¹, c✝, d, a, b, c, x✝: V

p: Path a b

q: Path b c

b✝: V

r: Path c b✝

a✝: b✝ ⟢ x✝

cons (comp (comp p q) r) a✝ = comp p (comp q (cons r a✝))
V: Type u

inst✝: Quiver V

a✝¹, b✝¹, c✝, d, a, b, c, x✝: V

p: Path a b

q: Path b c

b✝: V

r: Path c b✝

a✝: b✝ ⟢ x✝

comp (comp p q) (cons r a✝) = comp p (comp q (cons r a✝))
V: Type u

inst✝: Quiver V

a✝¹, b✝¹, c✝, d, a, b, c, x✝: V

p: Path a b

q: Path b c

b✝: V

r: Path c b✝

a✝: b✝ ⟢ x✝

cons (comp (comp p q) r) a✝ = comp p (cons (comp q r) a✝)
V: Type u

inst✝: Quiver V

a✝¹, b✝¹, c✝, d, a, b, c, x✝: V

p: Path a b

q: Path b c

b✝: V

r: Path c b✝

a✝: b✝ ⟢ x✝

comp (comp p q) (cons r a✝) = comp p (comp q (cons r a✝))
V: Type u

inst✝: Quiver V

a✝¹, b✝¹, c✝, d, a, b, c, x✝: V

p: Path a b

q: Path b c

b✝: V

r: Path c b✝

a✝: b✝ ⟢ x✝

cons (comp (comp p q) r) a✝ = cons (comp p (comp q r)) a✝
V: Type u

inst✝: Quiver V

a✝¹, b✝¹, c✝, d, a, b, c, x✝: V

p: Path a b

q: Path b c

b✝: V

r: Path c b✝

a✝: b✝ ⟢ x✝

comp (comp p q) (cons r a✝) = comp p (comp q (cons r a✝))
V: Type u

inst✝: Quiver V

a✝¹, b✝¹, c✝, d, a, b, c, x✝: V

p: Path a b

q: Path b c

b✝: V

r: 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 q
length_comp (
p: Path a b
p : 
Path: {V : Type ?u.6971} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.6971+1)?u.6972)
Path 
a: V
a 
b: V
b) : βˆ€ {
c: ?m.6987
c} (
q: Path b c
q : 
Path: {V : Type ?u.6990} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.6990+1)?u.6991)
Path 
b: V
b 
c: ?m.6987
c), (
p: Path a b
p.
comp: {V : Type ?u.7006} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q: Path b c
q).
length: {V : Type ?u.7027} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ β„•
length = 
p: Path a b
p.
length: {V : Type ?u.7042} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ β„•
length + 
q: Path b c
q.
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 a
nil => 
rfl: βˆ€ {Ξ± : Sort ?u.7148} {a : Ξ±}, a = a
rfl
  | _, 
cons: {V : Type ?u.7224} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons _ _ => 
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 q
length_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 q
Quiver.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 b
p₁ 
pβ‚‚: Path a b
pβ‚‚ : 
Path: {V : Type ?u.7718} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.7718+1)?u.7719)
Path 
a: V
a 
b: V
b} {
q₁: Path b c
q₁ 
qβ‚‚: Path b c
qβ‚‚ : 
Path: {V : Type ?u.7761} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.7761+1)?u.7762)
Path 
b: V
b 
c: V
c} (
hq: length q₁ = length qβ‚‚
hq : 
q₁: Path b c
q₁.
length: {V : Type ?u.7777} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ β„•
length = 
qβ‚‚: Path b c
qβ‚‚.
length: {V : Type ?u.7795} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ β„•
length) :
    
p₁: Path a b
p₁.
comp: {V : Type ?u.7811} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q₁: Path b c
q₁ = 
pβ‚‚: Path a b
pβ‚‚.
comp: {V : Type ?u.7826} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
qβ‚‚: Path b c
qβ‚‚ ↔ 
p₁: Path a b
p₁ = 
pβ‚‚: Path a b
pβ‚‚ ∧ 
q₁: Path b c
q₁ = 
qβ‚‚: Path b c
qβ‚‚ := 
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

comp p₁ q₁ = comp pβ‚‚ qβ‚‚ ↔ p₁ = pβ‚‚ ∧ q₁ = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

comp p₁ q₁ = comp pβ‚‚ qβ‚‚ ↔ p₁ = pβ‚‚ ∧ q₁ = qβ‚‚
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

p₁ = pβ‚‚ ∧ q₁ = qβ‚‚ β†’ comp p₁ q₁ = comp pβ‚‚ qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁: Path a b

q₁: Path b c

hq: length q₁ = length q₁

intro
comp p₁ q₁ = comp p₁ q₁
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁: Path a b

q₁: Path b c

hq: length q₁ = length q₁

intro
comp p₁ q₁ = comp p₁ q₁
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

p₁ = pβ‚‚ ∧ q₁ = qβ‚‚ β†’ comp p₁ q₁ = comp pβ‚‚ qβ‚‚
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

h: comp p₁ q₁ = comp pβ‚‚ qβ‚‚

p₁ = pβ‚‚ ∧ q₁ = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

comp p₁ q₁ = comp pβ‚‚ qβ‚‚ ↔ p₁ = pβ‚‚ ∧ q₁ = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚βœ: Path b c

hq✝: length q₁ = length qβ‚‚βœ

h✝: comp p₁ q₁ = comp pβ‚‚ qβ‚‚βœ

qβ‚‚: Path b b

hq: length nil = length qβ‚‚

h: comp p₁ nil = comp pβ‚‚ qβ‚‚

nil
p₁ = pβ‚‚ ∧ nil = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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β‚‚

cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

h: comp p₁ q₁ = comp pβ‚‚ qβ‚‚

p₁ = pβ‚‚ ∧ q₁ = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚βœ: Path b c

hq✝: length q₁ = length qβ‚‚βœ

h✝: comp p₁ q₁ = comp pβ‚‚ qβ‚‚βœ

qβ‚‚: Path b b

hq: length nil = length qβ‚‚

h: comp p₁ nil = comp pβ‚‚ qβ‚‚

nil
p₁ = pβ‚‚ ∧ nil = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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β‚‚

cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

h: comp p₁ q₁ = comp pβ‚‚ qβ‚‚

p₁ = pβ‚‚ ∧ q₁ = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq✝: length q₁ = length qβ‚‚

h✝: comp p₁ q₁ = comp pβ‚‚ qβ‚‚

hq: length nil = length nil

h: comp p₁ nil = comp pβ‚‚ nil

nil.nil
p₁ = pβ‚‚ ∧ nil = nil
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚βœ: Path b c

hq✝: length q₁ = length qβ‚‚βœ

h✝: comp p₁ q₁ = comp pβ‚‚ qβ‚‚βœ

b✝: V

qβ‚‚: Path b b✝

fβ‚‚: b✝ ⟢ b

hq: length nil = length (cons qβ‚‚ fβ‚‚)

h: comp p₁ nil = comp pβ‚‚ (cons qβ‚‚ fβ‚‚)

nil.cons
p₁ = pβ‚‚ ∧ nil = cons qβ‚‚ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

comp p₁ q₁ = comp pβ‚‚ qβ‚‚ ↔ p₁ = pβ‚‚ ∧ q₁ = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq✝: length q₁ = length qβ‚‚

h✝: comp p₁ q₁ = comp pβ‚‚ qβ‚‚

hq: length nil = length nil

h: comp p₁ nil = comp pβ‚‚ nil

nil.nil
p₁ = pβ‚‚ ∧ nil = nil
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq✝: length q₁ = length qβ‚‚

h✝: comp p₁ q₁ = comp pβ‚‚ qβ‚‚

hq: length nil = length nil

h: comp p₁ nil = comp pβ‚‚ nil

nil.nil
p₁ = pβ‚‚ ∧ nil = nil
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚βœ: Path b c

hq✝: length q₁ = length qβ‚‚βœ

h✝: comp p₁ q₁ = comp pβ‚‚ qβ‚‚βœ

b✝: V

qβ‚‚: Path b b✝

fβ‚‚: b✝ ⟢ b

hq: length nil = length (cons qβ‚‚ fβ‚‚)

h: comp p₁ nil = comp pβ‚‚ (cons qβ‚‚ fβ‚‚)

nil.cons
p₁ = pβ‚‚ ∧ nil = cons qβ‚‚ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚: Path b c

hq✝: length qβ‚βœ = length qβ‚‚

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚

d₁: V

q₁: Path b d₁

ih: βˆ€ {qβ‚‚ : Path b d₁}, length q₁ = length qβ‚‚ β†’ comp p₁ q₁ = comp pβ‚‚ qβ‚‚ β†’ p₁ = pβ‚‚ ∧ q₁ = qβ‚‚

f₁: d₁ ⟢ b

hq: length (cons q₁ f₁) = length nil

h: comp p₁ (cons q₁ f₁) = comp pβ‚‚ nil

cons.nil
p₁ = pβ‚‚ ∧ cons q₁ f₁ = nil
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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✝: V

qβ‚‚: 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.cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = cons qβ‚‚ fβ‚‚
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

comp p₁ q₁ = comp pβ‚‚ qβ‚‚ ↔ p₁ = pβ‚‚ ∧ q₁ = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚βœ: Path b c

hq✝: length q₁ = length qβ‚‚βœ

h✝: comp p₁ q₁ = comp pβ‚‚ qβ‚‚βœ

b✝: V

qβ‚‚: Path b b✝

fβ‚‚: b✝ ⟢ b

hq: length nil = length (cons qβ‚‚ fβ‚‚)

h: comp p₁ nil = comp pβ‚‚ (cons qβ‚‚ fβ‚‚)

nil.cons
p₁ = pβ‚‚ ∧ nil = cons qβ‚‚ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚βœ: Path b c

hq✝: length q₁ = length qβ‚‚βœ

h✝: comp p₁ q₁ = comp pβ‚‚ qβ‚‚βœ

b✝: V

qβ‚‚: Path b b✝

fβ‚‚: b✝ ⟢ b

hq: length nil = length (cons qβ‚‚ fβ‚‚)

h: comp p₁ nil = comp pβ‚‚ (cons qβ‚‚ fβ‚‚)

nil.cons
p₁ = pβ‚‚ ∧ nil = cons qβ‚‚ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚: Path b c

hq✝: length qβ‚βœ = length qβ‚‚

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚

d₁: V

q₁: Path b d₁

ih: βˆ€ {qβ‚‚ : Path b d₁}, length q₁ = length qβ‚‚ β†’ comp p₁ q₁ = comp pβ‚‚ qβ‚‚ β†’ p₁ = pβ‚‚ ∧ q₁ = qβ‚‚

f₁: d₁ ⟢ b

hq: length (cons q₁ f₁) = length nil

h: comp p₁ (cons q₁ f₁) = comp pβ‚‚ nil

cons.nil
p₁ = pβ‚‚ ∧ cons q₁ f₁ = nil
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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✝: V

qβ‚‚: 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.cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = cons qβ‚‚ fβ‚‚
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

comp p₁ q₁ = comp pβ‚‚ qβ‚‚ ↔ p₁ = pβ‚‚ ∧ q₁ = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚: Path b c

hq✝: length qβ‚βœ = length qβ‚‚

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚

d₁: V

q₁: Path b d₁

ih: βˆ€ {qβ‚‚ : Path b d₁}, length q₁ = length qβ‚‚ β†’ comp p₁ q₁ = comp pβ‚‚ qβ‚‚ β†’ p₁ = pβ‚‚ ∧ q₁ = qβ‚‚

f₁: d₁ ⟢ b

hq: length (cons q₁ f₁) = length nil

h: comp p₁ (cons q₁ f₁) = comp pβ‚‚ nil

cons.nil
p₁ = pβ‚‚ ∧ cons q₁ f₁ = nil
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚: Path b c

hq✝: length qβ‚βœ = length qβ‚‚

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚

d₁: V

q₁: Path b d₁

ih: βˆ€ {qβ‚‚ : Path b d₁}, length q₁ = length qβ‚‚ β†’ comp p₁ q₁ = comp pβ‚‚ qβ‚‚ β†’ p₁ = pβ‚‚ ∧ q₁ = qβ‚‚

f₁: d₁ ⟢ b

hq: length (cons q₁ f₁) = length nil

h: comp p₁ (cons q₁ f₁) = comp pβ‚‚ nil

cons.nil
p₁ = pβ‚‚ ∧ cons q₁ f₁ = nil
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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✝: V

qβ‚‚: 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.cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = cons qβ‚‚ fβ‚‚
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

hq: length q₁ = length qβ‚‚

comp p₁ q₁ = comp pβ‚‚ qβ‚‚ ↔ p₁ = pβ‚‚ ∧ q₁ = qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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✝: V

qβ‚‚: 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.cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = cons qβ‚‚ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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✝: V

qβ‚‚: 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.cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = cons qβ‚‚ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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✝: V

qβ‚‚: 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.cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = cons qβ‚‚ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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✝: V

qβ‚‚: 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.cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = cons qβ‚‚ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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.cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = cons qβ‚‚ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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✝: V

qβ‚‚: 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.cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = cons qβ‚‚ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁: Path a b

qβ‚βœ, qβ‚‚: Path b c

hq✝: length qβ‚βœ = length qβ‚‚

d₁, e₁: V

q₁: 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.intro
p₁ = p₁ ∧ cons q₁ f₁ = cons q₁ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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✝: V

qβ‚‚: 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.cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = cons qβ‚‚ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁: Path a b

qβ‚βœ, qβ‚‚: Path b c

hq✝: length qβ‚βœ = length qβ‚‚

d₁, e₁: V

q₁: 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.intro
p₁ = p₁ ∧ cons q₁ f₁ = cons q₁ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁: Path a b

qβ‚βœ, qβ‚‚: Path b c

hq✝: length qβ‚βœ = length qβ‚‚

d₁, e₁: V

q₁: 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.intro
p₁ = p₁ ∧ cons q₁ fβ‚‚ = cons q₁ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁: Path a b

qβ‚βœ, qβ‚‚: Path b c

hq✝: length qβ‚βœ = length qβ‚‚

d₁, e₁: V

q₁: 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.intro
p₁ = p₁ ∧ cons q₁ fβ‚‚ = cons q₁ fβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

qβ‚βœ, qβ‚‚βœ: Path b c

hq✝: length qβ‚βœ = length qβ‚‚βœ

h✝: comp p₁ qβ‚βœ = comp pβ‚‚ qβ‚‚βœ

d₁, e₁: V

q₁: 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✝: V

qβ‚‚: 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.cons
p₁ = pβ‚‚ ∧ cons q₁ f₁ = cons qβ‚‚ fβ‚‚
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 b
p₁ 
pβ‚‚: Path a b
pβ‚‚ : 
Path: {V : Type ?u.8988} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.8988+1)?u.8989)
Path 
a: V
a 
b: V
b} {
q₁: Path b c
q₁ 
qβ‚‚: Path b c
qβ‚‚ : 
Path: {V : Type ?u.9016} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.9016+1)?u.9017)
Path 
b: V
b 
c: V
c} (
h: length p₁ = length pβ‚‚
h : 
p₁: Path a b
p₁.
length: {V : Type ?u.9032} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ β„•
length = 
pβ‚‚: Path a b
pβ‚‚.
length: {V : Type ?u.9050} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ β„•
length) :
    
p₁: Path a b
p₁.
comp: {V : Type ?u.9066} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q₁: Path b c
q₁ = 
pβ‚‚: Path a b
pβ‚‚.
comp: {V : Type ?u.9081} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
qβ‚‚: Path b c
qβ‚‚ ↔ 
p₁: Path a b
p₁ = 
pβ‚‚: Path a b
pβ‚‚ ∧ 
q₁: Path b c
q₁ = 
qβ‚‚: Path b c
qβ‚‚ :=
  ⟨fun 
h_eq: ?m.9115
h_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 = k
Nat.add_left_cancel <| 
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

h: 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β‚‚
Goals accomplished! πŸ™
).
1: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
1 
h_eq: ?m.9115
h_eq,
   
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

h: length p₁ = length pβ‚‚

p₁ = pβ‚‚ ∧ q₁ = qβ‚‚ β†’ comp p₁ q₁ = comp pβ‚‚ qβ‚‚
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁: Path a b

q₁: Path b c

h: length p₁ = length p₁

intro
comp p₁ q₁ = comp p₁ q₁
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁: Path a b

q₁: Path b c

h: length p₁ = length p₁

intro
comp p₁ q₁ = comp p₁ q₁
V: Type u

inst✝: Quiver V

a, b, c, d: V

p₁, pβ‚‚: Path a b

q₁, qβ‚‚: Path b c

h: length p₁ = length pβ‚‚

p₁ = pβ‚‚ ∧ q₁ = qβ‚‚ β†’ comp p₁ q₁ = comp pβ‚‚ qβ‚‚
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 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 q
comp_injective_left (
q: Path b c
q : 
Path: {V : Type ?u.9798} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.9798+1)?u.9799)
Path 
b: V
b 
c: V
c) : 
Injective: {Ξ± : Sort ?u.9814} β†’ {Ξ² : Sort ?u.9813} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Injective fun 
p: Path a b
p : 
Path: {V : Type ?u.9818} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.9818+1)?u.9819)
Path 
a: V
a 
b: V
b => 
p: Path a b
p.
comp: {V : Type ?u.9832} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q: Path b c
q :=
  fun 
_: ?m.9859
_ 
_: ?m.9862
_ 
h: ?m.9865
h => ((
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 = a
rfl).
1: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
1 
h: ?m.9865
h).
1: βˆ€ {a b : Prop}, a ∧ b β†’ a
1
#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 q
Quiver.Path.comp_injective_left

theorem 
comp_injective_right: βˆ€ (p : Path a b), Injective (comp p)
comp_injective_right (
p: Path a b
p : 
Path: {V : Type ?u.9958} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.9958+1)?u.9959)
Path 
a: V
a 
b: V
b) : 
Injective: {Ξ± : Sort ?u.9974} β†’ {Ξ² : Sort ?u.9973} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Injective (
p: Path a b
p.
comp: {V : Type ?u.10005} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp : 
Path: {V : Type ?u.9979} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.9979+1)?u.9980)
Path 
b: V
b 
c: V
c β†’ 
Path: {V : Type ?u.9992} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.9992+1)?u.9993)
Path 
a: V
a 
c: V
c) :=
  fun 
_: ?m.10033
_ 
_: ?m.10036
_ 
h: ?m.10039
h => ((
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 = a
rfl).
1: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
1 
h: ?m.10039
h).
2: βˆ€ {a b : Prop}, a ∧ b β†’ b
2
#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 b
p₁ 
pβ‚‚: Path a b
pβ‚‚ : 
Path: {V : Type ?u.10143} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.10143+1)?u.10144)
Path 
a: V
a 
b: V
b} {
q: Path b c
q : 
Path: {V : Type ?u.10157} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.10157+1)?u.10158)
Path 
b: V
b 
c: V
c} : 
p₁: Path a b
p₁.
comp: {V : Type ?u.10173} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q: Path b c
q = 
pβ‚‚: Path a b
pβ‚‚.
comp: {V : Type ?u.10194} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q: Path b c
q ↔ 
p₁: Path a b
p₁ = 
pβ‚‚: Path a b
pβ‚‚ :=
  
q: Path b c
q.
comp_injective_left: βˆ€ {V : Type ?u.10215} [inst : Quiver V] {a b c : V} (q : Path b c), Injective fun p => comp p q
comp_injective_left.
eq_iff: βˆ€ {Ξ± : Sort ?u.10230} {Ξ² : Sort ?u.10231} {f : Ξ± β†’ Ξ²}, Injective f β†’ βˆ€ {a b : Ξ±}, f a = f b ↔ a = b
eq_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 b
p : 
Path: {V : Type ?u.10327} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.10327+1)?u.10328)
Path 
a: V
a 
b: V
b} {
q₁: Path b c
q₁ 
qβ‚‚: Path b c
qβ‚‚ : 
Path: {V : Type ?u.10342} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.10342+1)?u.10343)
Path 
b: V
b 
c: V
c} : 
p: Path a b
p.
comp: {V : Type ?u.10372} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q₁: Path b c
q₁ = 
p: Path a b
p.
comp: {V : Type ?u.10393} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
qβ‚‚: Path b c
qβ‚‚ ↔ 
q₁: Path b c
q₁ = 
qβ‚‚: Path b c
qβ‚‚ :=
  
p: Path a b
p.
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 = b
eq_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 V
toList : βˆ€ {
b: V
b : 
V: Type u
V}, 
Path: {V : Type ?u.10528} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.10528+1)?u.10529)
Path 
a: V
a 
b: V
b β†’ 
List: Type ?u.10542 β†’ Type ?u.10542
List 
V: Type u
V
  | _, 
nil: {V : Type ?u.10552} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil => 
[]: List ?m.10585
[]
  | _, @
cons: {V : Type ?u.10587} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
_: Type u
_ _ 
_: V
_ 
c: V
c _ 
p: Path a c
p _ => 
c: V
c :: 
p: Path a c
p.
toList: {b : V} β†’ Path a b β†’ List V
toList
#align quiver.path.to_list 
Quiver.Path.toList: {V : Type u} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ List V
Quiver.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 p
toList_comp (
p: Path a b
p : 
Path: {V : Type ?u.11912} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.11912+1)?u.11913)
Path 
a: V
a 
b: V
b) : βˆ€ {
c: ?m.11928
c} (
q: Path b c
q : 
Path: {V : Type ?u.11931} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.11931+1)?u.11932)
Path 
b: V
b 
c: ?m.11928
c), (
p: Path a b
p.
comp: {V : Type ?u.11947} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q: Path b c
q).
toList: {V : Type ?u.11968} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ List V
toList = 
q: Path b c
q.
toList: {V : Type ?u.11983} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ List V
toList ++ 
p: Path a b
p.
toList: {V : Type ?u.11995} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ List V
toList
  | _, 
nil: {V : Type ?u.12053} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil => 
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d: V

p: Path a b

toList (comp p nil) = toList nil ++ toList p
Goals accomplished! πŸ™

  | _, @
cons: {V : Type ?u.12091} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
_: Type u
_ _ 
_: V
_ 
d: V
d _ 
q: Path b d
q _ => 
Goals accomplished! πŸ™
V: Type u

inst✝: Quiver V

a, b, c, d✝: V

p: Path a b

x✝, d: V

q: Path b d

a✝: d ⟢ x✝

toList (comp p (cons q a✝)) = toList (cons q a✝) ++ toList p
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 p
Quiver.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.12734
b} (
p: Path a b
p : 
Path: {V : Type ?u.12737} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.12737+1)?u.12738)
Path 
a: V
a 
b: ?m.12734
b), 
p: Path a b
p.
toList: {V : Type ?u.12753} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ List V
toList.
Chain: {Ξ± : Type ?u.12765} β†’ (Ξ± β†’ Ξ± β†’ Prop) β†’ Ξ± β†’ List Ξ± β†’ Prop
Chain (fun 
x: ?m.12772
x 
y: ?m.12775
y => 
Nonempty: Sort ?u.12777 β†’ Prop
Nonempty (
y: ?m.12775
y ⟢ 
x: ?m.12772
x)) 
b: ?m.12734
b
  | _, 
nil: {V : Type ?u.12821} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil => 
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 c
cons 
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: V
a 
b: V
b : 
V: Type u
V, 
Subsingleton: Sort ?u.13313 β†’ Prop
Subsingleton (
a: V
a ⟢ 
b: V
b)]

theorem 
toList_injective: βˆ€ (a b : V), Injective toList
toList_injective (
a: V
a : 
V: Type u
V) : βˆ€ 
b: ?m.13371
b, 
Injective: {Ξ± : Sort ?u.13375} β†’ {Ξ² : Sort ?u.13374} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Injective (
toList: {V : Type ?u.13396} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ List V
toList : 
Path: {V : Type ?u.13380} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.13380+1)?u.13381)
Path 
a: V
a 
b: ?m.13371
b β†’ 
List: Type ?u.13394 β†’ Type ?u.13394
List 
V: Type u
V)
  | _, 
nil: {V : Type ?u.13436} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil, 
nil: {V : Type ?u.13443} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil, _ => 
rfl: βˆ€ {Ξ± : Sort ?u.13505} {a : Ξ±}, a = a
rfl
  | _, 
nil: {V : Type ?u.13513} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil, @
cons: {V : Type ?u.13518} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
_: Type u
_ _ 
_: V
_ 
c: V
c _ 
p: Path a c
p 
f: c ⟢ a
f, 
h: toList nil = toList (cons p f)
h => 
Goals accomplished! πŸ™
V: Type u

inst✝¹: Quiver V

a✝, b, c✝, d: V

inst✝: βˆ€ (a b : V), Subsingleton (a ⟢ b)

a, c: V

p: Path a c

f: c ⟢ a

h: toList nil = toList (cons p f)

nil = cons p f
Goals accomplished! πŸ™

  | _, @
cons: {V : Type ?u.13594} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
_: Type u
_ _ 
_: V
_ 
c: V
c _ 
p: Path a c
p 
f: c ⟢ a
f, 
nil: {V : Type ?u.13605} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
nil, 
h: toList (cons p f) = toList nil
h => 
Goals accomplished! πŸ™
V: Type u

inst✝¹: Quiver V

a✝, b, c✝, d: V

inst✝: βˆ€ (a b : V), Subsingleton (a ⟢ b)

a, c: V

p: Path a c

f: c ⟢ a

h: toList (cons p f) = toList nil

cons p f = nil
Goals accomplished! πŸ™

  | _, @
cons: {V : Type ?u.13677} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
_: Type u
_ _ 
_: V
_ 
c: V
c _ 
p: Path a c
p 
f: c ⟢ x✝
f, @
cons: {V : Type ?u.13686} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
cons 
_: Type u
_ _ 
_: V
_ 
t: V
t _ 
C: Path a t
C 
D: t ⟢ x✝
D, 
h: toList (cons p f) = toList (cons C D)
h => 
Goals accomplished! πŸ™
V: Type u

inst✝¹: Quiver V

a✝, b, c✝, d: V

inst✝: βˆ€ (a b : V), Subsingleton (a ⟢ b)

a, x✝, c: V

p: Path a c

f: c ⟢ x✝

t: V

C: Path a t

D: t ⟢ x✝

h: toList (cons p f) = toList (cons C D)

cons p f = cons C D
V: Type u

inst✝¹: Quiver V

a✝, b, c✝, d: V

inst✝: βˆ€ (a b : V), Subsingleton (a ⟢ b)

a, x✝, c: V

p: Path a c

f: c ⟢ x✝

t: V

C: Path a t

D: t ⟢ x✝

h: c = t ∧ toList p = toList C

cons p f = cons C D
V: Type u

inst✝¹: Quiver V

a✝, b, c✝, d: V

inst✝: βˆ€ (a b : V), Subsingleton (a ⟢ b)

a, x✝, c: V

p: Path a c

f: c ⟢ x✝

t: V

C: Path a t

D: t ⟢ x✝

h: toList (cons p f) = toList (cons C D)

cons p f = cons C D
V: Type u

inst✝¹: Quiver V

a✝, b, c✝, d: V

inst✝: βˆ€ (a b : V), Subsingleton (a ⟢ b)

a, x✝, c: V

p: Path a c

f: c ⟢ x✝

C: Path a c

D: c ⟢ x✝

hAC: toList p = toList C

intro
cons p f = cons C D
V: Type u

inst✝¹: Quiver V

a✝, b, c✝, d: V

inst✝: βˆ€ (a b : V), Subsingleton (a ⟢ b)

a, x✝, c: V

p: Path a c

f: c ⟢ x✝

t: V

C: Path a t

D: t ⟢ x✝

h: toList (cons p f) = toList (cons C D)

cons p f = cons C D
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 toList
Quiver.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 = q
toList_inj {
p: Path a b
p 
q: Path a b
q : 
Path: {V : Type ?u.15292} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.15292+1)?u.15293)
Path 
a: V
a 
b: V
b} : 
p: Path a b
p.
toList: {V : Type ?u.15308} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ List V
toList = 
q: Path a b
q.
toList: {V : Type ?u.15326} β†’ [inst : Quiver V] β†’ {a b : V} β†’ Path a b β†’ List V
toList ↔ 
p: Path a b
p = 
q: Path a b
q :=
  (
toList_injective: βˆ€ {V : Type ?u.15344} [inst : Quiver V] [inst_1 : βˆ€ (a b : V), Subsingleton (a ⟢ b)] (a b : V), Injective toList
toList_injective 
_: ?m.15346
_ 
_: ?m.15346
_).
eq_iff: βˆ€ {Ξ± : Sort ?u.15380} {Ξ² : Sort ?u.15381} {f : Ξ± β†’ Ξ²}, Injective f β†’ βˆ€ {a b : Ξ±}, f a = f b ↔ a = b
eq_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 = q
Quiver.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 W
F : 
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: V
a : 
V: Type u₁
V} : βˆ€ {
b: V
b : 
V: Type u₁
V}, 
Path: {V : Type ?u.15565} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.15565+1)?u.15566)
Path 
a: V
a 
b: V
b β†’ 
Path: {V : Type ?u.15579} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.15579+1)?u.15580)
Path (
F: V β₯€q W
F.
obj: {V : Type ?u.15589} β†’ [inst : Quiver V] β†’ {W : Type ?u.15588} β†’ [inst_1 : Quiver W] β†’ V β₯€q W β†’ V β†’ W
obj 
a: V
a) (
F: V β₯€q W
F.
obj: {V : Type ?u.15608} β†’ [inst : Quiver V] β†’ {W : Type ?u.15607} β†’ [inst_1 : Quiver W] β†’ V β₯€q W β†’ V β†’ W
obj 
b: V
b)
  | _, 
Path.nil: {V : Type ?u.15630} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
Path.nil => 
Path.nil: {V : Type ?u.15666} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
Path.nil
  | _, 
Path.cons: {V : Type ?u.15681} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
Path.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 c
Path.cons (
mapPath: {a b : V} β†’ Path a b β†’ Path (F.obj a) (F.obj b)
mapPath 
p: Path a b✝
p) (
F: V β₯€q W
F.
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.nil
mapPath_nil (
a: V
a : 
V: Type u₁
V) : 
F: V β₯€q W
F.
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 a
Path.nil : 
Path: {V : Type ?u.16520} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.16520+1)?u.16521)
Path 
a: V
a 
a: V
a) = 
Path.nil: {V : Type ?u.16553} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
Path.nil :=
  
rfl: βˆ€ {Ξ± : Sort ?u.16611} {a : Ξ±}, a = a
rfl
#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.nil
Prefunctor.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: V
a 
b: V
b 
c: V
c : 
V: Type u₁
V} (
p: Path a b
p : 
Path: {V : Type ?u.16692} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.16692+1)?u.16693)
Path 
a: V
a 
b: V
b) (
e: b ⟢ c
e : 
b: V
b ⟢ 
c: V
c) :
    
F: V β₯€q W
F.
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 c
Path.cons 
p: Path a b
p 
e: b ⟢ c
e) = 
Path.cons: {V : Type ?u.16772} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
Path.cons (
F: V β₯€q W
F.
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 b
p) (
F: V β₯€q W
F.
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 ⟢ c
e) :=
  
rfl: βˆ€ {Ξ± : Sort ?u.16837} {a : Ξ±}, a = a
rfl
#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: V
a 
b: V
b : 
V: Type u₁
V} (
p: Path a b
p : 
Path: {V : Type ?u.16932} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.16932+1)?u.16933)
Path 
a: V
a 
b: V
b) :
    βˆ€ {
c: V
c : 
V: Type u₁
V} (
q: Path b c
q : 
Path: {V : Type ?u.16950} β†’ [inst : Quiver V] β†’ V β†’ V β†’ Sort (max(?u.16950+1)?u.16951)
Path 
b: V
b 
c: V
c), 
F: V β₯€q W
F.
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 b
p.
comp: {V : Type ?u.16990} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp 
q: Path b c
q) = (
F: V β₯€q W
F.
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 b
p).
comp: {V : Type ?u.17034} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ Path b c β†’ Path a c
comp (
F: V β₯€q W
F.
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 c
q)
  | _, 
Path.nil: {V : Type ?u.17091} β†’ [inst : Quiver V] β†’ {a : V} β†’ Path a a
Path.nil => 
rfl: βˆ€ {Ξ± : Sort ?u.17127} {a : Ξ±}, a = a
rfl
  | 
c: V
c, 
Path.cons: {V : Type ?u.17198} β†’ [inst : Quiver V] β†’ {a b c : V} β†’ Path a b β†’ (b ⟢ c) β†’ Path a c
Path.cons 
q: Path b b✝
q 
e: b✝ ⟢ c
e => 
Goals accomplished! πŸ™
V: Type u₁

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F: V β₯€q W

a, b: V

p: Path a b

c, b✝: V

q: Path b b✝

e: b✝ ⟢ c

mapPath F (Path.comp p (Path.cons q e)) = Path.comp (mapPath F p) (mapPath F (Path.cons q e))
V: Type u₁

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F: V β₯€q W

a, b: V

p: Path a b

c, b✝: V

q: Path b b✝

e: b✝ ⟢ c

Path.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 V

W: Type uβ‚‚

inst✝: Quiver W

F: V β₯€q W

a, b: V

p: Path a b

c, b✝: V

q: Path b b✝

e: b✝ ⟢ c

Path.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 V

W: Type uβ‚‚

inst✝: Quiver W

F: V β₯€q W

a, b: V

p: Path a b

c, b✝: V

q: Path b b✝

e: b✝ ⟢ c

mapPath F (Path.comp p (Path.cons q e)) = Path.comp (mapPath F p) (mapPath F (Path.cons q e))
V: Type u₁

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F: V β₯€q W

a, b: V

p: Path a b

c, b✝: V

q: Path b b✝

e: b✝ ⟢ c

Path.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 V

W: Type uβ‚‚

inst✝: Quiver W

F: V β₯€q W

a, b: V

p: Path a b

c, b✝: V

q: Path b b✝

e: b✝ ⟢ c

Path.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: V
a 
b: V
b : 
V: Type u₁
V} (
f: a ⟢ b
f : 
a: V
a ⟢ 
b: V
b) : 
F: V β₯€q W
F.
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 ⟢ b
f.
toPath: {V : Type ?u.17804} β†’ [inst : Quiver V] β†’ {a b : V} β†’ (a ⟢ b) β†’ Path a b
toPath = (
F: V β₯€q W
F.
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 ⟢ b
f).
toPath: {V : Type ?u.17841} β†’ [inst : Quiver V] β†’ {a b : V} β†’ (a ⟢ b) β†’ Path a b
toPath :=
  
rfl: βˆ€ {Ξ± : Sort ?u.17865} {a : Ξ±}, a = a
rfl
#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