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

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

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

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

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

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ append (cons a✝¹ a✝) nil = cons a✝¹ a✝
Tactic:
case cons =>
  simp only [append]
  apply congrArg
  assumption
State after:
no goals

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ append (cons a✝¹ a✝) nil = cons a✝¹ a✝
Tactic:
simp only [append]
State after:
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ cons a✝¹ (append a✝ nil) = cons a✝¹ a✝

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ cons a✝¹ (append a✝ nil) = cons a✝¹ a✝
Tactic:
apply congrArg
State after:
case h
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ append a✝ nil = a✝

State before:
case h
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ append a✝ nil = a✝
Tactic:
assumption
State after:
no goals