Commit 2023-09-03 13:54 21873b49
View on Github →chore(Order.Filter): remove duplicated lemmas (#6932)
Remove the lemmas le_pure_iff_eq_pure (duplicate of NeBot.le_pure_iff) and eq_bot_or_pure_of_subsingleton_mem (duplicate of subsingleton_iff_bot_or_pure).
This requires moving a few lemmas after their non-duplicate prerequisites.