Commit 2026-03-21 08:07 981e8652

View on Github →

chore(Order/SuccPred/Basic): use to_dual more (#36612) When this file was originally tagged with to_dual, the attribute was less capable. Now, we can tag almost everything in the file. This PR does the first half of the remaining tagging. The rest can be done in a future PR.

Estimated changes

Modified Mathlib/Order/SuccPred/Basic.lean

deleted theorem Order.Icc_pred_right

deleted theorem Order.Icc_pred_right_of_not_isMin

deleted theorem Order.Icc_subset_Ioc_pred_left

deleted theorem Order.Icc_subset_Ioc_pred_left_of_not_isMin

deleted theorem Order.Ici_subset_Ioi_pred

deleted theorem Order.Ici_subset_Ioi_pred_of_not_isMin

deleted theorem Order.Ico_subset_Ioo_pred_left

deleted theorem Order.Ico_subset_Ioo_pred_left_of_not_isMin

deleted theorem Order.Iic_pred

deleted theorem Order.Iic_pred_of_not_isMin

deleted theorem Order.Ioc_pred_right

deleted theorem Order.Ioc_pred_right_of_not_isMin

deleted theorem Order.pred_covBy

deleted theorem Order.pred_covBy_of_not_isMin

deleted theorem Order.pred_eq_iff_covBy

deleted theorem Order.pred_eq_of_covBy

deleted theorem Order.pred_le_of_wcovBy

deleted theorem Order.pred_strictMono

deleted theorem Order.pred_wcovBy

deleted theorem OrderIso.map_pred

deleted def PredOrder.ofCore

deleted def PredOrder.ofLePredIff