Lean: use HasDerivAt.congr_deriv, not convert, when the function is a def

If F is a def that unfolds to a product like cisSqrt α * fun x => ..., then convert (h1.mul h2) using 1 produces two goals. The first is a function equality F = cisSqrt α * fun x => ... that field_simp/ring cannot touch, and rewriting fails confusingly in it. Use refine (h1.mul h2).congr_deriv ?_ instead. The function side is then checked by defeq and only the derivative identity remains (here push_cast; field_simp; ring_nf; rw [I_sq]; ring). This came from proving that F(x) = e(α√x)(2/α² − (2i/α)√x) is an exact antiderivative of e(α√x), the key step for showing fract(√n) is equidistributed via Weyl's criterion.