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

State before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ length (snoc (cons a✝ p') e) = Nat.succ (length (cons a✝ p'))
Tactic:
rw [snoc_cons]
State after:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ length (cons a✝ (snoc p' e)) = Nat.succ (length (cons a✝ p'))

State before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ length (cons a✝ (snoc p' e)) = Nat.succ (length (cons a✝ p'))
Tactic:
dsimp only [length]
State after:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ Nat.succ (length (snoc p' e)) = Nat.succ (Nat.succ (length p'))

State before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ Nat.succ (length (snoc p' e)) = Nat.succ (Nat.succ (length p'))
Tactic:
apply congrArg
State after:
case h
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ length (snoc p' e) = length p' + 1

State before:
case h
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ length (snoc p' e) = length p' + 1
Tactic:
apply snoc_length
State after:
no goals