feat(Analysis/Analytic): analytic order at zero with vanishing value (leanprover-community#36865)

Add AnalyticAt.analyticOrderAt_eq_one_of_zero_deriv_ne_zero: if f is analytic at x, f(x) = 0, and f'(x) ≠ 0, then analyticOrderAt f x = 1.
Placed next to analyticOrderAt_sub_eq_one_of_deriv_ne_zero in Order.lean per review feedback on leanprover-community#36778.

AI disclosure: Lean code developed with Claude (Anthropic) assistance in workflow. Mathematical content and proof strategies are original. All code verified locally with lake env lean before submission.

Co-authored-by: interleaves <psinary@hotmail.com>

Author: psinary-sketch

Mathlib/Analysis/Analytic/Order.lean

@@ -323,6 +323,14 @@ theorem AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero {x : 𝕜} (hf :
         deriv_fun_pow (by fun_prop), sub_self, zero_pow (by lia), zero_pow (by lia),
         mul_zero, zero_mul, zero_smul, zero_smul, add_zero]
 
+/-- At a zero with nonvanishing derivative, the analytic order is 1.
+This is a variant of `analyticOrderAt_sub_eq_one_of_deriv_ne_zero` with `f z₀ = 0`
+replacing the subtraction. -/
+theorem AnalyticAt.analyticOrderAt_eq_one_of_zero_deriv_ne_zero {x : 𝕜}
+    (hf : AnalyticAt 𝕜 f x) (hfx : f x = 0) (hf' : deriv f x ≠ 0) :
+    analyticOrderAt f x = 1 := by
+  simpa [hfx] using hf.analyticOrderAt_sub_eq_one_of_deriv_ne_zero hf'
+
 lemma natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero [CharZero 𝕜] [CompleteSpace E]
     (hf : AnalyticAt 𝕜 f z₀) :
     n ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0 := by