case zero

⊢ ↑sign (finRotate (Nat.zero + 1)) = (-1) ^ Nat.zero

case succ
n : ℕ
ih : ↑sign (finRotate (n + 1)) = (-1) ^ n
⊢ ↑sign (finRotate (Nat.succ n + 1)) = (-1) ^ Nat.succ n
n : ℕ
⊢ ↑sign (finRotate (n + 1)) = (-1) ^ n
induction' n with n ih
no goals
case zero

⊢ ↑sign (finRotate (Nat.zero + 1)) = (-1) ^ Nat.zero
simp
case succ
n : ℕ
ih : ↑sign (finRotate (n + 1)) = (-1) ^ n
⊢ ↑sign (↑decomposeFin.symm (1, finRotate (n + 1))) = (-1) ^ Nat.succ n
case succ
n : ℕ
ih : ↑sign (finRotate (n + 1)) = (-1) ^ n
⊢ ↑sign (finRotate (Nat.succ n + 1)) = (-1) ^ Nat.succ n
rw [finRotate_succ_eq_decomposeFin]
no goals
case succ
n : ℕ
ih : ↑sign (finRotate (n + 1)) = (-1) ^ n
⊢ ↑sign (↑decomposeFin.symm (1, finRotate (n + 1))) = (-1) ^ Nat.succ n
simp [ih, pow_succ]