mathlib3

dfdea866 - remove sorry in dirichlet_inv_to_fun