Theorem: Path.nil_length (Complexes/Structures/Quiver.lean)

State before:
V : Sort u_1
inst✝ : Quiver V
A✝ B C D A B✝ : V
a✝ : A ⟶ B✝
p : Path B✝ A
⊢ length (cons a✝ p) = Nat.zero ↔ cons a✝ p = nil' A
Tactic:
apply Iff.intro <;> (intro; simp [length] at *)
State after:
no goals

State before:
case mpr
V : Sort u_1
inst✝ : Quiver V
A✝ B C D A B✝ : V
a✝ : A ⟶ B✝
p : Path B✝ A
⊢ cons a✝ p = nil' A → length (cons a✝ p) = Nat.zero
Tactic:
intro
State after:
case mpr
V : Sort u_1
inst✝ : Quiver V
A✝ B C D A B✝ : V
a✝¹ : A ⟶ B✝
p : Path B✝ A
a✝ : cons a✝¹ p = nil' A
⊢ length (cons a✝¹ p) = Nat.zero

State before:
case mpr
V : Sort u_1
inst✝ : Quiver V
A✝ B C D A B✝ : V
a✝¹ : A ⟶ B✝
p : Path B✝ A
a✝ : cons a✝¹ p = nil' A
⊢ length (cons a✝¹ p) = Nat.zero
Tactic:
simp [length] at *
State after:
no goals