Leibniz's series for π

theorem Real.tendsto_sum_pi_div_four : Filter.Tendsto (fun (k : ℕ) => Finset.sum (Finset.range k) fun (i : ℕ) => (-1) ^ i / (2 * ↑i + 1)) Filter.atTop (nhds (Real.pi / 4))

Leibniz's series for π. The alternating sum of odd number reciprocals is π / 4, proved by using Abel's limit theorem to extend the Maclaurin series of arctan to 1.