Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-16 10:16 fe7d5738

View on Github →

refactor(data/set/enumerate): proof enumeration_inj using wlog

Estimated changes

Modified data/set/enumerate.lean

modified theorem set.enumerate_inj