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₂
refine' ⟨fun h => _, by rintro ⟨rfl, rfl⟩; rfl⟩
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

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₂

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

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₂
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₂
induction' q₁ with d₁ e₁ q₁ f₁ ih <;> obtain _ | ⟨q₂, f₂⟩ := q₂
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₁
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₂
rintro ⟨rfl, rfl⟩
no goals
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₁
rfl
no goals
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
exact ⟨h, rfl⟩
no goals
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₂
cases hq
no goals
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
cases hq
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₂
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₂
simp only [comp_cons, cons.injEq] at h
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₂
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₂
obtain rfl := h.1
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₂
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₂
obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq
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₂
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₂
rw [h.2.2.eq]
no goals
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₂
exact ⟨rfl, rfl⟩