mathlib

ec8f2ac8 - refactor(data/ordmap/ordset): simpler proof of `not_le_delta` (#6119)

refactor(data/ordmap/ordset): simpler proof of `not_le_delta` (#6119) 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.