In the following file we prove that equivalence relations and partitions are the same thing by constructing an isomorphism between the type of equivalence relations and the type of partitions.
There are few Challenges in the file below each involving filling in for
sorrys in the
Lean code. Once all these challenges are accomplished, you have established the above-mentioned isomorphism.