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

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

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

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

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

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

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

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