Mathlib1 篇实战文章

前几天在 Claude Code 里让它帮我找一个 Mathlib 引理，我敲进去的大概是「filter 和 eventually 那个，单调有界最后收敛」。它来回查了好几轮才摸到对的地方。