Complex.borelCaratheodory_zero_closedBall

public theorem borelCaratheodory_zero_closedBall {f : ℂ → ℂ} {M r R : ℝ}    (hf : AnalyticOnNhd ℂ f (Metric.closedBall (0 : ℂ) R))    (hr : 0 < r) (hlt : r < R) (hM : 0 < M) (hf0 : f 0 = 0)    (hf_re : ∀ w, ‖w‖ ≤ R → (f w).re ≤ M) {z : ℂ} (hz : ‖z‖ ≤ r) :    ‖f z‖ ≤ 2 * M * r / (R - r) := by  have hR : 0 < R := lt_trans hr hlt  have hz_ball : z ∈ Metric.ball (0 : ℂ) R := by    rw [Metric.mem_ball, dist_zero_right]    exact hz.trans_lt hlt  have hf_diff : DifferentiableOn ℂ f (Metric.ball (0 : ℂ) R) := by    intro w hw    have hw' : w ∈ Metric.closedBall (0 : ℂ) R := ball_subset_closedBall hw    exact (hf w hw').differentiableAt.differentiableWithinAt  have hf_map : Set.MapsTo f (Metric.ball (0 : ℂ) R) {w | w.re ≤ M} := by    intro w hw    simp only [Set.mem_setOf_eq]    have hw' : ‖w‖ < R := by simpa [Metric.mem_ball, dist_zero_right] using hw    exact hf_re w hw'.le  have hbc :=    borelCaratheodory_zero hM hf_diff hf_map hR hz_ball hf0  have hzR : ‖z‖ < R := by    rw [Metric.mem_ball, dist_zero_right] at hz_ball    exact hz_ball  have hmono : ‖z‖ / (R - ‖z‖) ≤ r / (R - r) := by    have hrden : 0 < R - r := sub_pos.mpr hlt    have hden : 0 < R - ‖z‖ := sub_pos.mpr hzR    rw [div_le_div_iff₀ hden hrden]    nlinarith [hz, norm_nonneg z]  have hM' : 0 ≤ 2 * M := mul_nonneg (by norm_num) (le_of_lt hM)  calc ‖f z‖      ≤ 2 * M * ‖z‖ / (R - ‖z‖) := hbc    _ ≤ 2 * M * (r / (R - r)) := by        simpa [mul_div_assoc] using mul_le_mul_of_nonneg_left hmono hM'    _ = 2 * M * r / (R - r) := by ring