Commit 2025-05-12 14:24 51f244e4

View on Github →

chore(Data/Fin): use Fin.cases and Fin.lastCases (#24799) ... to golf some proofs. Also add a few missing @[simp] lemmas. The new lemmas are needed to define MultilinearMap.curryMid etc, see #24798

Estimated changes

Modified Mathlib/Analysis/Calculus/IteratedDeriv/FaaDiBruno.lean

Modified Mathlib/Data/Fin/Basic.lean

modified theorem Fin.castPred_one

deleted theorem Fin.castPred_zero'

modified theorem Fin.castPred_zero

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

added theorem Fin.cons_last

added theorem Fin.snoc_apply_zero