Logderiv tendsto of div exp tendsto

lemma logderiv_tendsto_of_div_exp_tendsto {F : ℍ → ℂ} (hF : MDiff F) {a C : ℂ} (hC : C ≠ 0)    (hlim : Filter.Tendsto (fun z : ℍ ↦ F z / cexp (a * z)) atImInfty (nhds C)) :    Filter.Tendsto (fun z : ℍ ↦ D F z / F z) atImInfty (nhds (a / (2 * π * I))) := by  set q : ℍ → ℂ := fun w ↦ cexp (a * w) with hq  set g : ℍ → ℂ := fun w ↦ F w / q w with hg  have hq_ne : ∀ w : ℍ, q w ≠ 0 := fun w ↦ Complex.exp_ne_zero _  have hq_md : MDiff q := by    intro τ    change MDiffAt ((fun t : ℂ ↦ cexp (a * t)) ∘ fun w : ℍ ↦ (w : ℂ)) τ    exact DifferentiableAt_MDifferentiableAt      (G := fun t : ℂ ↦ cexp (a * t)) (z := τ) ((differentiableAt_id.const_mul a).cexp)  have hg_md : MDiff g := MDifferentiable_div hF hq_md hq_ne  have hDg_div_g : Filter.Tendsto (fun z ↦ D g z / g z) atImInfty (nhds 0) := by    change Filter.Tendsto (D g / g) atImInfty (nhds 0)    simpa using (D_tendsto_zero_of_isBoundedAtImInfty hg_md (hlim.isBigO_one ℝ)).div hlim hC  have hF_eq : F = q * g := by ext w; simp only [hg, Pi.mul_apply, mul_div_cancel₀ _ (hq_ne w)]  have hDq_div_q : ∀ z : ℍ, D q z / q z = a / (2 * π * I) :=    fun z ↦ by rw [hq]; exact D_cexp_div a z  have h_logderiv : ∀ᶠ z : ℍ in atImInfty, D F z / F z = a / (2 * π * I) + D g z / g z := by    filter_upwards [hlim.eventually_ne hC] with z hz    rw [hF_eq, Pi.mul_apply, logderiv_mul_eq q g hq_md hg_md z (hq_ne z) hz, hDq_div_q z]  have hsum : Filter.Tendsto (fun z ↦ a / (2 * π * I) + D g z / g z) atImInfty      (nhds (a / (2 * π * I))) := by tendsto_cont  exact hsum.congr' (by filter_upwards [h_logderiv] with z hz; exact hz.symm)