Theorem: Fin.perm_fin_two_apply_apply (Controlbits/PermFintwo.lean)

State before:
q : Fin 2
π : Equiv.Perm (Fin 2)
⊢ π (π q) = q
Tactic:
rw [← Equiv.Perm.mul_apply, perm_fin_two_mul_self, Equiv.Perm.one_apply]
State after:
no goals