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

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

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

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

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

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (q : Path C✝ C), append (append a✝ q) r = append a✝ (append q r)
q : Path C✝ C
⊢ append (append (cons a✝¹ a✝) q) r = append (cons a✝¹ a✝) (append q r)
Tactic:
case cons ih => simp [append]; apply ih
State after:
no goals

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (q : Path C✝ C), append (append a✝ q) r = append a✝ (append q r)
q : Path C✝ C
⊢ append (append (cons a✝¹ a✝) q) r = append (cons a✝¹ a✝) (append q r)
Tactic:
simp [append]
State after:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (q : Path C✝ C), append (append a✝ q) r = append a✝ (append q r)
q : Path C✝ C
⊢ append (append a✝ q) r = append a✝ (append q r)

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (q : Path C✝ C), append (append a✝ q) r = append a✝ (append q r)
q : Path C✝ C
⊢ append (append a✝ q) r = append a✝ (append q r)
Tactic:
apply ih
State after:
no goals