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

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