mathlib

13bc7a20 - feat(data/pfun): review APIs, add some lemmas about `fix_induction` (#17004)