D is Bounded At Im Infty of bounded

lemma D_isBoundedAtImInfty_of_bounded {f : ℍ → ℂ}    (hf : MDiff f)    (hbdd : IsBoundedAtImInfty f) :    IsBoundedAtImInfty (D f) := by  rw [isBoundedAtImInfty_iff] at hbdd ⊢  obtain ⟨M, A, hMA⟩ := hbdd  use M / π, 2 * max A 0 + 1  intro z hz  have hR_pos : 0 < z.im / 2 := by linarith [z.im_pos]  have hclosed := closedBall_center_subset_upperHalfPlane z  have hDiff : DiffContOnCl ℂ (f ∘ ofComplex) (Metric.ball (z : ℂ) (z.im / 2)) :=    diffContOnCl_comp_ofComplex_of_mdifferentiable hf hclosed  have hf_bdd_sphere : ∀ w ∈ Metric.sphere (z : ℂ) (z.im / 2), ‖(f ∘ ofComplex) w‖ ≤ M := by    intro w hw    have hw_im_pos : 0 < w.im := hclosed (Metric.sphere_subset_closedBall hw)    have hdist : dist w z = z.im / 2 := Metric.mem_sphere.mp hw    have habs : |w.im - z.im| ≤ z.im / 2 := by      calc |w.im - z.im| = |(w - z).im| := by simp [Complex.sub_im]        _ ≤ ‖w - z‖ := abs_im_le_norm _        _ = dist w z := (dist_eq_norm _ _).symm        _ = z.im / 2 := hdist    have hw_im_ge_A : A ≤ w.im := by linarith [(abs_le.mp habs).1, le_max_left A 0]    simpa [ofComplex_apply_of_im_pos hw_im_pos] using hMA ⟨w, hw_im_pos⟩ hw_im_ge_A  have hz_im_ge_1 : 1 ≤ z.im := by linarith [le_max_right A 0]  have hM_nonneg : 0 ≤ M := le_trans (norm_nonneg _) (hMA z (by linarith [le_max_left A 0]))  calc ‖D f z‖ ≤ M / (2 * π * (z.im / 2)) := norm_D_le_of_sphere_bound hR_pos hDiff hf_bdd_sphere    _ = M / (π * z.im) := by ring    _ ≤ M / (π * 1) := by gcongr    _ = M / π := by ring