Commit 2025-03-11 07:54 43020fb7

View on Github →

feat(Order/Fin): add @[simp] and @[gcongr] lemmas (#22455)

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.castPred_le_castPred

added theorem Fin.castPred_lt_castPred

Modified Mathlib/Order/Fin/Basic.lean

added theorem Fin.addNat_inj

added theorem Fin.addNat_le_addNat_iff

added theorem Fin.addNat_lt_addNat_iff

added theorem Fin.castLE_le_castLE_iff

added theorem Fin.castLE_lt_castLE_iff

added theorem Fin.natAdd_inj

added theorem Fin.natAdd_le_natAdd_iff

added theorem Fin.natAdd_lt_natAdd_iff

added theorem Fin.predAbove_le_predAbove

added theorem Fin.succAbove_inj

added theorem GCongr.Fin.predAbove_le_predAbove_right

added theorem GCongr.predAbove_le_predAbove_left