Commit 2024-11-12 20:13 66f0c7ed

View on Github →

chore: remove obsolete porting note about Finset.castSucc (#18929) Removes a comment in Data.Fin.Tuple.Basic that says

Porting note: i.castSucc does not work like it did in Lean 3 and rewrites all instances of (castSucc i) in that file to i.castSucc. The comment was included when that file was first ported in a43b3f18decdb5808a2dfc1d09cb17a88657d115. Currently, however, there does not seem to be any issue with writing i.castSucc as was done in mathlib3.

Estimated changes

modified def Fin.init
modified theorem Fin.init_update_castSucc
modified def Fin.snoc
modified theorem Fin.snoc_castSucc
modified theorem Fin.snoc_cast_add
modified theorem Fin.snoc_update