Some auxiliary results for Function.Exact

Nothing in this file since it's already merged into mathlib.