Theorem: Path.first_eq_inv_last (Complexes/Structures/SerreGraph.lean)

State before:
V : Sort u_1
G : SerreGraph V
A B C : V
p : Path A B
x✝¹ x✝ B✝ : V
e : x✝¹ ⟶ B✝
p' : Path B✝ x✝
⊢ first (cons e p') = last (inverse (cons e p'))
Tactic:
simp [first, last, inverse, snoc, last_snoc]
State after:
no goals