case zero
α : Type ?u.22310
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ↑(numDerangements Nat.zero) = ∑ k in Finset.range (Nat.zero + 1), (-1) ^ k * ↑(Nat.ascFactorial k (Nat.zero - k))

case succ
α : Type ?u.22310
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
⊢ ↑(numDerangements (Nat.succ n)) =
    ∑ k in Finset.range (Nat.succ n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (Nat.succ n - k))
α : Type ?u.22310
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
induction' n with n hn
case succ
α : Type ?u.22310
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
case succ
α : Type ?u.22310
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
⊢ ↑(numDerangements (Nat.succ n)) =
    ∑ k in Finset.range (Nat.succ n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (Nat.succ n - k))
rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self,
  Nat.ascFactorial_zero, Int.ofNat_one, mul_one, pow_succ, neg_one_mul, sub_eq_add_neg,
  add_left_inj, Finset.sum_congr rfl]
case succ
α : Type ?u.22310
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
case succ
α : Type ?u.22310
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
intro x hx
case succ
α : Type ?u.22310
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
⊢ (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
case succ
α : Type ?u.22310
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
no goals
case succ
α : Type ?u.22310
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
⊢ (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_tsub_cancel_of_le h_le, Int.ofNat_mul,
  Int.ofNat_succ, mul_left_comm]
no goals
case zero
α : Type ?u.22310
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ↑(numDerangements Nat.zero) = ∑ k in Finset.range (Nat.zero + 1), (-1) ^ k * ↑(Nat.ascFactorial k (Nat.zero - k))
rfl