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 [← inv_rotate_inv A l.inv]
State after:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (inv (rotate A (inv (inv l)))) (inv (rotate A l))

State before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (inv (rotate A (inv (inv l)))) (inv (rotate A l))
Tactic:
congr 2 <;> rw [inv_inv]
State after:
no goals