Commit 2025-05-19 08:29 f7eae15e

View on Github →

chore(Fin/Basic): drop Prop arguments with default values (#24979) Due to proof irrelevalnce, there is no reason to allow users to supply custom proofs for these arguments.

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

modified theorem Fin.castSucc_pred_eq_pred_castSucc

modified theorem Fin.predAbove_castPred_of_le

modified theorem Fin.predAbove_castPred_of_lt

modified theorem Fin.predAbove_castSucc_of_lt

modified theorem Fin.predAbove_of_castSucc_lt

modified theorem Fin.predAbove_of_le_castSucc

modified theorem Fin.predAbove_of_lt_succ

modified theorem Fin.predAbove_of_succ_le

modified theorem Fin.predAbove_pred_of_le

modified theorem Fin.predAbove_pred_of_lt

modified theorem Fin.predAbove_succ_of_lt

modified theorem Fin.succAbove_castPred_of_lt

modified theorem Fin.succAbove_pred_of_lt