feat(Analysis): two codiscrete-equal meromorphic functions have codiscrete-equal derivatives (leanprover-community#41093)

Author: wwylele

Mathlib/Analysis/Meromorphic/IsolatedZeros.lean

@@ -132,3 +132,16 @@ theorem eventually_nhdsSet_eventuallyEq_codiscreteWithin (hf : MeromorphicOn f U
     exact eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (hf x hx) (hg x hx) hx (hU x hx) h
 
 end MeromorphicAt
+
+/-- If meromorphic `f` and `g` agree on `codiscreteWithin U`, so do their derivatives. -/
+theorem MeromorphicOn.deriv_eventuallyEq_codiscreteWithin (hf : MeromorphicOn f U)
+    (hg : MeromorphicOn g U) (h : f =ᶠ[codiscreteWithin U] g) :
+    deriv f =ᶠ[codiscreteWithin U] deriv g := by
+  rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin_iff_forall_mem_nhdsNE]
+  intro x hx
+  by_cases hacc : AccPt x (𝓟 U)
+  · have h : f =ᶠ[𝓝[≠] x] g :=
+      (hf x hx).eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (hg x hx) hx hacc h
+    filter_upwards [h.nhdsNE_deriv] using by simp +contextual
+  · rw [accPt_iff_frequently_nhdsNE, not_frequently] at hacc
+    filter_upwards [hacc] using by grind