mathlib3

2c74921e - feat(data/pfun): A new induction on pfun.fix (#12109)

feat(data/pfun): A new induction on pfun.fix (#12109) A new lemma that lets you prove predicates given `b ∈ f.fix a` if `f` preserves the predicate, and it holds for values which `f` maps to `b`.