Commit 2023-07-27 11:51 24924f96

View on Github →

chore: bump to nightly-2023-07-15 (#5992) Various adaptations to changes when Fin API was moved to Std. One notable change is that many lemmas are now stated in terms of i ≠ 0 (for i : Fin n) rather then i.1 ≠ 0, and as a consequence many Fin.vne_of_ne applications have been added or removed, mostly removed.

Estimated changes

deleted def Fin.addCases
deleted theorem Fin.addCases_left
deleted theorem Fin.addCases_right
deleted theorem Fin.addNat_mk
deleted theorem Fin.addNat_one
deleted theorem Fin.addNat_subNat
deleted theorem Fin.add_def
deleted theorem Fin.add_one_le_iff
deleted theorem Fin.add_one_lt_iff
deleted theorem Fin.add_one_pos
deleted def Fin.cases
deleted theorem Fin.cases_succ'
deleted theorem Fin.cases_succ
deleted theorem Fin.cases_zero
deleted theorem Fin.castAdd_castAdd
deleted theorem Fin.castAdd_castLT
deleted theorem Fin.castAdd_lt
deleted theorem Fin.castAdd_mk
deleted theorem Fin.castAdd_natAdd
deleted theorem Fin.castAdd_zero
deleted theorem Fin.castLE_castLE
deleted theorem Fin.castLE_comp_castLE
deleted theorem Fin.castLE_mk
deleted theorem Fin.castLE_of_eq
deleted theorem Fin.castLE_succ
deleted theorem Fin.castLE_zero
deleted theorem Fin.castLT_castAdd
deleted theorem Fin.castLT_castSucc
deleted theorem Fin.castLT_mk
added def Fin.castPred
deleted theorem Fin.castSucc_castLT
deleted theorem Fin.castSucc_eq_zero_iff
deleted theorem Fin.castSucc_fin_succ
deleted theorem Fin.castSucc_inj
deleted theorem Fin.castSucc_lt_last
deleted theorem Fin.castSucc_lt_succ
deleted theorem Fin.castSucc_mk
deleted theorem Fin.castSucc_ne_zero_iff
deleted theorem Fin.castSucc_one
added theorem Fin.castSucc_pos'
deleted theorem Fin.castSucc_pos
added theorem Fin.castSucc_zero'
deleted theorem Fin.castSucc_zero
added theorem Fin.cast_refl
deleted theorem Fin.coeSucc_eq_succ
deleted theorem Fin.coe_addNat
deleted theorem Fin.coe_castAdd
deleted theorem Fin.coe_castLE
deleted theorem Fin.coe_castLT
deleted theorem Fin.coe_castSucc
deleted theorem Fin.coe_clamp
deleted theorem Fin.coe_mul
deleted theorem Fin.coe_natAdd
deleted theorem Fin.coe_pred
deleted theorem Fin.coe_subNat
deleted theorem Fin.dite_val
deleted theorem Fin.eq_last_of_not_lt
deleted theorem Fin.eq_mk_iff_val_eq
deleted theorem Fin.eq_succ_of_ne_zero
deleted theorem Fin.eq_zero_or_eq_succ
deleted theorem Fin.exists_castSucc_eq
deleted theorem Fin.exists_fin_one
deleted theorem Fin.exists_fin_succ
deleted theorem Fin.exists_fin_two
deleted theorem Fin.exists_iff
deleted theorem Fin.ext
deleted theorem Fin.fin_one_eq_zero
deleted theorem Fin.forall_fin_one
deleted theorem Fin.forall_fin_succ
deleted theorem Fin.forall_fin_two
deleted theorem Fin.forall_iff
deleted def Fin.induction
deleted def Fin.inductionOn
deleted theorem Fin.induction_succ
deleted theorem Fin.induction_zero
deleted theorem Fin.is_le'
deleted theorem Fin.is_le
deleted theorem Fin.is_lt
deleted theorem Fin.ite_val
deleted def Fin.lastCases
deleted theorem Fin.lastCases_castSucc
deleted theorem Fin.lastCases_last
deleted theorem Fin.last_add_one
deleted theorem Fin.last_le_iff
deleted theorem Fin.last_pos
deleted theorem Fin.le_castSucc_iff
deleted theorem Fin.le_coe_addNat
deleted theorem Fin.le_coe_natAdd
deleted theorem Fin.le_last
added theorem Fin.le_zero_iff'
deleted theorem Fin.le_zero_iff
deleted theorem Fin.lt_add_one_iff
deleted theorem Fin.lt_succ
deleted theorem Fin.mk_le_mk
deleted theorem Fin.mk_le_of_le_val
deleted theorem Fin.mk_lt_mk
deleted theorem Fin.mk_lt_of_lt_val
deleted theorem Fin.mk_one
deleted theorem Fin.mk_succ_pos
deleted theorem Fin.mk_val
deleted theorem Fin.mk_zero
deleted theorem Fin.mod_def
deleted theorem Fin.mul_def
deleted theorem Fin.natAdd_castAdd
deleted theorem Fin.natAdd_castSucc
deleted theorem Fin.natAdd_last
deleted theorem Fin.natAdd_mk
deleted theorem Fin.natAdd_natAdd
deleted theorem Fin.natAdd_zero
deleted theorem Fin.not_lt_zero
deleted theorem Fin.one_lt_succ_succ
deleted theorem Fin.one_pos
added theorem Fin.pos_iff_ne_zero'
deleted theorem Fin.pos_iff_ne_zero
deleted theorem Fin.pos_iff_nonempty
added def Fin.predAbove
modified theorem Fin.predAbove_zero
deleted theorem Fin.pred_add_one
deleted theorem Fin.pred_castSucc_succ
deleted theorem Fin.pred_eq_iff_eq_succ
deleted theorem Fin.pred_inj
deleted theorem Fin.pred_le_pred_iff
deleted theorem Fin.pred_lt_pred_iff
deleted theorem Fin.pred_mk
deleted theorem Fin.pred_mk_succ'
deleted theorem Fin.pred_mk_succ
deleted theorem Fin.pred_one
deleted theorem Fin.pred_succ
modified theorem Fin.pred_succAbove_pred
deleted theorem Fin.subNat_addNat
deleted theorem Fin.subNat_mk
deleted theorem Fin.sub_def
added def Fin.succAbove
deleted def Fin.succRec
deleted def Fin.succRecOn
deleted theorem Fin.succRecOn_succ
deleted theorem Fin.succRecOn_zero
deleted theorem Fin.succ_castSucc
deleted theorem Fin.succ_eq_last_succ
deleted theorem Fin.succ_inj
deleted theorem Fin.succ_last
deleted theorem Fin.succ_le_succ_iff
deleted theorem Fin.succ_lt_succ_iff
deleted theorem Fin.succ_mk
deleted theorem Fin.succ_ne_zero
modified theorem Fin.succ_one_eq_two'
deleted theorem Fin.succ_one_eq_two
deleted theorem Fin.succ_pos
deleted theorem Fin.succ_pred
deleted theorem Fin.succ_succ_ne_one
modified theorem Fin.succ_zero_eq_one'
deleted theorem Fin.succ_zero_eq_one
deleted theorem Fin.val_add
deleted theorem Fin.val_add_one
deleted theorem Fin.val_add_one_of_lt
deleted theorem Fin.val_last
deleted theorem Fin.val_lt_last
deleted theorem Fin.val_mk
deleted theorem Fin.val_mul
deleted theorem Fin.val_one
deleted theorem Fin.val_succ
deleted theorem Fin.val_two
added theorem Fin.val_zero'
deleted theorem Fin.val_zero
deleted theorem Fin.zero_le
deleted theorem Fin.zero_lt_one
deleted theorem Fin.zero_ne_one
deleted theorem List.mem_reverse'
deleted theorem List.take_nil
deleted theorem Nat.succ_lt_succ_iff