Commit 2025-09-04 06:44 419963ad

View on Github →

chore(Data/Fin/Basic): Split lemmas on succ and pred. (#29199) This PR splits succ, pred and related lemmas from the long Data/Fin/Basic file. These go to SuccPred.lean. The previous contents of SuccPred.lean, which are about SuccOrder and PredOrder, go to a new file SuccPredOrder.lean

Estimated changes

deleted theorem Fin.castAdd_inj
deleted theorem Fin.castAdd_injective
deleted theorem Fin.castLE_castSucc
deleted theorem Fin.castLE_comp_castSucc
deleted theorem Fin.castLE_inj
deleted theorem Fin.castLE_injective
deleted theorem Fin.castLE_rfl
deleted theorem Fin.castLT_eq_castPred
deleted def Fin.castPred
deleted theorem Fin.castPred_castSucc
deleted theorem Fin.castPred_eq_zero
deleted theorem Fin.castPred_inj
deleted theorem Fin.castPred_le_castPred
deleted theorem Fin.castPred_le_iff
deleted theorem Fin.castPred_le_pred_iff
deleted theorem Fin.castPred_lt_castPred
deleted theorem Fin.castPred_lt_iff
deleted theorem Fin.castPred_mk
deleted theorem Fin.castPred_ne_zero
deleted theorem Fin.castPred_one
deleted theorem Fin.castPred_succAbove
deleted theorem Fin.castPred_zero
deleted theorem Fin.castSucc_castAdd
deleted theorem Fin.castSucc_castPred
deleted theorem Fin.castSucc_eq_zero_iff'
deleted theorem Fin.castSucc_injective
deleted theorem Fin.castSucc_le_succ
deleted theorem Fin.castSucc_lt_succ_iff
deleted theorem Fin.castSucc_ne_last
deleted theorem Fin.castSucc_ne_zero_iff'
deleted theorem Fin.castSucc_pos_iff
deleted theorem Fin.castSucc_pred_lt
deleted theorem Fin.castSucc_pred_lt_iff
deleted theorem Fin.castSucc_zero'
deleted theorem Fin.cast_eq_cast
deleted theorem Fin.cast_inj
deleted theorem Fin.cast_le_cast
deleted theorem Fin.cast_lt_cast
deleted theorem Fin.castpred_succ_le_iff
deleted theorem Fin.coe_castPred
deleted theorem Fin.coe_eq_castSucc
deleted theorem Fin.coe_succ_lt_iff_lt
deleted theorem Fin.exists_fin_succ'
deleted theorem Fin.exists_succAbove_eq
deleted theorem Fin.exists_succ_eq
deleted theorem Fin.forall_fin_succ'
deleted theorem Fin.le_castPred_iff
deleted theorem Fin.le_castSucc_pred_iff
deleted theorem Fin.le_pred_castSucc_iff
deleted theorem Fin.le_pred_iff
deleted theorem Fin.le_zero_iff'
deleted theorem Fin.leftInverse_cast
deleted theorem Fin.lt_castPred_iff
deleted theorem Fin.lt_castPred_succ
deleted theorem Fin.lt_castPred_succ_iff
deleted theorem Fin.lt_pred_iff
deleted theorem Fin.lt_succ_castPred
deleted theorem Fin.lt_succ_castPred_iff
deleted theorem Fin.ne_succAbove
deleted theorem Fin.one_pos'
deleted theorem Fin.one_succAbove_one
deleted theorem Fin.one_succAbove_succ
deleted theorem Fin.one_succAbove_zero
deleted def Fin.predAbove
deleted theorem Fin.predAbove_last_apply
deleted theorem Fin.predAbove_of_lt_succ
deleted theorem Fin.predAbove_of_succ_le
deleted theorem Fin.predAbove_pred_of_le
deleted theorem Fin.predAbove_pred_of_lt
deleted theorem Fin.predAbove_pred_self
deleted theorem Fin.predAbove_right_last
deleted theorem Fin.predAbove_right_zero
deleted theorem Fin.predAbove_succAbove
deleted theorem Fin.predAbove_succ_of_le
deleted theorem Fin.predAbove_succ_of_lt
deleted theorem Fin.predAbove_succ_self
deleted theorem Fin.predAbove_surjective
deleted theorem Fin.predAbove_zero
deleted theorem Fin.predAbove_zero_succ
deleted theorem Fin.pred_castSucc_lt
deleted theorem Fin.pred_castSucc_lt_iff
deleted theorem Fin.pred_last
deleted theorem Fin.pred_le_iff
deleted theorem Fin.pred_lt_castPred
deleted theorem Fin.pred_lt_castPred_iff
deleted theorem Fin.pred_lt_iff
deleted theorem Fin.pred_one'
deleted theorem Fin.pred_succAbove
deleted theorem Fin.pred_succAbove_pred
deleted theorem Fin.range_castLE
deleted theorem Fin.range_castSucc
deleted theorem Fin.range_succ
deleted theorem Fin.range_succAbove
deleted theorem Fin.rightInverse_cast
deleted def Fin.succAbove
deleted theorem Fin.succAbove_eq_last_iff
deleted theorem Fin.succAbove_eq_zero_iff
deleted theorem Fin.succAbove_last
deleted theorem Fin.succAbove_last_apply
deleted theorem Fin.succAbove_left_inj
deleted theorem Fin.succAbove_ne
deleted theorem Fin.succAbove_ne_last
deleted theorem Fin.succAbove_ne_zero
deleted theorem Fin.succAbove_of_lt_succ
deleted theorem Fin.succAbove_of_succ_le
deleted theorem Fin.succAbove_pos
deleted theorem Fin.succAbove_predAbove
deleted theorem Fin.succAbove_pred_of_le
deleted theorem Fin.succAbove_pred_of_lt
deleted theorem Fin.succAbove_pred_self
deleted theorem Fin.succAbove_right_inj
deleted theorem Fin.succAbove_succ_of_le
deleted theorem Fin.succAbove_succ_of_lt
deleted theorem Fin.succAbove_succ_self
deleted theorem Fin.succAbove_zero
deleted theorem Fin.succAbove_zero_apply
deleted theorem Fin.succ_castAdd
deleted theorem Fin.succ_castPred_le_iff
deleted theorem Fin.succ_injective
deleted theorem Fin.succ_le_castSucc_iff
deleted theorem Fin.succ_natAdd
deleted theorem Fin.succ_ne_last_iff
deleted theorem Fin.succ_ne_last_of_lt
deleted theorem Fin.succ_one_eq_two'
deleted theorem Fin.succ_predAbove_succ
deleted theorem Fin.succ_predAbove_zero
deleted theorem Fin.succ_succAbove_one
deleted theorem Fin.succ_succAbove_succ
deleted theorem Fin.succ_succAbove_zero
deleted theorem Fin.succ_zero_eq_one'
deleted theorem Fin.zero_ne_one'
deleted theorem Fin.zero_succAbove
deleted def finCongr
deleted theorem finCongr_apply_coe
deleted theorem finCongr_apply_mk
deleted theorem finCongr_eq_equivCast
deleted theorem finCongr_refl
deleted theorem finCongr_symm
deleted theorem finCongr_symm_apply_coe
added theorem Fin.castAdd_inj
added theorem Fin.castAdd_injective
added theorem Fin.castLE_castSucc
added theorem Fin.castLE_inj
added theorem Fin.castLE_injective
added theorem Fin.castLE_rfl
added theorem Fin.castLT_eq_castPred
added def Fin.castPred
added theorem Fin.castPred_castSucc
added theorem Fin.castPred_eq_zero
added theorem Fin.castPred_inj
added theorem Fin.castPred_le_iff
added theorem Fin.castPred_lt_iff
added theorem Fin.castPred_mk
added theorem Fin.castPred_ne_zero
added theorem Fin.castPred_one
added theorem Fin.castPred_succAbove
added theorem Fin.castPred_zero
added theorem Fin.castSucc_castAdd
added theorem Fin.castSucc_castPred
added theorem Fin.castSucc_injective
added theorem Fin.castSucc_le_succ
added theorem Fin.castSucc_ne_last
added theorem Fin.castSucc_pos_iff
added theorem Fin.castSucc_pred_lt
added theorem Fin.castSucc_zero'
added theorem Fin.cast_eq_cast
added theorem Fin.cast_inj
added theorem Fin.cast_le_cast
added theorem Fin.cast_lt_cast
added theorem Fin.coe_castPred
added theorem Fin.coe_eq_castSucc
added theorem Fin.coe_succ_lt_iff_lt
added theorem Fin.exists_fin_succ'
added theorem Fin.exists_succ_eq
added theorem Fin.forall_fin_succ'
added theorem Fin.le_castPred_iff
added theorem Fin.le_pred_iff
added theorem Fin.le_zero_iff'
added theorem Fin.leftInverse_cast
added theorem Fin.lt_castPred_iff
added theorem Fin.lt_castPred_succ
added theorem Fin.lt_pred_iff
added theorem Fin.lt_succ_castPred
added theorem Fin.ne_succAbove
added theorem Fin.one_pos'
added theorem Fin.one_succAbove_one
added theorem Fin.one_succAbove_succ
added theorem Fin.one_succAbove_zero
deleted theorem Fin.orderPred_apply
deleted theorem Fin.orderPred_eq
deleted theorem Fin.orderPred_succ
deleted theorem Fin.orderPred_zero
deleted theorem Fin.orderSucc_apply
deleted theorem Fin.orderSucc_castSucc
deleted theorem Fin.orderSucc_eq
deleted theorem Fin.orderSucc_last
added def Fin.predAbove
added theorem Fin.predAbove_zero
added theorem Fin.pred_castSucc_lt
added theorem Fin.pred_last
added theorem Fin.pred_le_iff
added theorem Fin.pred_lt_castPred
added theorem Fin.pred_lt_iff
added theorem Fin.pred_one'
added theorem Fin.pred_succAbove
added theorem Fin.range_castLE
added theorem Fin.range_castSucc
added theorem Fin.range_succ
added theorem Fin.range_succAbove
added theorem Fin.rightInverse_cast
added def Fin.succAbove
added theorem Fin.succAbove_last
added theorem Fin.succAbove_left_inj
added theorem Fin.succAbove_ne
added theorem Fin.succAbove_ne_last
added theorem Fin.succAbove_ne_zero
added theorem Fin.succAbove_pos
added theorem Fin.succAbove_zero
added theorem Fin.succ_castAdd
added theorem Fin.succ_injective
added theorem Fin.succ_natAdd
added theorem Fin.succ_ne_last_iff
added theorem Fin.succ_ne_last_of_lt
added theorem Fin.succ_one_eq_two'
added theorem Fin.succ_succAbove_one
added theorem Fin.succ_zero_eq_one'
added theorem Fin.zero_ne_one'
added theorem Fin.zero_succAbove
added def finCongr
added theorem finCongr_apply_coe
added theorem finCongr_apply_mk
added theorem finCongr_eq_equivCast
added theorem finCongr_refl
added theorem finCongr_symm
added theorem Fin.orderPred_apply
added theorem Fin.orderPred_eq
added theorem Fin.orderPred_succ
added theorem Fin.orderPred_zero
added theorem Fin.orderSucc_apply
added theorem Fin.orderSucc_castSucc
added theorem Fin.orderSucc_eq
added theorem Fin.orderSucc_last