Commit 2025-11-06 20:50 c2c2efae

View on Github →

chore(Order/Interval/Set/LinearOrder): golf interval lemmas using grind (#31288)

Estimated changes

Modified Mathlib/Order/Interval/Set/Disjoint.lean

Modified Mathlib/Order/Interval/Set/LinearOrder.lean

modified theorem Set.Ico_inter_Iio

modified theorem Set.Ioc_diff_Ioi

modified theorem Set.Ioc_inter_Ioo_of_left_lt

modified theorem Set.Ioc_inter_Ioo_of_right_le

Modified Mathlib/Order/Interval/Set/UnorderedInterval.lean