Commit 2026-09-11 08:52 a3ab3e36

View on Github →

chore(Data/Fin/SuccPred): avoid importing the order hierarchy (#43152) Mathlib.Data.Fin.SuccPred imports Mathlib.Logic.Equiv.Set mostly for two simp lemmas that use Equiv.ofInjective, which brings with it nontrivial order definitions such as BooleanAlgebra. These were introduced in leanprover-community/mathlib3#6815 but seemingly never used and spelled strangely, so we deprecate them.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Fin/Basic.lean

Modified Mathlib/Data/Fin/Embedding.lean

Created Mathlib/Data/Fin/EquivOfInjective.lean

added theorem Fin.coe_of_injective_castLE_symm

added theorem Fin.coe_of_injective_castSucc_symm

Modified Mathlib/Data/Fin/Rev.lean

Modified Mathlib/Data/Fin/SuccPred.lean

modified theorem Fin.castLE_rfl

modified theorem Fin.castLT_eq_castPred

modified theorem Fin.castPred_castSucc

modified theorem Fin.castPred_mk

deleted theorem Fin.coe_of_injective_castLE_symm

deleted theorem Fin.coe_of_injective_castSucc_symm

modified theorem Fin.pred_last

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/Data/Fin/Tuple/Embedding.lean

Modified Mathlib/Data/Fin/VecNotation.lean

Modified Mathlib/Data/Num/Bitwise.lean

Modified Mathlib/Data/Vector/Basic.lean

Modified Mathlib/Order/Fin/Basic.lean

Modified Mathlib/Order/Interval/Set/Fin.lean