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

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p : Path A B
p' : Path B C
e : C ⟶ D
⊢ append p (snoc p' e) = snoc (append p p') e
Tactic:
induction p
State after:
case nil
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ : V
p' : Path A✝ C
⊢ append nil (snoc p' e) = snoc (append nil p') e

case cons
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : ∀ (p' : Path C✝ C), append a✝ (snoc p' e) = snoc (append a✝ p') e
p' : Path C✝ C
⊢ append (cons a✝¹ a✝) (snoc p' e) = snoc (append (cons a✝¹ a✝) p') e

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ : V
p' : Path A✝ C
⊢ append nil (snoc p' e) = snoc (append nil p') e
Tactic:
case nil => rfl
State after:
no goals

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ : V
p' : Path A✝ C
⊢ append nil (snoc p' e) = snoc (append nil p') e
Tactic:
rfl
State after:
no goals

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (p' : Path C✝ C), append a✝ (snoc p' e) = snoc (append a✝ p') e
p' : Path C✝ C
⊢ append (cons a✝¹ a✝) (snoc p' e) = snoc (append (cons a✝¹ a✝) p') e
Tactic:
case cons ih => simp [append, ih p', snoc_cons]
State after:
no goals

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (p' : Path C✝ C), append a✝ (snoc p' e) = snoc (append a✝ p') e
p' : Path C✝ C
⊢ append (cons a✝¹ a✝) (snoc p' e) = snoc (append (cons a✝¹ a✝) p') e
Tactic:
simp [append, ih p', snoc_cons]
State after:
no goals