Serre D is Bounded At Im Infty of bounded

theorem serre_D_isBoundedAtImInfty_of_bounded {f : ℍ → ℂ} (k : ℂ)    (hf : MDiff f)    (hbdd : IsBoundedAtImInfty f) : IsBoundedAtImInfty (serre_D k f) := by  simp only [serre_D_eq]  have hD : IsBoundedAtImInfty (D f) := D_isBoundedAtImInfty_of_bounded hf hbdd  have hE₂f : IsBoundedAtImInfty (fun z => k * 12⁻¹ * E₂ z * f z) := by    have hconst : IsBoundedAtImInfty (fun _ : ℍ => k * 12⁻¹) :=      Filter.const_boundedAtFilter _ _    have hmul : IsBoundedAtImInfty (fun z => (k * 12⁻¹) * (E₂ z * f z)) :=      hconst.mul (E₂_isBoundedAtImInfty.mul hbdd)    rw [isBoundedAtImInfty_iff] at hmul ⊢    obtain ⟨M, A, hMA⟩ := hmul    refine ⟨M, A, ?_⟩    intro z hz    simpa [mul_assoc] using hMA z hz  exact hD.sub hE₂f