E₂E₄ sub E₆ div q tendsto

theorem E₂E₄_sub_E₆_div_q_tendsto :    Tendsto (fun z : ℍ ↦ (E₂ z * E₄ z - E₆ z) / cexp (2 * π * I * z))      atImInfty (nhds 720) := by  have h_eq : ∀ z : ℍ,      (E₂ z * E₄ z - E₆ z) / cexp (2 * π * Complex.I * z) =        720 * (∑' n : ℕ+, ↑n * ↑(ArithmeticFunction.sigma 3 n) *          cexp (2 * π * Complex.I * (n - 1) * z)) := by    intro z    rw [E₂_mul_E₄_sub_E₆ z, mul_div_assoc, ← tsum_div_const]    congr 1    apply tsum_congr    intro n    rw [mul_div_assoc, ← Complex.exp_sub]    congr 2    ring  simp_rw [h_eq, sigma3_qexp_reindex_pnat_nat]  set a : ℕ → ℂ := fun m => ↑(m + 1) * ↑(ArithmeticFunction.sigma 3 (m + 1)) with ha  have ha0 : a 0 = 1 := by simp [ha, ArithmeticFunction.sigma_one]  have hbound : ∀ m, ‖a m‖ ≤ ((m + 1 : ℕ) : ℝ) ^ 5 := fun m => by    simp only [ha, norm_mul, Complex.norm_natCast]    calc (↑(m + 1) : ℝ) * ↑(ArithmeticFunction.sigma 3 (m + 1))        ≤ (↑(m + 1) : ℝ) * (↑(m + 1) : ℝ) ^ 4 :=          mul_le_mul_of_nonneg_left (mod_cast ArithmeticFunction.sigma_le_pow_succ 3 (m + 1))            (Nat.cast_nonneg _)      _ = _ := by ring  have h_eq2 : ∀ z : ℍ,      ∑' m : ℕ, ↑(m + 1) * ↑(ArithmeticFunction.sigma 3 (m + 1)) *        cexp (2 * π * Complex.I * m * z) =      ∑' m : ℕ, a m * cexp (2 * π * Complex.I * z * m) := by    intro z    apply tsum_congr    intro m    simp only [ha]    ring_nf  simp_rw [h_eq2]  simpa [ha0] using (qexp_tendsto_of_poly_bound hbound).const_mul (720 : ℂ)