DerivUpperBnd_aux6

theorem DerivUpperBnd_aux6 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Icc (1 - A / |t|.log) 2) :    let N := ⌊|t|⌋₊;    0 < N → ↑N ≤ |t| → ↑σ + ↑t * I ≠ 1 → 1 / 2 < σ →    2 * |t| * ↑N ^ (-σ) / σ ≤ 2 * (8 * A.exp) := by  intro N Npos N_le_t neOne σ_gt  rw [mul_div_assoc, mul_assoc]  apply mul_le_mul_iff_right₀ (by norm_num) |>.mpr  have h := UpperBnd_aux6 t_gt ⟨σ_gt, hσ.2⟩ neOne Npos N_le_t |>.2.2  apply le_trans (mul_le_mul_iff_right₀ (a := |t|) (by positivity) |>.mpr h) ?_  rw [← mul_assoc, mul_comm _ 8, mul_assoc]  gcongr  convert! UpperBnd_aux2 t_gt hσ.1 using 1  rw [mul_comm, ← Real.rpow_add_one (by positivity)]; ring_nf