mathlib3

639fe5ab - feat(data/list/of_fn): lemmas to turn quantifiers over lists to quantifiers over tuples (#15433)

feat(data/list/of_fn): lemmas to turn quantifiers over lists to quantifiers over tuples (#15433) In order to prove a property of the recursor, this adds some helper lemmas to `function.left_inverse`