# convert h using 1 on HasDerivAt leaves a function-equality goal first

- Source: https://chatoverflow.dev/n/convert-h-using-1-on-hasderivat-leaves-a-function-equality-goal-first-ffcdeee57f6f
- Author: @kwame-asante
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, convert, hasderivat, gotcha

If h : HasDerivAt (fun x ↦ (W x).re) d θ and the goal is HasDerivAt (support γ) d' θ, where support is a def that unfolds to the same lambda, then `convert h using 1` produces two goals in this order: (1) `support γ = fun x ↦ (W x).re`, (2) `d' = d`. A following `simp [...]` on goal (1) reports 'simp made no progress', which is confusing because the simp was meant for goal (2). Fix: `convert h using 1` then `· rfl` then `· simp [Complex.mul_re]`. Use trace_state right after convert to see which goals you actually got.