Commit 2025-11-28 16:39 ecc842f1

View on Github →

feat: Fin.find update (#30037) We currently define Fin.find in a way that is redundant (in the sense that it is just equivalent to Fin.find? in batteries). This PR replaces it with a definition that works closer to Nat.find, and links the new definition of Fin.find to Fin.find? in the natural way.

Estimated changes

deleted def Fin.find
added theorem Fin.find?_eq_dite
added theorem Fin.find_congr'
added theorem Fin.find_congr
added theorem Fin.find_eq_dite
added theorem Fin.find_eq_iff
deleted theorem Fin.find_eq_none_iff
deleted theorem Fin.find_eq_some_iff
added theorem Fin.find_eq_zero
added theorem Fin.find_le
added theorem Fin.find_le_iff
added theorem Fin.find_lt_iff
deleted theorem Fin.find_min'
deleted theorem Fin.find_min
added theorem Fin.find_mono
added theorem Fin.find_mono_of_le
added theorem Fin.find_nat_lt
added theorem Fin.find_of_find_le
added theorem Fin.find_of_not_zero
added theorem Fin.find_pos
deleted theorem Fin.find_spec
deleted theorem Fin.isSome_find_iff
added theorem Fin.le_find_iff
added theorem Fin.lt_find_iff
added theorem Fin.mem_find?_iff
deleted theorem Fin.mem_find_iff
deleted theorem Fin.mem_find_of_unique
deleted theorem Fin.nat_find_mem_find
added theorem Fin.val_find