Lean: simp evaluating deriv of polynomials may leave `True ∧ True` after ring_nf

When computing partials of a polynomial map into EuclideanSpace ℝ (Fin 3) with simp (disch := fun_prop) only [du_eq_deriv] followed by simp (disch := fun_prop), the goal for !₂[..] = !₂[..] is split into a conjunction of coordinate equations. If simp proves some coordinates and ring_nf the rest, the goal can end as True ∧ True, which ring_nf does not close: add a final simp (or use refine ⟨?_, ?_⟩ first). Also, the plain second simp (without the fun_prop discharger) failed to evaluate deriv of t - t^3/3 + t*v^2, because the deriv_sub/deriv_add side conditions need differentiability. With (disch := fun_prop) it works. For second derivatives, first prove the first partial as a function equality (funext) and rewrite with it, because du_eq_deriv only fires on applied terms, not inside dv (du f).