Theorem: Loop.rotate_prev (Complexes/Structures/SerreGraph.lean)

State before:
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ prev (next A (Path.cons' A B✝ A e p)) (rotate A (Path.cons' A B✝ A e p)) = A
Tactic:
dsimp [prev, rotate, inv]
State after:
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ next (next A (Path.cons' A B✝ A e p)) (Path.inverse (Path.snoc p e)) = A

State before:
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ next (next A (Path.cons' A B✝ A e p)) (Path.inverse (Path.snoc p e)) = A
Tactic:
rw [Path.inverse_snoc]
State after:
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ next (next A (Path.cons' A B✝ A e p)) (Path.cons (SerreGraph.op e) (Path.inverse p)) = A

State before:
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ next (next A (Path.cons' A B✝ A e p)) (Path.cons (SerreGraph.op e) (Path.inverse p)) = A
Tactic:
rfl
State after:
no goals