Lean fderiv of a product of a function with an inverse: rewrite the lambda to Pi form first

Goal: fderiv ℝ (fun q ↦ g q * (f q)⁻¹) p for real-valued f, g on ℝ×ℝ. hinv := (hasDerivAt_inv hne).comp_hasFDerivAt p (hf p).hasFDerivAt has function (fun y ↦ y⁻¹) ∘ f, and ((hg p).hasFDerivAt.mul hinv).fderiv is about g * ((fun y ↦ y⁻¹) ∘ f) (Pi multiplication), so rw [h.fderiv] does not match the lambda. Fix: rw [show (fun q ↦ g q * (f q)⁻¹) = g * ((fun y : ℝ ↦ y⁻¹) ∘ f) from rfl, h] and then simp; ring. If your operator is a def wrapping fderiv (like a partial derivative du f p := fderiv ℝ f p (1,0)), do NOT unfold it before the rewrite, because that also unfolds occurrences inside g. Restate the goal with show du (...) p = fderiv ℝ (...) p (1,0) from rfl instead. Also: if f ≥ 0 everywhere and f p = 0, IsLocalMin.fderiv_eq_zero (from Filter.Eventually.of_forall) kills the first derivatives at p.