-- Mathlib/Combinatorics/Derangements/Exponential.lean
theorem numDerangements_tendsto_inv_e :
    Tendsto (fun n => (numDerangements n : ℝ) / n.factorial) atTop (𝓝 (Real.exp (-1)))

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑((k + 1).ascFactorial (n - k)) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Tactic:
rw [Nat.ascFactorial_eq_div, add_tsub_cancel_of_le h_le]

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(n.factorial / k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * (↑n.factorial / ↑k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Tactic:
field_simp [Nat.factorial_ne_zero]

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑n.factorial * ↑k.factorial = (-1) ^ k * (↑k.factorial * ↑n.factorial)

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
⊢ Tendsto (fun n => ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))

Tactic:
suffices ∀ n : ℕ, (numDerangements n : ℝ) / n.factorial = s (n + 1) by
  simp_rw [this]
  rw [tendsto_add_atTop_iff_nat
    (f := fun n => ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1]
  apply HasSum.tendsto_sum_nat
  rw [Real.exp_eq_exp_ℝ]
  exact expSeries_div_hasSum_exp ℝ (-1 : ℝ)

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
⊢ ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ↑(numDerangements n) / ↑n.factorial = s (n + 1)

Tactic:
rw [← Int.cast_natCast, numDerangements_sum]

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ↑(∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))) / ↑n.factorial = s (n + 1)

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n => s (n + 1)) atTop (𝓝 (Real.exp (-1)))

Tactic:
rw [tendsto_add_atTop_iff_nat
  (f := fun n => ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1]

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial) atTop (𝓝 (Real.exp (-1)))

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(n.factorial / k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Tactic:
push_cast [Nat.factorial_dvd_factorial h_le]

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * (↑n.factorial / ↑k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Proof state:
case h
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ HasSum (fun i => (-1) ^ i / ↑i.factorial) (Real.exp (-1))

Tactic:
rw [Real.exp_eq_exp_ℝ]

Result:
case h
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ HasSum (fun i => (-1) ^ i / ↑i.factorial) (exp ℝ (-1))

Proof state:
⊢ Tendsto (fun n => ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))

Tactic:
let s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k / k.factorial

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
⊢ Tendsto (fun n => ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ (-1) ^ k * ↑((k + 1).ascFactorial (n - k)) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Tactic:
have h_le : k ≤ n := Finset.mem_range_succ_iff.mp hk

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑((k + 1).ascFactorial (n - k)) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑((i + 1).ascFactorial (n - i)) / ↑n.factorial = s (n + 1)

Tactic:
refine Finset.sum_congr (refl _) ?_

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n - x)) / ↑n.factorial = (-1) ^ x / ↑x.factorial

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ↑(∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))) / ↑n.factorial = s (n + 1)

Tactic:
push_cast

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ (∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n - x))) / ↑n.factorial = s (n + 1)

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n - x)) / ↑n.factorial = (-1) ^ x / ↑x.factorial

Tactic:
intro k hk

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ (-1) ^ k * ↑((k + 1).ascFactorial (n - k)) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
⊢ ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)

Tactic:
intro n

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ↑(numDerangements n) / ↑n.factorial = s (n + 1)

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ (∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n - x))) / ↑n.factorial = s (n + 1)

Tactic:
rw [Finset.sum_div]

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑((i + 1).ascFactorial (n - i)) / ↑n.factorial = s (n + 1)

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n => ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))

Tactic:
simp_rw [this]

Result:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n => s (n + 1)) atTop (𝓝 (Real.exp (-1)))

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑n.factorial * ↑k.factorial = (-1) ^ k * (↑k.factorial * ↑n.factorial)

Tactic:
ring

Result:
no goals

Proof state:
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial) atTop (𝓝 (Real.exp (-1)))

Tactic:
apply HasSum.tendsto_sum_nat

Result:
case h
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ HasSum (fun i => (-1) ^ i / ↑i.factorial) (Real.exp (-1))

Proof state:
case h
s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ HasSum (fun i => (-1) ^ i / ↑i.factorial) (exp ℝ (-1))

Tactic:
exact expSeries_div_hasSum_exp ℝ (-1 : ℝ)

Result:
no goals