[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
e : b ⟶ a
h : nil = cons p e
⊢ False
[PROOFSTEP]
injection h
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
e : b ⟶ a
h : cons p e = nil
⊢ False
[PROOFSTEP]
injection h
[GOAL]
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
[PROOFSTEP]
injection h
[GOAL]
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'
[PROOFSTEP]
injection h
[GOAL]
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'
[PROOFSTEP]
injection h
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
hzero : length p = 0
⊢ a = b
[PROOFSTEP]
cases p
[GOAL]
case nil
V : Type u
inst✝ : Quiver V
a c d : V
hzero : length nil = 0
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
case cons
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
⊢ a = b
[PROOFSTEP]
cases Nat.succ_ne_zero _ hzero
[GOAL]
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✝
[PROOFSTEP]
rw [comp_cons, nil_comp p]
[GOAL]
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✝))
[PROOFSTEP]
rw [comp_cons, comp_cons, comp_cons, comp_assoc p q r]
[GOAL]
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₂
[PROOFSTEP]
refine' ⟨fun h => _, by rintro ⟨rfl, rfl⟩; rfl⟩
[GOAL]
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₂
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ : Path a b
q₁ : Path b c
hq : length q₁ = length q₁
⊢ comp p₁ q₁ = comp p₁ q₁
[PROOFSTEP]
rfl
[GOAL]
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₂
[PROOFSTEP]
induction' q₁ with d₁ e₁ q₁ f₁ ih
[GOAL]
case 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₂✝
q₂ : Path b b
hq : length nil = length q₂
h : comp p₁ nil = comp p₂ q₂
⊢ p₁ = p₂ ∧ nil = q₂
[PROOFSTEP]
obtain _ | ⟨q₂, f₂⟩ := q₂
[GOAL]
case cons
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₂
⊢ p₁ = p₂ ∧ cons q₁ f₁ = q₂
[PROOFSTEP]
obtain _ | ⟨q₂, f₂⟩ := q₂
[GOAL]
case 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
⊢ p₁ = p₂ ∧ nil = nil
[PROOFSTEP]
exact ⟨h, rfl⟩
[GOAL]
case nil.cons
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₂)
⊢ p₁ = p₂ ∧ nil = cons q₂ f₂
[PROOFSTEP]
cases hq
[GOAL]
case cons.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
⊢ p₁ = p₂ ∧ cons q₁ f₁ = nil
[PROOFSTEP]
cases hq
[GOAL]
case cons.cons
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₂)
⊢ p₁ = p₂ ∧ cons q₁ f₁ = cons q₂ f₂
[PROOFSTEP]
simp only [comp_cons, cons.injEq] at h 
[GOAL]
case cons.cons
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₂
⊢ p₁ = p₂ ∧ cons q₁ f₁ = cons q₂ f₂
[PROOFSTEP]
obtain rfl := h.1
[GOAL]
case cons.cons
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₂
⊢ p₁ = p₂ ∧ cons q₁ f₁ = cons q₂ f₂
[PROOFSTEP]
obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq
[GOAL]
case cons.cons.intro
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₂
⊢ p₁ = p₁ ∧ cons q₁ f₁ = cons q₁ f₂
[PROOFSTEP]
rw [h.2.2.eq]
[GOAL]
case cons.cons.intro
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₂
⊢ p₁ = p₁ ∧ cons q₁ f₂ = cons q₁ f₂
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
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.8816 h h_eq + length q₁ = ?m.8816 h h_eq + length q₂
[PROOFSTEP]
simpa [h] using congr_arg length h_eq
[GOAL]
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₂
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ : Path a b
q₁ : Path b c
h : length p₁ = length p₁
⊢ comp p₁ q₁ = comp p₁ q₁
[PROOFSTEP]
rfl
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
⊢ toList (comp p nil) = toList nil ++ toList p
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
simp [toList_comp]
[GOAL]
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
[PROOFSTEP]
cases h
[GOAL]
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
[PROOFSTEP]
cases h
[GOAL]
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
[PROOFSTEP]
simp only [toList, List.cons.injEq] at h 
[GOAL]
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
[PROOFSTEP]
obtain ⟨rfl, hAC⟩ := h
[GOAL]
case intro
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
⊢ cons p f = cons C D
[PROOFSTEP]
simp [toList_injective _ _ hAC]
[GOAL]
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))
[PROOFSTEP]
dsimp
[GOAL]
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)
[PROOFSTEP]
rw [mapPath_comp p q]
