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



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



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


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


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