A collection of set theorems and custom tactics in lean 4.

Useful for:

• Learning How Set Theory Works in Lean 4
• Formalization of Logic Puzzles using Set Theory

The following guide uses mathematics_in_lean as an example but is relevant to any project in general:

https://leanprover-community.github.io/install/project.html#working-on-an-existing-project