Theorem: Loop.rotate'_next (Complexes/Structures/SerreGraph.lean)

State before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ next (prev A l) (rotate' A l) = A
Tactic:
show prev _ (rotate _ l.inv) = A
State after:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ prev (next A (inv l)) (rotate A (inv l)) = A

State before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ prev (next A (inv l)) (rotate A (inv l)) = A
Tactic:
simp
State after:
no goals