Complex.weierstrassFactor_sub_one_pow_bound

theorem weierstrassFactor_sub_one_pow_bound {m : ℕ} {z : ℂ} (hz : ‖z‖ ≤ 1 / 2) :    ‖weierstrassFactor m z - 1‖ ≤ 4 * ‖z‖ ^ (m + 1) := by  by_cases hm : m = 0  · subst hm    have hmain : ‖(1 - z) - 1‖ ≤ 4 * ‖z‖ ^ 1 := by      have h : (1 - z) - 1 = -z := by ring      calc        ‖(1 - z) - 1‖ = ‖-z‖ := by simp [h]        _ = ‖z‖ := norm_neg z        _ = ‖z‖ ^ 1 := by simp        _ ≤ 4 * ‖z‖ ^ 1 := by nlinarith [pow_nonneg (norm_nonneg z) 1]    simpa [weierstrassFactor] using hmain  · have hz_lt : ‖z‖ < 1 := lt_of_le_of_lt hz (by norm_num)    by_cases hz1 : z = 1    · exfalso; rw [hz1] at hz; norm_num at hz    have h_eq : weierstrassFactor m z = exp (-logTail m z) :=      weierstrassFactor_eq_exp_neg_tail m hz_lt hz1    rw [h_eq]    have h_tail_bound := norm_logTail_le_two_mul_norm_pow hz_lt hz m    have hw_le_one : ‖-logTail m z‖ ≤ 1 := by      simp only [norm_neg]      have : ‖logTail m z‖ ≤ 1 := by        have hm_pos : 0 < m := Nat.pos_of_ne_zero hm        have h2 : 2 ≤ m + 1 := by          exact Nat.succ_le_succ (Nat.succ_le_iff.2 hm_pos)        have hpow : (‖z‖ ^ (m + 1)) ≤ (‖z‖ ^ 2) := by          have hz1' : ‖z‖ ≤ 1 := by nlinarith [hz]          have hz0' : 0 ≤ ‖z‖ := norm_nonneg z          exact pow_le_pow_of_le_one hz0' hz1' h2        have hmul : 2 * ‖z‖ ^ (m + 1) ≤ 2 * ‖z‖ ^ 2 := by gcongr        have hsq : 2 * ‖z‖ ^ 2 ≤ 1 := by          have hz0 : 0 ≤ ‖z‖ := norm_nonneg z          have hz_sq : ‖z‖ ^ 2 ≤ (1 / 2 : ℝ) ^ 2 := pow_le_pow_left₀ hz0 hz 2          nlinarith        exact (h_tail_bound.trans hmul).trans hsq      linarith    have h_exp_sub_one : ‖exp (-logTail m z) - 1‖ ≤ 2 * ‖-logTail m z‖ :=      Complex.norm_exp_sub_one_le hw_le_one    simp only [norm_neg] at h_exp_sub_one    calc      ‖exp (-logTail m z) - 1‖ ≤ 2 * ‖logTail m z‖ := h_exp_sub_one      _ ≤ 2 * (2 * ‖z‖ ^ (m + 1)) := by gcongr      _ = 4 * ‖z‖ ^ (m + 1) := by ring