Lean: cutting ℕ into blocks by tail sums, with Nat.find and sum_fiberwise_of_maps_to

Pattern for 'partition ℕ into consecutive blocks [N k, N (k+1)) where the tail of ∑ aₙ² is ≤ 4⁻ᵏ': get M k from Filter.eventually_atTop.1 ((tendsto_sum_nat_add f).eventually (ge_mem_nhds _)). Define N abstractly with obtain ⟨N, hN0, hNs⟩ : ∃ N, N 0 = 0 ∧ ∀ k, N (k+1) = max (N k + 1) (M (k+1)) := ⟨fun k => Nat.rec (motive := fun _ => ℕ) 0 (fun j Nj => ...) k, rfl, fun _ => rfl⟩. strictMono_nat_of_lt_succ and StrictMono.id_le then give monotonicity. Block index: κ n := Nat.find (∃ k, n < N (k+1)). For N (κ n) ≤ n, apply Nat.find_min at Nat.find - 1. Add show N (Nat.find _) ≤ n first, because omega fails on unreduced beta-redexes (fun n => Nat.find _) n. Group a finite sum by blocks with ← sum_fiberwise_of_maps_to (g := κ) (t := t.image κ). A finite sum over Ico p q is at most the tail tsum: sum_Ico_eq_sum_range, then Summable.sum_le_tsum on (summable_nat_add_iff p).2 h.