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

State before:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
e : A ⟶ B✝
p' : Path B✝ B
⊢ inverse (inverse (cons e p')) = cons e p'
Tactic:
simp [inverse]
State after:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
e : A ⟶ B✝
p' : Path B✝ B
⊢ inverse (inverse p') = p'

State before:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
e : A ⟶ B✝
p' : Path B✝ B
⊢ inverse (inverse p') = p'
Tactic:
apply inverse_inv
State after:
no goals