calc
  _ = |((n : ℝ) ^ (-σ))| := ?_
  _ ≤ Real.exp (Real.log n * -σ) := Real.abs_rpow_le_exp_log_mul (n : ℝ) (-σ)
  _ ≤ Real.exp (Real.log n *  -(1 - A / Real.log t)) := ?_
  _ ≤ Real.exp (- Real.log n + A) := Real.exp_le_exp_of_le ?_
  _ ≤ _ := by rw [Real.exp_add, Real.exp_neg, Real.exp_log n_gt_0']
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
case neg.calc_1
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ ‖↑n ^ (-s)‖ = |↑n ^ (-σ)|

case neg.calc_2
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ ((↑n).log * -σ).exp ≤ ((↑n).log * -(1 - A / t.log)).exp

case neg.calc_3
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ (↑n).log * -(1 - A / t.log) ≤ -(↑n).log + A