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

State before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝ C✝ D A B C : V
q : Path A C
⊢ length (append nil q) = length nil + length q
Tactic:
rw [Nat.add_comm]
State after:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝ C✝ D A B C : V
q : Path A C
⊢ length (append nil q) = length q + length nil

State before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝ C✝ D A B C : V
q : Path A C
⊢ length (append nil q) = length q + length nil
Tactic:
rfl
State after:
no goals

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
q : Path B C
⊢ length (append (cons a✝ p') q) = length (cons a✝ p') + length q
Tactic:
dsimp [append, 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
q : Path B C
⊢ Nat.succ (length (append p' q)) = Nat.succ (length p') + length q

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
q : Path B C
⊢ Nat.succ (length (append p' q)) = Nat.succ (length p') + length q
Tactic:
rw [Nat.succ_add]
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
q : Path B C
⊢ Nat.succ (length (append p' q)) = Nat.succ (length p' + length q)

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
q : Path B C
⊢ Nat.succ (length (append p' q)) = Nat.succ (length p' + length q)
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
q : Path B C
⊢ length (append p' q) = length p' + length q

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
q : Path B C
⊢ length (append p' q) = length p' + length q
Tactic:
apply length_append
State after:
no goals