DerivUpperBnd_aux2

lemma DerivUpperBnd_aux2 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Icc (1 - A / |t|.log) 2) :    let N := ⌊|t|⌋₊;    let s := ↑σ + ↑t * I;    0 < N → ↑N ≤ |t| → s ≠ 1 →    1 / 2 < σ → ‖-↑N ^ (1 - s) / (1 - s) ^ 2‖ ≤ A.exp * 2 * (1 / 3) := by  intro N s Npos N_le_t neOne σ_gt  dsimp only [s]  simp_rw [norm_div, norm_neg, norm_pow, norm_natCast_cpow_of_pos Npos _,    sub_re, one_re, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im,    mul_one, sub_self, add_zero]  have h := UpperBnd_aux6 t_gt ⟨σ_gt, hσ.2⟩ neOne Npos N_le_t |>.1  rw [(by ring_nf : N ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ^ 2 =          N ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ * 1 / ‖1 - (↑σ + ↑t * I)‖)]  apply mul_le_mul ?_ ?_ (inv_nonneg.mpr <| norm_nonneg _) ?_  · rw [mul_one]; exact le_trans h (by gcongr; exact UpperBnd_aux2 t_gt hσ.1)  · rw [inv_eq_one_div, div_le_iff₀ <| norm_pos_iff.mpr <| sub_ne_zero_of_ne neOne.symm,        mul_comm, ← mul_div_assoc, mul_one, le_div_iff₀ (by norm_num), one_mul]    apply le_trans t_gt.le ?_    rw [← abs_neg]; convert! abs_im_le_norm (1 - (σ + t * I)); simp  · exact mul_nonneg (Real.exp_nonneg _) (by norm_num)