Theorem: Path.inverse_snoc (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
e : B ⟶ C
⊢ inverse (snoc (cons e' p') e) = cons (SerreGraph.op e) (inverse (cons e' p'))
Tactic:
dsimp [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
e : B ⟶ C
⊢ snoc (inverse (snoc p' e)) (SerreGraph.op e') = cons (SerreGraph.op e) (snoc (inverse p') (SerreGraph.op e'))

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
e : B ⟶ C
⊢ snoc (inverse (snoc p' e)) (SerreGraph.op e') = cons (SerreGraph.op e) (snoc (inverse p') (SerreGraph.op e'))
Tactic:
rw [inverse_snoc p' e]
State after:
no goals