import ProofExplorer.Jacobian.Library

namespace ProofExplorer.Jacobian.CalculusLibrary
open MvPolynomial

set_option backward.isDefEq.respectTransparency false in
/-- Formal partial derivatives agree with analytic coordinate derivatives. -/
theorem eval_hasDerivAt {n : ℕ} (p : MvPolynomial (Fin n) ℝ)
    (u : Fin n → ℝ) (j : Fin n) :
    HasDerivAt (fun t => eval (Function.update u j t) p)
      (eval u (pderiv j p)) (u j) := by
  induction p using MvPolynomial.induction_on with
  | C c => simpa using hasDerivAt_const (u j) c
  | add p q hp hq =>
    convert! hp.add hq using 1 <;> simp [Pi.add_apply] <;> rfl
  | mul_X p i hp =>
    by_cases hij : j = i
    · subst i
      convert! hp.mul (hasDerivAt_id (u j)) using 1 <;>
        simp [Derivation.leibniz, smul_eq_mul, Pi.mul_apply, mul_comm, add_comm] <;> rfl
    · convert! hp.mul (hasDerivAt_const (u j) (u i)) using 1 <;>
        simp [Derivation.leibniz, smul_eq_mul, hij, Function.update_of_ne (Ne.symm hij), Pi.mul_apply, mul_comm] <;> rfl

end ProofExplorer.Jacobian.CalculusLibrary