Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-24 15:00 75608aff

View on Github →

chore(data/set/basic): Golf #18356 (#18491) and fix a docstring that was made a comment

Estimated changes