mathlib

0e3184fc - feat(data/fin/tuple/basic): add lemmas for rewriting exists and forall over `n+1`-tuples (#15048)

feat(data/fin/tuple/basic): add lemmas for rewriting exists and forall over `n+1`-tuples (#15048) The lemma names `fin.forall_fin_succ_pi` and `fin.exists_fin_succ_pi` mirror the existing `fin.forall_fin_succ` and `fin.exists_fin_succ`.