no goals
α : Type ?u.27282
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ finRotate (bit1 n) ∈ alternatingGroup (Fin (bit1 n))
rw [mem_alternatingGroup, bit1, sign_finRotate, pow_bit0', Int.units_mul_self, one_pow]