Complex.analyticOrderAt_weierstrassFactor_div_self

theorem analyticOrderAt_weierstrassFactor_div_self (m : ℕ) {a : ℂ} (ha : a ≠ 0) :    analyticOrderAt (fun z : ℂ => weierstrassFactor m (z / a)) a = (1 : ℕ∞) := by  set F : ℂ → ℂ := fun z => weierstrassFactor m (z / a)  have hF : AnalyticAt ℂ F a := by    have hdiv : Differentiable ℂ (fun z : ℂ => z / a) := by      simp [div_eq_mul_inv]    have hdiff : Differentiable ℂ F := (differentiable_weierstrassFactor m).comp hdiv    exact Differentiable.analyticAt (f := F) hdiff a  let g : ℂ → ℂ := fun z => (-a⁻¹) * Complex.exp (partialLogSum m (z / a))  have hg : AnalyticAt ℂ g a := by    have hdiv : Differentiable ℂ (fun z : ℂ => z / a) := by      simp [div_eq_mul_inv]    have hpls : Differentiable ℂ (fun z : ℂ => partialLogSum m (z / a)) :=      (differentiable_partialLogSum m).comp hdiv    have hexp : Differentiable ℂ (fun z : ℂ => Complex.exp (partialLogSum m (z / a))) :=      (Complex.differentiable_exp).comp hpls    have hdiffg : Differentiable ℂ g := by      simpa [g] using hexp.const_mul (-a⁻¹ : ℂ)    exact Differentiable.analyticAt (f := g) hdiffg a  have hg0 : g a ≠ 0 := by    have hconst : (-a⁻¹ : ℂ) ≠ 0 := by simp [ha]    have hexp0 : Complex.exp (partialLogSum m (a / a)) ≠ 0 :=      Complex.exp_ne_zero (partialLogSum m (a / a))    simpa [g] using mul_ne_zero hconst hexp0  refine (hF.analyticOrderAt_eq_natCast (n := 1)).2 ?_  refine ⟨g, hg, hg0, ?_⟩  refine Filter.Eventually.of_forall ?_  intro z  have hlin : (1 - z / a) = (z - a) * (-a⁻¹) := by    have h1 : (1 : ℂ) = a * a⁻¹ := by simp [ha]    simp [div_eq_mul_inv, h1]    ring  simp only [F, g, pow_one, smul_eq_mul]  rw [weierstrassFactor_def]  simp [hlin, mul_assoc]