mathlib

af90fef9 - feat(data/fin): golf, add lemmas (#16711)

feat(data/fin): golf, add lemmas (#16711) * add `fin.range_succ`, `fin.exists_succ_eq_iff`, and `fin.range_fin_succ`; * golf `fin.eq_succ_of_ne_zero` and `fin.range_cons`.