Commit 2021-02-09 20:16 296899eb
View on Github →refactor(data/string/basic): simplify proof of to_list_nonempty (#6117)
Co-authors: lean-gptf, Stanislas Polu
This was found by formal-lean-wm-to-tt-m1-m2-v4-c4 when we evaluated it on theorems added to mathlib after we last extracted training data.