case zero
α : Type ?u.11655
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ↑(numDerangements (Nat.zero + 1)) = (↑Nat.zero + 1) * ↑(numDerangements Nat.zero) - (-1) ^ Nat.zero

case succ
α : Type ?u.11655
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ ↑(numDerangements (Nat.succ n + 1)) = (↑(Nat.succ n) + 1) * ↑(numDerangements (Nat.succ n)) - (-1) ^ Nat.succ n
α : Type ?u.11655
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
induction' n with n hn
no goals
case zero
α : Type ?u.11655
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ↑(numDerangements (Nat.zero + 1)) = (↑Nat.zero + 1) * ↑(numDerangements Nat.zero) - (-1) ^ Nat.zero
rfl
case succ
α : Type ?u.11655
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ (↑n + 1) * (↑(numDerangements n) + ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n)) =
    (↑n + 1 + 1) * ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n) - -1 * (-1) ^ n
case succ
α : Type ?u.11655
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ ↑(numDerangements (Nat.succ n + 1)) = (↑(Nat.succ n) + 1) * ↑(numDerangements (Nat.succ n)) - (-1) ^ Nat.succ n
simp only [numDerangements_add_two, hn, pow_succ, Int.ofNat_mul, Int.ofNat_add, Int.ofNat_succ]
no goals
case succ
α : Type ?u.11655
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ (↑n + 1) * (↑(numDerangements n) + ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n)) =
    (↑n + 1 + 1) * ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n) - -1 * (-1) ^ n
ring