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

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.