Commit 2025-02-14 10:46 1da726ff
View on Github →feat(Data/Fin/Basic): add norm_cast tag to cast_val_eq_self (#21775)
Now, norm_cast can simplify Nat.cast (Fin.val n) to n. This is point (1) of https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Possible.20improvements.20to.20Lean.2FMathlib/near/499085779.
Also removes some outdated porting notes, which talk about (now removed) align statements.