conv => rw [mul_assoc]; rhs; rw [mul_comm]
case refine_1
σ 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|⌋₊ ^ (1 - σ) ≤ |t| ^ (1 - σ) * 2 * ‖1 - (↑σ + ↑t * I)‖
case refine_1
σ 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|⌋₊ ^ (1 - σ) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖ * |t| ^ (1 - σ)