[GOAL]
⊢ Tendsto (fun n => ↑(numDerangements n) / ↑(Nat.factorial n)) atTop (𝓝 (Real.exp (-1)))
[PROOFSTEP]
let s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1 : ℝ) ^ k / k.factorial
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
⊢ Tendsto (fun n => ↑(numDerangements n) / ↑(Nat.factorial n)) atTop (𝓝 (Real.exp (-1)))
[PROOFSTEP]
suffices ∀ n : ℕ, (numDerangements n : ℝ) / n.factorial = s (n + 1)
  by
  simp_rw [this]
    -- shift the function by 1, and then use the fact that the partial sums
        -- converge to the infinite sum
  rw [tendsto_add_atTop_iff_nat (f := fun n => ∑ k in Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1]
  apply HasSum.tendsto_sum_nat
  rw [Real.exp_eq_exp_ℝ]
  exact expSeries_div_hasSum_exp ℝ (-1 : ℝ)
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
⊢ Tendsto (fun n => ↑(numDerangements n) / ↑(Nat.factorial n)) atTop (𝓝 (Real.exp (-1)))
[PROOFSTEP]
simp_rw [this]
  -- shift the function by 1, and then use the fact that the partial sums
      -- converge to the infinite sum
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
⊢ Tendsto (fun n => ∑ k in Finset.range (n + 1), (-1) ^ k / ↑(Nat.factorial k)) atTop (𝓝 (Real.exp (-1)))
[PROOFSTEP]
rw [tendsto_add_atTop_iff_nat (f := fun n => ∑ k in Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1]
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
⊢ Tendsto (fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)) atTop (𝓝 (Real.exp (-1)))
[PROOFSTEP]
apply HasSum.tendsto_sum_nat
[GOAL]
case h
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
⊢ HasSum (fun i => (-1) ^ i / ↑(Nat.factorial i)) (Real.exp (-1))
[PROOFSTEP]
rw [Real.exp_eq_exp_ℝ]
[GOAL]
case h
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
⊢ HasSum (fun i => (-1) ^ i / ↑(Nat.factorial i)) (exp ℝ (-1))
[PROOFSTEP]
exact expSeries_div_hasSum_exp ℝ (-1 : ℝ)
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
⊢ ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
[PROOFSTEP]
intro n
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n : ℕ
⊢ ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
[PROOFSTEP]
rw [← Int.cast_ofNat, numDerangements_sum]
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n : ℕ
⊢ ↑(∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))) / ↑(Nat.factorial n) = s (n + 1)
[PROOFSTEP]
push_cast
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n : ℕ
⊢ (∑ x in Finset.range (n + 1), (-1) ^ x * ↑(Nat.ascFactorial x (n - x))) / ↑(Nat.factorial n) =
    ∑ k in Finset.range (n + 1), (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
rw [Finset.sum_div]
  -- get down to individual terms
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n : ℕ
⊢ ∑ x in Finset.range (n + 1), (-1) ^ x * ↑(Nat.ascFactorial x (n - x)) / ↑(Nat.factorial n) =
    ∑ k in Finset.range (n + 1), (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
refine' Finset.sum_congr (refl _) _
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      (-1) ^ x * ↑(Nat.ascFactorial x (n - x)) / ↑(Nat.factorial n) = (-1) ^ x / ↑(Nat.factorial x)
[PROOFSTEP]
intro k hk
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ (-1) ^ k * ↑(Nat.ascFactorial k (n - k)) / ↑(Nat.factorial n) = (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
have h_le : k ≤ n := Finset.mem_range_succ_iff.mp hk
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(Nat.ascFactorial k (n - k)) / ↑(Nat.factorial n) = (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
rw [Nat.ascFactorial_eq_div, add_tsub_cancel_of_le h_le]
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(Nat.factorial n / Nat.factorial k) / ↑(Nat.factorial n) = (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
push_cast [Nat.factorial_dvd_factorial h_le]
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * (↑(Nat.factorial n) / ↑(Nat.factorial k)) / ↑(Nat.factorial n) = (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
field_simp [Nat.factorial_ne_zero]
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(Nat.factorial n) * ↑(Nat.factorial k) = (-1) ^ k * (↑(Nat.factorial k) * ↑(Nat.factorial n))
[PROOFSTEP]
ring
