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

State before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (rotate A (inv l)) (inv (rotate' A l))
Tactic:
rw [rotate', inv_inv]
State after:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (rotate A (inv l)) (rotate A (inv l))

State before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (rotate A (inv l)) (rotate A (inv l))
Tactic:
exact .refl _
State after:
no goals