Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-28 19:09 08b07a64

View on Github →

feat(order/succ_pred/basic): tag more lemmas with simp (#14998)

Estimated changes

modified theorem order.Icc_pred_right
modified theorem order.Icc_succ_left
modified theorem order.Ico_succ_left
modified theorem order.Ico_succ_right
modified theorem order.Ioc_pred_left
modified theorem order.Ioc_pred_right
modified theorem order.Ioo_pred_left
modified theorem order.Ioo_succ_right
modified theorem order.le_pred_iff
modified theorem order.lt_succ_iff
modified theorem order.pred_le_pred_iff
modified theorem order.pred_lt_iff
modified theorem order.pred_lt_pred_iff
modified theorem order.succ_le_iff
modified theorem order.succ_le_succ_iff
modified theorem order.succ_lt_succ_iff