apply le_trans ?_ (by linarith [hσ.1] : 4 ≤ σ * 8)
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) ≤ σ * 8
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) ≤ 4