Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-15 10:42 0d1d4c95

View on Github →

feat(data/finset/basic): strengthen finset.nonempty.cons_induction (#11452) This change makes it strong enough to be used in three other lemmas.

Estimated changes