We present ZFLean, a Lean 4 library for doing core mathematics inside a model of ZFC with the ergonomics expected of typed Mathlib developments. Building on Mathlib's ZFC model, we contribute a relational calculus for sets with rewriting hints and small predictable tactics, canonical set-theoretic constructions -- Booleans, naturals, integers, sums/option -- and bridges between ZFC objects and Lean's native types enabling mixed set-level/typed proofs. The layer reduces boilerplate for extensional reasoning while remaining compatible with vanilla Mathlib. We discuss library organization and usage patterns that lower the friction of set-theoretic formalization in a dependently typed assistant. We demonstrate typical use of the framework with a case study exercising our constructions and relational calculus through a proof of an isomorphism theorem on curried functions.

翻译：我们提出ZFLean，这是一个Lean 4库，用于在ZFC模型内进行核心数学工作，并具备类型化Mathlib开发所期望的人体工程学特性。基于Mathlib的ZFC模型，我们贡献了一套集合的关系演算，包含重写提示和小型可预测策略、规范的集合论构造（布尔值、自然数、整数、和/选项）以及ZFC对象与Lean原生类型之间的桥梁，支持混合的集合层级/类型化证明。该层在保持与原生Mathlib兼容的同时，减少了外延推理中的样板代码。我们讨论了库的组织和使用模式，这些模式降低了在依赖类型证明助手中进行集合论形式化的摩擦。我们通过一个案例研究展示了该框架的典型用法，该案例利用我们的构造和关系演算，对柯里化函数上的同构定理进行了证明。