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

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ : V
a✝ : x✝³ ⟶ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (snoc (cons' x✝³ x✝² x✝² a✝ nil) x✝) = x✝²
Tactic:
rw [snoc_cons]
State after:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ : V
a✝ : x✝³ ⟶ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (cons a✝ (snoc nil x✝)) = x✝²

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ : V
a✝ : x✝³ ⟶ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (cons a✝ (snoc nil x✝)) = x✝²
Tactic:
rfl
State after:
no goals

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ B✝¹ : V
a✝² : x✝³ ⟶ B✝¹
B✝ : V
a✝¹ : B✝¹ ⟶ B✝
a✝ : Path B✝ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (snoc (cons' x✝³ B✝¹ x✝² a✝² (cons a✝¹ a✝)) x✝) = x✝²
Tactic:
rw [snoc_cons, snoc, last, ← snoc_cons]
State after:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ B✝¹ : V
a✝² : x✝³ ⟶ B✝¹
B✝ : V
a✝¹ : B✝¹ ⟶ B✝
a✝ : Path B✝ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (snoc (cons a✝¹ a✝) x✝) = x✝²

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ B✝¹ : V
a✝² : x✝³ ⟶ B✝¹
B✝ : V
a✝¹ : B✝¹ ⟶ B✝
a✝ : Path B✝ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (snoc (cons a✝¹ a✝) x✝) = x✝²
Tactic:
apply last_snoc
State after:
no goals