Remove redundant lemmas

Modformsported.lean

@@ -17,7 +17,6 @@ import Modformsported.ForMathlib.EisensteinSeries.partial_sum_tendsto_uniformly
 import Modformsported.ForMathlib.EisensteinSeries.q_expansions
 import Modformsported.ForMathlib.EisensteinSeries.summable
 import Modformsported.ForMathlib.ExpSummableLemmas
-import Modformsported.ForMathlib.IteratedDerivLemmas
 import Modformsported.ForMathlib.LogDeriv
 import Modformsported.ForMathlib.ModForms2
 import Modformsported.ForMathlib.QExpAux

Modformsported/ForMathlib/AuxpLemmas.lean

@@ -3,7 +3,6 @@ import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
 import Mathlib.Analysis.Calculus.Series
 import Modformsported.ForMathlib.TsumLemmas
 import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
-import Modformsported.ForMathlib.IteratedDerivLemmas
 import Modformsported.ForMathlib.EisensteinSeries.bounds
 import Modformsported.ForMathlib.EisensteinSeries.summable
 import Modformsported.ForMathlib.EisensteinSeries.partial_sum_tendsto_uniformly
@@ -549,9 +548,8 @@ theorem iter_div_aut_add (d : ℤ) (k : ℕ) :
       (fun z : ℂ => 1 / (z - d)) + fun z : ℂ => 1 / (z + d) :=
     by rfl
   rw [h1]
-  have := iter_deriv_within_add k ⟨x, hx⟩ (fun z : ℂ => 1 / (z - d)) fun z : ℂ => 1 / (z + d)
   simp at *
-  rw [this]
+  rw [iteratedDerivWithin_add hx upperHalfSpace.uniqueDiffOn]
   · have h2 := aut_iter_deriv d k hx
     have h3 := aut_iter_deriv' d k hx
     simp at *
@@ -987,7 +985,7 @@ theorem aux_iter_der_tsum (k : ℕ) (hk : 2 ≤ k) (x : ℍ') :
         ((fun z : ℂ => 1 / z) + fun z : ℂ => ∑' n : ℕ+, (1 / (z - n) + 1 / (z + n))) ℍ' x =
       (-1) ^ (k : ℕ) * (k : ℕ)! * ∑' n : ℤ, 1 / ((x : ℂ) + n) ^ (k + 1 : ℕ) :=
   by
-  rw [iter_deriv_within_add]
+  rw [iteratedDerivWithin_add x.2 UpperHalfPlane.upperHalfSpace.uniqueDiffOn]
   · have h1 := aut_iter_deriv 0 k x.2
     simp  at *
     rw [h1]

Modformsported/ForMathlib/EisensteinSeries/q_expansions.lean

@@ -10,7 +10,6 @@ import Modformsported.ModForms.Riemzeta
 import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
 import Mathlib.Analysis.Calculus.Series
 import Modformsported.ForMathlib.TsumLemmas
-import Modformsported.ForMathlib.IteratedDerivLemmas
 import Modformsported.ForMathlib.ExpSummableLemmas
 import Modformsported.ForMathlib.AuxpLemmas
 import Modformsported.ForMathlib.Cotangent.CotangentIdentity

Modformsported/ForMathlib/ExpSummableLemmas.lean

@@ -2,9 +2,10 @@ import Mathlib.Data.Complex.Exponential
 import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
 import Mathlib.Analysis.Calculus.Series
 import Modformsported.ForMathlib.TsumLemmas
-import Modformsported.ForMathlib.IteratedDerivLemmas
 import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
+import Modformsported.ForMathlib.ModForms2
+import Modformsported.ModForms.HolomorphicFunctions
 
 noncomputable section
 
@@ -487,15 +488,19 @@ theorem iter_der_within_add (k : ℕ+) (x : ℍ') :
         (fun z => ↑π * I - (2 * ↑π * I) • ∑' n : ℕ, Complex.exp (2 * ↑π * I * n * z)) ℍ' x =
       -(2 * ↑π * I) * ∑' n : ℕ, (2 * ↑π * I * n) ^ (k : ℕ) * Complex.exp (2 * ↑π * I * n * x) :=
   by
-  rw [iter_der_within_const_neg k k.2 x]
+  have := iteratedDerivWithin_const_neg x.2 UpperHalfPlane.upperHalfSpace.uniqueDiffOn k.2 (↑π * I)
+    (f := fun z => (2 * ↑π * I) • ∑' (n : ℕ), cexp (2 * ↑π * I * ↑n * z))
+  erw [this]
   simp
   have :=
-    iter_der_within_neg' k x fun z => (2 * ↑π * I) • ∑' n : ℕ, Complex.exp (2 * ↑π * I * n * z)
+    iteratedDerivWithin_neg' x.2 UpperHalfPlane.upperHalfSpace.uniqueDiffOn (n := k)
+      (f := fun z => (2 * ↑π * I) • ∑' n : ℕ, Complex.exp (2 * ↑π * I * n * z))
   simp at this
-  rw [this]
+  erw [this]
   · rw [neg_eq_neg_one_mul]
     have t2 :=
-      iter_der_within_const_mul' k x (2 * ↑π * I) fun z => ∑' n : ℕ, Complex.exp (2 * ↑π * I * n * z)
+      iteratedDerivWithin_const_mul x.2 UpperHalfPlane.upperHalfSpace.uniqueDiffOn (n := k)
+        (2 * ↑π * I) (f := fun z => ∑' n : ℕ, Complex.exp (2 * ↑π * I * n * z))
     simp at t2
     rw [t2]
     · simp