-- Mathlib/Combinatorics/Quiver/Path.lean
theorem comp_inj {p₁ p₂ : Path a b} {q₁ q₂ : Path b c} (hq : q₁.length = q₂.length) :
    p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂

Proof state:
case nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₂ : Path b b
hq : nil.length = q₂.length
h : p₁.comp nil = p₂.comp q₂
⊢ p₁ = p₂ ∧ nil = q₂

Tactic:
rcases q₂ with _ | ⟨q₂, f₂⟩

Result:
case nil.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
hq : nil.length = nil.length
h : p₁.comp nil = p₂.comp nil
⊢ p₁ = p₂ ∧ nil = nil

case nil.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ b
hq : nil.length = (q₂.cons f₂).length
h : p₁.comp nil = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ nil = q₂.cons f₂

Proof state:
case cons.cons.intro
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ f₂ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₁.comp q₂ → p₁ = p₁ ∧ q₁ = q₂
hq : (q₁.cons f₁).length = (q₁.cons f₂).length
h : b✝ = b✝ ∧ HEq (p₁.comp q₁) (p₁.comp q₁) ∧ HEq f₁ f₂
⊢ p₁ = p₁ ∧ q₁.cons f₂ = q₁.cons f₂

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

Proof state:
case intro
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
q₁ : Path b c
hq : q₁.length = q₁.length
⊢ p₁.comp q₁ = p₁.comp q₁

Tactic:
rfl

Result:
no goals

Proof state:
case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Tactic:
simp only [comp_cons, cons.injEq] at h

Result:
case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : b✝¹ = b✝ ∧ HEq (p₁.comp q₁) (p₂.comp q₂) ∧ HEq f₁ f₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Proof state:
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : q₁.length = q₂.length
⊢ p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂

Tactic:
refine ⟨fun h => ?_, by rintro ⟨rfl, rfl⟩; rfl⟩

Result:
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : q₁.length = q₂.length
h : p₁.comp q₁ = p₂.comp q₂
⊢ p₁ = p₂ ∧ q₁ = q₂

Proof state:
case nil.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
hq : nil.length = nil.length
h : p₁.comp nil = p₂.comp nil
⊢ p₁ = p₂ ∧ nil = nil

Tactic:
exact ⟨h, rfl⟩

Result:
no goals

Proof state:
case cons.cons.intro
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ f₂ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₁.comp q₂ → p₁ = p₁ ∧ q₁ = q₂
hq : (q₁.cons f₁).length = (q₁.cons f₂).length
h : b✝ = b✝ ∧ HEq (p₁.comp q₁) (p₁.comp q₁) ∧ HEq f₁ f₂
⊢ p₁ = p₁ ∧ q₁.cons f₁ = q₁.cons f₂

Tactic:
rw [h.2.2.eq]

Result:
case cons.cons.intro
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ f₂ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₁.comp q₂ → p₁ = p₁ ∧ q₁ = q₂
hq : (q₁.cons f₁).length = (q₁.cons f₂).length
h : b✝ = b✝ ∧ HEq (p₁.comp q₁) (p₁.comp q₁) ∧ HEq f₁ f₂
⊢ p₁ = p₁ ∧ q₁.cons f₂ = q₁.cons f₂

Proof state:
case nil.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ b
hq : nil.length = (q₂.cons f₂).length
h : p₁.comp nil = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ nil = q₂.cons f₂

Tactic:
cases hq

Result:
no goals

Proof state:
case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : b✝ = b✝ ∧ HEq (p₁.comp q₁) (p₂.comp q₂) ∧ HEq f₁ f₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Tactic:
obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq

Result:
case cons.cons.intro
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ f₂ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₁.comp q₂ → p₁ = p₁ ∧ q₁ = q₂
hq : (q₁.cons f₁).length = (q₁.cons f₂).length
h : b✝ = b✝ ∧ HEq (p₁.comp q₁) (p₁.comp q₁) ∧ HEq f₁ f₂
⊢ p₁ = p₁ ∧ q₁.cons f₁ = q₁.cons f₂

Proof state:
case cons.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₁ : Path b b✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
f₁ : b✝ ⟶ b
hq : (q₁.cons f₁).length = nil.length
h : p₁.comp (q₁.cons f₁) = p₂.comp nil
⊢ p₁ = p₂ ∧ q₁.cons f₁ = nil

Tactic:
cases hq

Result:
no goals

Proof state:
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : q₁.length = q₂.length
⊢ p₁ = p₂ ∧ q₁ = q₂ → p₁.comp q₁ = p₂.comp q₂

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case intro
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
q₁ : Path b c
hq : q₁.length = q₁.length
⊢ p₁.comp q₁ = p₁.comp q₁

Proof state:
case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : b✝¹ = b✝ ∧ HEq (p₁.comp q₁) (p₂.comp q₂) ∧ HEq f₁ f₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Tactic:
obtain rfl := h.1

Result:
case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : b✝ = b✝ ∧ HEq (p₁.comp q₁) (p₂.comp q₂) ∧ HEq f₁ f₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Proof state:
case cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
q₂ : Path b c✝
hq : (q₁.cons f₁).length = q₂.length
h : p₁.comp (q₁.cons f₁) = p₂.comp q₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂

Tactic:
rcases q₂ with _ | ⟨q₂, f₂⟩

Result:
case cons.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₁ : Path b b✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
f₁ : b✝ ⟶ b
hq : (q₁.cons f₁).length = nil.length
h : p₁.comp (q₁.cons f₁) = p₂.comp nil
⊢ p₁ = p₂ ∧ q₁.cons f₁ = nil

case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂